defpred S₁[ Ordinal] means ( $1 in W implies A1 +^ $1 in W );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

let B be Ordinal; :: thesis:
assume that
A2: for C being Ordinal st C in B & C in W holds
A1 +^ C in W and
A3: B in W ; :: thesis:
[:B,{(1-element_of W)}:] in W by A3, CLASSES2:61;
then [:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:] in W by CLASSES2:60;
then A4: card ([:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:]) in card W by CLASSES2:1;
A5: A1 +^ B c= W

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in A1 +^ B ; :: thesis:
then reconsider A = x as Ordinal ;

A7: now :: thesis:

A8: B c= W by A3, ORDINAL1:def 2;
assume A1 c= A ; :: thesis:
then consider C being Ordinal such that
A9: A = A1 +^ C by ORDINAL3:27;
C in B by A6, A9, ORDINAL3:22;
hence x in W by A2, A9, A8; :: thesis:

end;

A10: ( A in A1 or A1 c= A ) by ORDINAL1:16;
A1 c= W by ORDINAL1:def 2;
hence x in W by A10, A7; :: thesis:

end;

card (A1 +^ B) = card ([:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:]) by CARD_2:9;
hence A1 +^ B in W by A4, A5, CLASSES1:1; :: thesis:

end;

for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A1);
hence A1 +^ B1 is Ordinal of W ; :: thesis: