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
thus for X, Y being set st X in Rank M & Y c= X holds
Y in Rank M by CLASSES1:41; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b1 being set holds
( not b1 in Rank M or bool b1 in Rank M ) ) & ( for b1 being set holds
( not b1 c= Rank M or b1, Rank M are_equipotent or b1 in Rank M ) ) )
thus for X being set st X in Rank M holds
bool X in Rank M :: thesis: for b1 being set holds
( not b1 c= Rank M or b1, Rank M are_equipotent or b1 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
A2: ( A in M & X in Rank A ) by CLASSES1:31;
( succ A in M & bool X in Rank (succ A) ) by A2, CLASSES1:42, ORDINAL1:28;
hence bool X in Rank M by CLASSES1:31; :: thesis: verum
end;
A3: cf M = M by A1, CARD_5:def 3;
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;
set R = the_rank_of X;
assume that
A5: X c= Rank M and
A6: not X, Rank M are_equipotent and
A7: not X in Rank M ; :: thesis: contradiction
( card X c= card (Rank M) & card X <> card (Rank M) ) by A5, A6, CARD_1:5, CARD_1:11;
then A8: card X in M by A1, A4, Th35, ORDINAL1:11;
per cases ( X = {} or not X is empty ) ;
suppose not X is empty ; :: thesis: contradiction
then reconsider X1 = X as non empty set ;
the_rank_of X in M
proof
deffunc H2( set ) -> set = the_rank_of $1;
set RANKS = { H2(x) where x is Element of X1 : x in X1 } ;
A11: for x being set st x in X holds
x in Rank M by A5;
{ H2(x) where x is Element of X1 : x in X1 } c= M
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { H2(x) where x is Element of X1 : x in X1 } or y in M )
assume y in { H2(x) where x is Element of X1 : x in X1 } ; :: thesis: y in M
then consider x being Element of X1 such that
A12: y = the_rank_of x and
x in X1 ;
x in Rank M by A11;
hence y in M by A12, CLASSES1:66; :: thesis: verum
end;
then reconsider RANKS1 = { H2(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 A13: 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 { H2(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 { H2(x) where x is Element of X1 : x in X1 } & N1 c= C ) )
assume N1 in M ; :: thesis: ex C being Ordinal st
( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C )
then consider x being set such that
A14: x in X1 and
A15: not the_rank_of x in N1 by A13;
take C = the_rank_of x; :: thesis: ( C in { H2(x) where x is Element of X1 : x in X1 } & N1 c= C )
thus C in { H2(x) where x is Element of X1 : x in X1 } by A14; :: thesis: N1 c= C
thus N1 c= C by A15, ORDINAL1:16; :: thesis: verum
end;
then RANKS1 is unbounded by Th6;
then A16: cf M c= card RANKS1 by Th20;
card { H2(x) where x is Element of X1 : x in X1 } c= card X1 from TREES_2:sch 2();
 then M c= card X1 by A3, A16;
then card X1 in card X1 by A8;
hence contradiction ; :: thesis: verum
end;
then consider N1 being Ordinal such that
A17: N1 in M and
A18: for x being set st x in X1 holds
the_rank_of x in N1 ;
the_rank_of X c= N1 by A18, CLASSES1:69;
hence the_rank_of X in M by A17, ORDINAL1:12; :: thesis: verum
end;
hence contradiction by A7, CLASSES1:66; :: thesis: verum
end;
end;
end;