let A, B be Ordinal; :: thesis: ( A in B iff alef A in alef B )
defpred S₁[ Ordinal] means for A being Ordinal st A in $1 holds
alef A in alef $1;
A1: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A2: S₁[B] ; :: thesis: S₁[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies alef A in alef (succ B) )
A3: alef (succ B) = nextcard (alef B) by Th39;

A4: now

assume A in B ; :: thesis: ( A in succ B implies alef A in alef (succ B) )
then A5: alef A in alef B by A2;
alef B in nextcard (alef B) by Th32;
hence ( A in succ B implies alef A in alef (succ B) ) by A3, A5, ORDINAL1:19; :: thesis: verum

end;

A6: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;
assume A in succ B ; :: thesis: alef A in alef (succ B)
hence alef A in alef (succ B) by A3, A6, A4, Th32, ORDINAL1:21, ORDINAL1:34; :: thesis: verum

end;

A7: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A8: B <> {} and
A9: B is limit_ordinal and
for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
alef A in alef C ; :: thesis: S₁[B]
let A be Ordinal; :: thesis: ( A in B implies alef A in alef B )
consider S being T-Sequence such that
A10: ( dom S = B & ( for C being Ordinal st C in B holds
S . C = H₁(C) ) ) from ORDINAL2:sch 2();
assume A in B ; :: thesis: alef A in alef B
then succ A in B by A9, ORDINAL1:41;
then ( S . (succ A) in rng S & S . (succ A) = alef (succ A) ) by A10, FUNCT_1:def 5;
then A11: alef (succ A) in sup (rng S) by ORDINAL2:27;
sup (rng S) = sup S by ORDINAL2:35;
then A12: alef (succ A) c= sup S by A11, ORDINAL1:def 2;
A13: card (alef (succ A)) = alef (succ A) by Def5;
A14: ( alef (succ A) = nextcard (alef A) & alef A in nextcard (alef A) ) by Th32, Th39;
alef B = card (sup S) by A8, A9, A10, Lm1;
then alef (succ A) c= alef B by A12, A13, Th27;
hence alef A in alef B by A14; :: thesis: verum

end;

A15: S₁[ {} ] ;
A16: for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A15, A1, A7);
hence ( A in B implies alef A in alef B ) ; :: thesis: ( alef A in alef B implies A in B )
assume A17: alef A in alef B ; :: thesis: A in B
then A18: alef A <> alef B ;
not B in A by A16, A17;
hence A in B by A18, ORDINAL1:24; :: thesis: verum