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

A1: now :: thesis: for x being object st x in E holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in E implies ex y being object st S₁[x,y] )
assume x in E ; :: thesis: ex y being object 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 object st S₁[x,y] ; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in rng f implies x is Ordinal )
assume x in rng f ; :: thesis: x is Ordinal
then consider y being object such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 3;
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:24;
take A ; :: thesis: E = Collapse (E,A)
thus for x being object 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 object ; :: 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 3;
then Collapse (E,B) c= Collapse (E,A) by Th4, A6, ORDINAL1:def 2;
hence x in Collapse (E,A) by A9; :: thesis: verum

end;

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