let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies Rank M is Tarski )
assume A1: M is strongly_inaccessible ; :: thesis: Rank M is Tarski
then A2: cf M = M by CARD_5:def 4;
thus for X, Y being set st X in Rank M & Y c= X holds
Y in Rank M by CLASSES1:47; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b₁ being set holds
( not b₁ in Rank M or bool b₁ in Rank M ) ) & ( for b₁ being set holds
( not b₁ c= Rank M or b₁, Rank M are_equipotent or b₁ in Rank M ) ) )
thus for X being set st X in Rank M holds
bool X in Rank M :: thesis: for b₁ being set holds
( not b₁ c= Rank M or b₁, Rank M are_equipotent or b₁ in Rank M )

proof

let X be set ; :: thesis: ( X in Rank M implies bool X in Rank M )
assume X in Rank M ; :: thesis: bool X in Rank M
then consider A being Ordinal such that
A3: ( A in M & X in Rank A ) by CLASSES1:35;
( succ A in M & bool X in Rank (succ A) ) by A3, CLASSES1:48, ORDINAL1:41;
hence bool X in Rank M by CLASSES1:35; :: thesis: verum

end;

thus for X being set holds
( not X c= Rank M or X, Rank M are_equipotent or X in Rank M ) :: thesis: verum

proof

let X be set ; :: thesis: ( not X c= Rank M or X, Rank M are_equipotent or X in Rank M )
A4: ( card X c< M iff ( card X c= M & card X <> M ) ) by XBOOLE_0:def 8;
assume A5: ( X c= Rank M & not X, Rank M are_equipotent & not X in Rank M ) ; :: thesis: contradiction
then ( card X c= card (Rank M) & card X <> card (Rank M) ) by CARD_1:21, CARD_1:27;
then A6: ( card X = card X & card X in M ) by A1, A4, Th36, ORDINAL1:21;
set R = the_rank_of X;

per cases ( X = {} or not X is empty ) ;

suppose A7: X = {} ; :: thesis: contradiction

( {} <> M & {} c= M ) ;
then {} c< M by XBOOLE_0:def 8;
then ( {} in M & M c= Rank M ) by CLASSES1:44, ORDINAL1:21;
hence contradiction by A5, A7; :: thesis: verum

end;

suppose not X is empty ; :: thesis: contradiction

then reconsider X1 = X as non empty set ;
the_rank_of X in M

proof

A8: for x being set st x in X holds
x in Rank M by A5;
deffunc H₂( set ) -> set = the_rank_of $1;
set RANKS = { H₂(x) where x is Element of X1 : x in X1 } ;
{ H₂(x) where x is Element of X1 : x in X1 } c= M

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { H₂(x) where x is Element of X1 : x in X1 } or y in M )
assume A9: y in { H₂(x) where x is Element of X1 : x in X1 } ; :: thesis: y in M
consider x being Element of X1 such that
A10: ( y = the_rank_of x & x in X1 ) by A9;
x in Rank M by A8;
hence y in M by A10, CLASSES1:74; :: thesis: verum

end;

then reconsider RANKS1 = { H₂(x) where x is Element of X1 : x in X1 } as Subset of M ;
ex N1 being Ordinal st
( N1 in M & ( for x being set st x in X1 holds
the_rank_of x in N1 ) )

proof

assume A11: for N1 being Ordinal st N1 in M holds
ex x being set st
( x in X1 & not the_rank_of x in N1 ) ; :: thesis: contradiction
for N1 being Ordinal st N1 in M holds
ex C being Ordinal st
( C in { H₂(x) where x is Element of X1 : x in X1 } & N1 c= C )

proof

let N1 be Ordinal; :: thesis: ( N1 in M implies ex C being Ordinal st
( C in { H₂(x) where x is Element of X1 : x in X1 } & N1 c= C ) )
assume A12: N1 in M ; :: thesis: ex C being Ordinal st
( C in { H₂(x) where x is Element of X1 : x in X1 } & N1 c= C )
consider x being set such that
A13: x in X1 and
A14: not the_rank_of x in N1 by A11, A12;
take C = the_rank_of x; :: thesis: ( C in { H₂(x) where x is Element of X1 : x in X1 } & N1 c= C )
thus C in { H₂(x) where x is Element of X1 : x in X1 } by A13; :: thesis: N1 c= C
thus N1 c= C by A14, ORDINAL1:26; :: thesis: verum

end;

then RANKS1 is unbounded by Th7;
then A15: cf M c= card RANKS1 by Th21;
card { H₂(x) where x is Element of X1 : x in X1 } c= card X1 from TREES_2:sch 2();
then M c= card X1 by A2, A15, XBOOLE_1:1;
then card X1 in card X1 by A6;
hence contradiction ; :: thesis: verum

end;

then consider N1 being Ordinal such that
A16: N1 in M and
A17: for x being set st x in X1 holds
the_rank_of x in N1 ;
the_rank_of X c= N1 by A17, CLASSES1:77;
hence the_rank_of X in M by A16, ORDINAL1:22; :: thesis: verum

end;

hence contradiction by A5, CLASSES1:74; :: thesis: verum

end;

end;

end;