per cases ( Rank (the_rank_of X) is Universe or not Rank (the_rank_of X) is Universe ) ;

suppose Rank (the_rank_of X) is Universe ; :: thesis: ex b₁ being Universe st
( X c= b₁ & ( for Y being Universe st X c= Y holds
b₁ c= Y ) )

then reconsider R = Rank (the_rank_of X) as Universe ;
take R ; :: thesis: ( X c= R & ( for Y being Universe st X c= Y holds
R c= Y ) )
thus X c= R by CLASSES1:def 9; :: thesis: for Y being Universe st X c= Y holds
R c= Y
let Y be Universe; :: thesis: ( X c= Y implies R c= Y )
assume X c= Y ; :: thesis: R c= Y
then the_rank_of X c= the_rank_of Y by CLASSES1:67;
then A1: R c= Rank (the_rank_of Y) by CLASSES1:37;
A2: Rank (card Y) = Y by Th31;
then the_rank_of Y c= card Y by CLASSES1:def 9;
then Rank (the_rank_of Y) c= Y by A2, CLASSES1:37;
hence R c= Y by A1; :: thesis: verum

end;

suppose A3: Rank (the_rank_of X) is not Universe ; :: thesis: ex b₁ being Universe st
( X c= b₁ & ( for Y being Universe st X c= Y holds
b₁ c= Y ) )

take R = Tarski-Class (Rank (the_rank_of X)); :: thesis: ( X c= R & ( for Y being Universe st X c= Y holds
R c= Y ) )
A4: Rank (the_rank_of X) in R by CLASSES1:2;
X c= Rank (the_rank_of X) by CLASSES1:def 9;
then X in R by A4, CLASSES1:def 1;
hence X c= R by ORDINAL1:def 2; :: thesis: for Y being Universe st X c= Y holds
R c= Y
let Y be Universe; :: thesis: ( X c= Y implies R c= Y )
assume X c= Y ; :: thesis: R c= Y
then A5: the_rank_of X c= the_rank_of Y by CLASSES1:67;
A6: Rank (card Y) = Y by Th31;
then A7: the_rank_of Y c= card Y by CLASSES1:def 9;
Y c= Rank (the_rank_of Y) by CLASSES1:def 9;
then card Y c= the_rank_of Y by A6, CLASSES1:37;
then card Y = the_rank_of Y by A7;
then the_rank_of X c< card Y by A3, A5, A6;
then the_rank_of X in card Y by ORDINAL1:11;
then Rank (the_rank_of X) in Y by A6, CLASSES1:36;
then Y is_Tarski-Class_of Rank (the_rank_of X) ;
hence R c= Y by CLASSES1:def 4; :: thesis: verum

end;

end;