let E be non empty set ; :: thesis: for d being Element of E ex A being Ordinal st d in Collapse (E,A)
let d be Element of E; :: thesis: ex A being Ordinal st d in Collapse (E,A)
defpred S₁[ object ] means for A being Ordinal holds not $1 in Collapse (E,A);
defpred S₂[ object , object ] means ex A being Ordinal st
( $2 = A & $1 in Collapse (E,A) & ( for B being Ordinal st $1 in Collapse (E,B) holds
A c= B ) );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in E & S₁[x] ) ) from XBOOLE_0:sch 1();

now :: thesis: for x being object holds not x in X

given x being object such that A2: x in X ; :: thesis: contradiction
consider m being set such that
A3: m in X and
A4: X misses m by A2, XREGULAR:1;
reconsider m = m as Element of E by A1, A3;

A5: now :: thesis: for x being object st x in m /\ E holds
ex y being object st S₂[x,y]

let x be object ; :: thesis: ( x in m /\ E implies ex y being object st S₂[x,y] )
defpred S₃[ Ordinal] means x in Collapse (E,$1);
assume A6: x in m /\ E ; :: thesis: ex y being object st S₂[x,y]
then x in m by XBOOLE_0:def 4;
then A7: not x in X by A4, XBOOLE_0:3;
x in E by A6, XBOOLE_0:def 4;
then A8: ex A being Ordinal st S₃[A] by A1, A7;
ex A being Ordinal st
( S₃[A] & ( for B being Ordinal st S₃[B] holds
A c= B ) ) from ORDINAL1:sch 1(A8);
hence ex y being object st S₂[x,y] ; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = m /\ E & ( for x being object st x in m /\ E holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A5);
for y being object st y in rng f holds
y is Ordinal

proof

let y be object ; :: thesis: ( y in rng f implies y is Ordinal )
assume y in rng f ; :: thesis: y is Ordinal
then consider x being object such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 3;
ex A being Ordinal st
( f . x = A & x in Collapse (E,A) & ( for B being Ordinal st x in Collapse (E,B) holds
A c= B ) ) by A9, A10;
hence y is Ordinal by A11; :: thesis: verum

end;

then consider A being Ordinal such that
A12: rng f c= A by ORDINAL1:24;
for d being Element of E st d in m holds
ex B being Ordinal st
( B in A & d in Collapse (E,B) )

proof

let d be Element of E; :: thesis: ( d in m implies ex B being Ordinal st
( B in A & d in Collapse (E,B) ) )
assume d in m ; :: thesis: ex B being Ordinal st
( B in A & d in Collapse (E,B) )
then A13: d in m /\ E by XBOOLE_0:def 4;
then consider B being Ordinal such that
A14: f . d = B and
A15: d in Collapse (E,B) and
for C being Ordinal st d in Collapse (E,C) holds
B c= C by A9;
take B ; :: thesis: ( B in A & d in Collapse (E,B) )
B in rng f by A9, A13, A14, FUNCT_1:def 3;
hence ( B in A & d in Collapse (E,B) ) by A12, A15; :: thesis: verum

end;

then m in { d9 where d9 is Element of E : for d being Element of E st d in d9 holds
ex B being Ordinal st
( B in A & d in Collapse (E,B) ) } ;
then m in Collapse (E,A) by Th1;
hence contradiction by A1, A3; :: thesis: verum

end;

hence ex A being Ordinal st d in Collapse (E,A) by A1; :: thesis: verum