set a = the Ordinal of W;
the Ordinal of W in On W by ORDINAL1:def 9;
then the Ordinal of W in dom L by Def2;
then L . the Ordinal of W in rng L by FUNCT_1:def 3;
then ( L . the Ordinal of W c= union (rng L) & L . the Ordinal of W <> {} ) by ZFMISC_1:74;
then union (rng L) <> {} ;
then reconsider S = Union L as non empty set by CARD_3:def 4;
( rng L c= W & Union L = union (rng L) ) by CARD_3:def 4;
then A1: Union L c= union W by ZFMISC_1:77;
S c= W
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in W )
assume x in S ; :: thesis: x in W
then consider X being set such that
A2: x in X and
A3: X in W by A1, TARSKI:def 4;
X c= W by A3, ORDINAL1:def 2;
hence x in W by A2; :: thesis: verum
end;
hence Union L is Subclass of W ; :: thesis: verum