let X be set ; :: thesis:
let a be Ordinal of W; :: thesis:
set f = the Function of VAR,(L . a);
assume X in L . a ; :: thesis:
then reconsider e = X as Element of L . a ;
L . a in Union L by A2;
then A5: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),( the Function of VAR,(L . a) / ((x. 1),e))) in Union L by A3;
L . a is epsilon-transitive by A2;
hence (L . a) /\ (bool X) in Union L by A5, Th1; :: thesis:

end;

defpred S₁[ set , set ] means $1 in L . $2;
let X be set ; :: thesis:
assume A7: X in Union L ; :: thesis:
A8: X in bool X by ZFMISC_1:def 1;
then reconsider D = (Union L) /\ (bool X) as non empty set by A7, XBOOLE_0:def 4;
A9: X in (Union L) /\ (bool X) by A7, A8, XBOOLE_0:def 4;
A10: for d being Element of D ex a being Ordinal of W st S₁[d,a]

let d be Element of D; :: thesis:
d in Union L by XBOOLE_0:def 4;
then consider u2 being set such that
A11: u2 in dom L and
A12: d in L . u2 by Lm1;
u2 in On W by A11, ZF_REFLE:def 2;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7;
take u2 ; :: thesis:
thus S₁[d,u2] by A12; :: thesis:

end;

consider f being Function such that
A13: ( dom f = D & ( for d being Element of D ex a being Ordinal of W st
( a = f . d & S₁[d,a] & ( for b being Ordinal of W st S₁[d,b] holds
a c= b ) ) ) ) from ZF_REFLE:sch 1(A10);
A14: rng f c= W

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in rng f ; :: thesis:
then consider u1 being object such that
A15: u1 in D and
A16: u = f . u1 by A13, FUNCT_1:def 3;
reconsider u1 = u1 as Element of D by A15;
ex a being Ordinal of W st
( a = f . u1 & u1 in L . a & ( for b being Ordinal of W st u1 in L . b holds
a c= b ) ) by A13;
hence u in W by A16; :: thesis:

end;

let u2 be object ; :: according to TARSKI:def 3 :: thesis:
assume u2 in D ; :: thesis:
then reconsider d = u2 as Element of D ;
consider c being Ordinal of W such that
A19: c = f . d and
A20: d in L . c and
for b being Ordinal of W st d in L . b holds
c c= b by A13;
c in rng f by A13, A19, FUNCT_1:def 3;
then L . c c= L . a by A1, ORDINAL2:19;
hence u2 in L . a by A20; :: thesis:

end;

end;

let X be set ; :: according to ORDINAL1:def 2 :: thesis:
assume X in Union L ; :: thesis:
then consider u being set such that
A22: u in dom L and
A23: X in L . u by Lm1;
reconsider u = u as Ordinal by A22;
u in On W by A22, ZF_REFLE:def 2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A2;
then A24: X c= L . u by A23;
let u1 be object ; :: according to TARSKI:def 3 :: thesis:
A25: L . u c= Union L by ZF_REFLE:16;
assume u1 in X ; :: thesis:
then u1 in L . u by A24;
hence u1 in Union L by A25; :: thesis:

end;