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₁[ set ] means for A being Ordinal holds not $1 in Collapse E,A;
defpred S₂[ set , set ] 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 set holds
( x in X iff ( x in E & S₁[x] ) ) from XBOOLE_0:sch 1();
assume A2: for A being Ordinal holds not d in Collapse E,A ; :: thesis: contradiction

now

given x being set such that A3: x in X ; :: thesis: contradiction
consider m being set such that
A4: ( m in X & ( for x being set holds
( not x in X or not x in m ) ) ) by A3, TARSKI:7;
reconsider m = m as Element of E by A1, A4;

A8: now

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

end;

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

proof

let y be set ; :: thesis: ( y in rng f implies y is Ordinal )
assume y in rng f ; :: thesis: y is Ordinal
then consider x being set such that
A12: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
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 A11, A12;
hence y is Ordinal by A12; :: thesis: verum

end;

then consider A being Ordinal such that
A13: rng f c= A by ORDINAL1:36;
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 A14: d in m /\ E by XBOOLE_0:def 4;
then consider B being Ordinal such that
A15: ( f . d = B & d in Collapse E,B & ( for C being Ordinal st d in Collapse E,C holds
B c= C ) ) by A11;
take B ; :: thesis: ( B in A & d in Collapse E,B )
B in rng f by A11, A14, A15, FUNCT_1:def 5;
hence ( B in A & d in Collapse E,B ) by A13, A15; :: thesis: verum

end;

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

end;

then not d in X ;
hence contradiction by A1, A2; :: thesis: verum