New example

--- a/src/ZF/ex/misc.ML	Fri Nov 28 07:41:24 1997 +0100
+++ b/src/ZF/ex/misc.ML	Fri Nov 28 10:36:08 1997 +0100
@@ -14,6 +14,11 @@
 by (Blast_tac 1);
 result();
 
+(*variant of the benchmark above*)
+goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+by (Blast_tac 1);
+result();
+
 context Perm.thy;
 
 (*Example 12 (credited to Peter Andrews) from