consider a being Ordinal of W;
a in On W by ORDINAL1:def 10;
then a in dom L by Def5;
then L . a in rng L by FUNCT_1:def 5;
then ( L . a c= union (rng L) & L . a <> {} ) by RELAT_1:def 9, ZFMISC_1:92;
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, RELAT_1:def 19;
then A1: Union L c= union W by ZFMISC_1:95;
S c= W

proof

let x be set ; :: 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