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: S₁[ {} ] ;
A2: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A3: S₁[B] ; :: thesis: S₁[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies alef A in alef (succ B) )
assume A4: A in succ B ; :: thesis: alef A in alef (succ B)
A5: alef (succ B) = nextcard (alef B) by Th39;
A6: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;

now

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

end;

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

end;

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