suppose Rank (the_rank_of X) is Universe ; :: thesis:

then reconsider R = Rank (the_rank_of X) as Universe ;
take R ; :: thesis:
thus X c= R by CLASSES1:def 9; :: thesis:
let Y be Universe; :: thesis:
assume X c= Y ; :: thesis:
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:

end;

suppose A3: Rank (the_rank_of X) is not Universe ; :: thesis:

take R = Tarski-Class (Rank (the_rank_of X)); :: thesis:
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:
let Y be Universe; :: thesis:
assume X c= Y ; :: thesis:
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:

end;

end;