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