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]

proof

let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
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: A1 +^ B in W
[: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

proof

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

A7: now :: thesis: ( A1 c= A implies x in W )

A8: B c= W by A3, ORDINAL1:def 2;
assume A1 c= A ; :: thesis: x in W
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: verum

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: verum

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: verum

end;

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