let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies card (Rank M) = M )
consider L being Sequence such that
A1: ( dom L = M & ( for A being Ordinal st A in M holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A2: rng L is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not X in rng L or not Y in rng L or X,Y are_c=-comparable )
assume X in rng L ; :: thesis: ( not Y in rng L or X,Y are_c=-comparable )
then consider x being object such that
A3: x in dom L and
A4: X = L . x by FUNCT_1:def 3;
assume Y in rng L ; :: thesis: X,Y are_c=-comparable
then consider y being object such that
A5: y in dom L and
A6: Y = L . y by FUNCT_1:def 3;
reconsider x = x, y = y as Ordinal by A3, A5;
A7: Y = Rank y by A1, A5, A6;
A8: ( x c= y or y c= x ) ;
X = Rank x by A1, A3, A4;
then ( X c= Y or Y c= X ) by A7, A8, CLASSES1:37;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

card M c= card (Rank M) by CARD_1:11, CLASSES1:38;
then A9: M c= card (Rank M) ;
A10: Rank M = Union L by A1, CLASSES2:24
.= union (rng L) by CARD_3:def 4 ;
assume A11: M is strongly_inaccessible ; :: thesis: card (Rank M) = M

now :: thesis: for X being set st X in rng L holds
card X in M

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 object such that
A12: x in dom L and
A13: X = L . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A12;
card (Rank x) in M by A11, A1, A12, Th34;
hence card X in M by A1, A12, A13; :: thesis: verum

end;

then card (union (rng L)) c= M by A2, CARD_3:46;
hence card (Rank M) = M by A10, A9, XBOOLE_0:def 10; :: thesis: verum