defpred S_{1}[ 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_{1}[C] ) holds

S_{1}[B]
_{1}[B]
from ORDINAL1:sch 2(A1);

hence A1 +^ B1 is Ordinal of W ; :: thesis: verum

A1: for B being Ordinal st ( for C being Ordinal st C in B holds

S

S

proof

for B being Ordinal holds S
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds

S_{1}[C] ) implies S_{1}[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

hence A1 +^ B in W by A4, A5, CLASSES1:1; :: thesis: verum

end;S

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

card (A1 +^ B) = card ([:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:])
by CARD_2:9;
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 ;

A1 c= W by ORDINAL1:def 2;

hence x in W by A10, A7; :: thesis: verum

end;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 )

A10:
( A in A1 or A1 c= A )
by ORDINAL1:16;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;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

A1 c= W by ORDINAL1:def 2;

hence x in W by A10, A7; :: thesis: verum

hence A1 +^ B in W by A4, A5, CLASSES1:1; :: thesis: verum

hence A1 +^ B1 is Ordinal of W ; :: thesis: verum