reconsider K = phi | (Rank a) as Ordinal-Sequence by Th11;
reconsider A = Union (W | K) as Ordinal by Th13;
a in On W by ORDINAL1:def 10;
then ( dom K c= Rank a & Rank a in W ) by CLASSES2:26, RELAT_1:87;
then ( dom (W | K) c= dom K & dom K in W ) by CLASSES1:def 1, FUNCT_1:89;
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:146;
then ( rng (W | K) c= W & card (rng (W | K)) in card W ) by A1, CARD_2:3, ORDINAL1:22, RELAT_1:116;
then A2: rng (W | K) in W by CLASSES1:2;
union (rng (W | K)) = Union (W | K) by CARD_3:def 4;
then A in W by A2, CLASSES2:65;
hence union (phi,a) is Ordinal of W ; :: thesis: verum