Simplified proof of Hausdorff_next_exists.

--- a/src/ZF/Zorn.ML	Fri Apr 28 15:38:15 1995 +0200
+++ b/src/ZF/Zorn.ML	Mon May 01 11:17:41 1995 +0200
@@ -204,8 +204,6 @@
 			    chain_subset_Pow RS subsetD,
 			    choice_super]) 1);
 (*Now, verify that it increases*)
-by (rtac allI 1);
-by (rtac impI 1);
 by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl]
                         setloop split_tac [expand_if]) 1);
 by (safe_tac ZF_cs);