let M be non countable Aleph; :: thesis: for A being Ordinal st M is strongly_inaccessible & A in M holds
card (Rank A) in M
let A be Ordinal; :: thesis: ( M is strongly_inaccessible & A in M implies card (Rank A) in M )
assume A1: ( M is strongly_inaccessible & A in M ) ; :: thesis: card (Rank A) in M
then A3: cf M = M by CARD_5:def 4;
defpred S₁[ Ordinal] means ( $1 in M implies card (Rank $1) in M );
A4: S₁[ {} ] by CLASSES1:33;
A5: for B1 being Ordinal st S₁[B1] holds
S₁[ succ B1]

proof

let B1 be Ordinal; :: thesis: ( S₁[B1] implies S₁[ succ B1] )
assume A6: S₁[B1] ; :: thesis: S₁[ succ B1]
assume succ B1 in M ; :: thesis: card (Rank (succ B1)) in M
then succ B1 c= M by ORDINAL1:def 2;
then A7: exp 2,(card (Rank B1)) in M by A1, A6, CARD_FIL:def 14, ORDINAL1:33;
Rank (succ B1) = bool (Rank B1) by CLASSES1:34;
hence card (Rank (succ B1)) in M by A7, CARD_2:44; :: thesis: verum

end;

A8: for B1 being Ordinal st B1 <> {} & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S₁[B2] ) holds
S₁[B1]

proof

let B1 be Ordinal; :: thesis: ( B1 <> {} & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S₁[B2] ) implies S₁[B1] )
assume that
B1 <> {} and
A9: B1 is limit_ordinal and
A10: for B2 being Ordinal st B2 in B1 holds
S₁[B2] ; :: thesis: S₁[B1]
assume A11: B1 in M ; :: thesis: card (Rank B1) in M
then A12: card B1 in M by CARD_1:25;
consider L being T-Sequence such that
A13: ( dom L = B1 & ( for A being Ordinal st A in B1 holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A14: Rank B1 = Union L by A9, A13, CLASSES2:25
.= union (rng L) by CARD_3:def 4 ;
card (rng L) c= card B1 by A13, CARD_1:28;
then A15: card (rng L) in cf M by A3, A12, ORDINAL1:22;
for Y being set st Y in rng L holds
card Y in M

proof

let Y be set ; :: thesis: ( Y in rng L implies card Y in M )
assume A16: Y in rng L ; :: thesis: card Y in M
consider x being set such that
A17: x in dom L and
A18: Y = L . x by A16, FUNCT_1:def 5;
reconsider x1 = x as Element of B1 by A13, A17;
A19: x1 in M by A11, A13, A17, ORDINAL1:19;
Y = Rank x1 by A13, A17, A18;
hence card Y in M by A10, A13, A17, A19; :: thesis: verum

end;

hence card (Rank B1) in M by A14, A15, Th34; :: thesis: verum

end;

for B1 being Ordinal holds S₁[B1] from ORDINAL2:sch 1(A4, A5, A8);
hence card (Rank A) in M by A1; :: thesis: verum