defpred S_{1}[ Ordinal] means ( $1 in W implies $1 *^ B1 in W );

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

S_{1}[C] ) holds

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

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

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

S

S

proof

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

S_{1}[C] ) implies S_{1}[A] )

assume that

A2: for C being Ordinal st C in A & C in W holds

C *^ B1 in W and

A3: A in W ; :: thesis: A *^ B1 in W

[:A,B1:] in W by A3, CLASSES2:61;

then A4: card [:A,B1:] in card W by CLASSES2:1;

A5: A *^ B1 c= W

hence A *^ B1 in W by A4, A5, CLASSES1:1; :: thesis: verum

end;S

assume that

A2: for C being Ordinal st C in A & C in W holds

C *^ B1 in W and

A3: A in W ; :: thesis: A *^ B1 in W

[:A,B1:] in W by A3, CLASSES2:61;

then A4: card [:A,B1:] in card W by CLASSES2:1;

A5: A *^ B1 c= W

proof

card (A *^ B1) = card [:A,B1:]
by CARD_2:11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A *^ B1 or x in W )

A6: B1 c= W by ORDINAL1:def 2;

assume A7: x in A *^ B1 ; :: thesis: x in W

then reconsider B = x as Ordinal ;

B1 <> {} by A7, ORDINAL2:38;

then consider C, D being Ordinal such that

A8: B = (C *^ B1) +^ D and

A9: D in B1 by ORDINAL3:47;

C *^ B1 c= B by A8, ORDINAL3:24;

then C *^ B1 in A *^ B1 by A7, ORDINAL1:12;

then A10: C in A by ORDINAL3:34;

A c= W by A3, ORDINAL1:def 2;

then reconsider CB = C *^ B1, D = D as Ordinal of W by A2, A9, A6, A10;

x = CB +^ D by A8;

hence x in W ; :: thesis: verum

end;A6: B1 c= W by ORDINAL1:def 2;

assume A7: x in A *^ B1 ; :: thesis: x in W

then reconsider B = x as Ordinal ;

B1 <> {} by A7, ORDINAL2:38;

then consider C, D being Ordinal such that

A8: B = (C *^ B1) +^ D and

A9: D in B1 by ORDINAL3:47;

C *^ B1 c= B by A8, ORDINAL3:24;

then C *^ B1 in A *^ B1 by A7, ORDINAL1:12;

then A10: C in A by ORDINAL3:34;

A c= W by A3, ORDINAL1:def 2;

then reconsider CB = C *^ B1, D = D as Ordinal of W by A2, A9, A6, A10;

x = CB +^ D by A8;

hence x in W ; :: thesis: verum

hence A *^ B1 in W by A4, A5, CLASSES1:1; :: thesis: verum

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