reconsider K = phi | (Rank a) as Ordinal-Sequence by Th9;
reconsider A = Union (W |` K) as Ordinal by Th11;
a in On W by ORDINAL1:def 9;
then ( dom K c= Rank a & Rank a in W ) by CLASSES2:25, RELAT_1:58;
then ( dom (W |` K) c= dom K & dom K in W ) by CLASSES1:def 1, FUNCT_1:56;
then dom (W |` K) in W by CLASSES1:def 1;
then A1: card (dom (W |` K)) in card W by CLASSES2:1;
(W |` K) .: (dom (W |` K)) = rng (W |` K) by RELAT_1:113;
then ( rng (W |` K) c= W & card (rng (W |` K)) in card W ) by A1, CARD_1:67, ORDINAL1:12, RELAT_1:85;
then A2: rng (W |` K) in W by CLASSES1:1;
union (rng (W |` K)) = Union (W |` K) by CARD_3:def 4;
then A in W by A2, CLASSES2:59;
hence union (phi,a) is Ordinal of W ; :: thesis: verum