let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies card (Rank M) = M )
assume A1: M is strongly_inaccessible ; :: thesis: card (Rank M) = M
consider L being T-Sequence such that
A2: ( dom L = M & ( for A being Ordinal st A in M holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A3: Rank M = Union L by A2, CLASSES2:25
.= union (rng L) by CARD_3:def 4 ;
A4: rng L is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 9 :: thesis: ( not X in rng L or not Y in rng L or not R12(X,Y) )
assume X in rng L ; :: thesis: ( not Y in rng L or not R12(X,Y) )
then consider x being set such that
A5: ( x in dom L & X = L . x ) by FUNCT_1:def 5;
assume Y in rng L ; :: thesis: R12(X,Y)
then consider y being set such that
A6: ( y in dom L & Y = L . y ) by FUNCT_1:def 5;
reconsider x = x, y = y as Ordinal by A5, A6;
( X = Rank x & Y = Rank y & ( x c= y or y c= x ) ) by A2, A5, A6;
then ( X c= Y or Y c= X ) by CLASSES1:43;
hence R12(X,Y) by XBOOLE_0:def 9; :: thesis: verum

end;

now

let X be set ; :: thesis: ( X in rng L implies card X in M )
assume X in rng L ; :: thesis: card X in M
then consider x being set such that
A7: ( x in dom L & X = L . x ) by FUNCT_1:def 5;
reconsider x = x as Ordinal by A7;
card (Rank x) in M by A1, A2, A7, Th35;
hence card X in M by A2, A7; :: thesis: verum

end;

then A8: card (union (rng L)) c= M by A4, CARD_3:62;
card M c= card (Rank M) by CARD_1:27, CLASSES1:44;
then M c= card (Rank M) by CARD_1:def 5;
hence card (Rank M) = M by A3, A8, XBOOLE_0:def 10; :: thesis: verum