let M be non countable Aleph; :: thesis:
let A be Ordinal; :: thesis:
assume that
A1: M is strongly_inaccessible and
A2: A in M ; :: thesis:
defpred S₁[ Ordinal] means ( $1 in M implies card (Rank $1) in M );
A3: for B1 being Ordinal st S₁[B1] holds
S₁[ succ B1]

end;

A6: cf M = M by A1, CARD_5:def 3;
A7: for B1 being Ordinal st B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S₁[B2] ) holds
S₁[B1]

let B1 be Ordinal; :: thesis:
assume that
B1 <> 0 and
A8: B1 is limit_ordinal and
A9: for B2 being Ordinal st B2 in B1 holds
S₁[B2] ; :: thesis:
consider L being Sequence such that
A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A11: card (rng L) c= card B1 by A10, CARD_1:12;
assume A12: B1 in M ; :: thesis:
then card B1 in M by CARD_1:9;
then A13: card (rng L) in cf M by A6, A11, ORDINAL1:12;
A14: for Y being set st Y in rng L holds
card Y in M

let Y be set ; :: thesis:
assume Y in rng L ; :: thesis:
then consider x being object such that
A15: x in dom L and
A16: Y = L . x by FUNCT_1:def 3;
reconsider x1 = x as Element of B1 by A10, A15;
( x1 in M & Y = Rank x1 ) by A12, A10, A15, A16, ORDINAL1:10;
hence card Y in M by A9, A10, A15; :: thesis:

end;

end;