# HG changeset patch
# User lcp
# Date 786106267 -3600
# Node ID 521a6f3ff27912fbff08c4955f3d33fbf076b1dd
# Parent  ec86863e87c8f0f2b44e6cd26d7b2d96b5a67468
le_UN_Ord_lt_csucc: added comment

diff -r ec86863e87c8 -r 521a6f3ff279 src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Tue Nov 29 00:31:31 1994 +0100
+++ b/src/ZF/Cardinal_AC.ML	Tue Nov 29 11:51:07 1994 +0100
@@ -144,6 +144,8 @@
 by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
 val lt_subset_trans = result();
 
+(*The same yet again, but the index set need not be a cardinal.  
+  Surprisingly complicated proof!*)
 goal Cardinal_AC.thy
     "!!K. [| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |] ==> \
 \         (UN w:W. j(w)) < csucc(K)";