let E be non empty set ; :: thesis: ex A being Ordinal st E = 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 ) );

A1: now

let x be set ; :: thesis: ( x in E implies ex y being set st S₁[x,y] )
assume x in E ; :: thesis: ex y being set st S₁[x,y]
then reconsider d = x as Element of E ;
defpred S₂[ Ordinal] means d in Collapse E,$1;
A2: ex A being Ordinal st S₂[A] by Th5;
ex A being Ordinal st
( S₂[A] & ( for B being Ordinal st S₂[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = E & ( for x being set st x in E holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
for x being set st x in rng f holds
x is Ordinal

proof

let x be set ; :: thesis: ( x in rng f implies x is Ordinal )
assume x in rng f ; :: thesis: x is Ordinal
then consider y being set such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 5;
ex A being Ordinal st
( f . y = A & y in Collapse E,A & ( for C being Ordinal st y in Collapse E,C holds
A c= C ) ) by A3, A4;
hence x is Ordinal by A5; :: thesis: verum

end;

then consider A being Ordinal such that
A6: rng f c= A by ORDINAL1:36;
take A ; :: thesis: E = Collapse E,A
thus for x being set st x in E holds
x in Collapse E,A :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Collapse E,A c= E

proof

let x be set ; :: thesis: ( x in E implies x in Collapse E,A )
assume A7: x in E ; :: thesis: x in Collapse E,A
then consider B being Ordinal such that
A8: f . x = B and
A9: x in Collapse E,B and
for C being Ordinal st x in Collapse E,C holds
B c= C by A3;
B in rng f by A3, A7, A8, FUNCT_1:def 5;
then B c= A by A6, ORDINAL1:def 2;
then Collapse E,B c= Collapse E,A by Th4;
hence x in Collapse E,A by A9; :: thesis: verum

end;

thus Collapse E,A c= E by Th7; :: thesis: verum