per cases ;

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 8; :: thesis:
let Y be Universe; :: thesis:
assume X c= Y ; :: thesis:
then the_rank_of X c= the_rank_of Y by CLASSES1:75;
then A2: R c= Rank (the_rank_of Y) by CLASSES1:43;
A3: Rank (card Y) = Y by Th32;
then the_rank_of Y c= card Y by CLASSES1:def 8;
then Rank (the_rank_of Y) c= Y by A3, CLASSES1:43;
hence R c= Y by A2, XBOOLE_1:1; :: thesis:

end;

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

take R = Tarski-Class (Rank (the_rank_of X)); :: thesis:
( X c= Rank (the_rank_of X) & Rank (the_rank_of X) in R ) by CLASSES1:5, CLASSES1:def 8;
then X in R by 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:75;
A6: ( Rank (card Y) = Y & Y c= Rank (the_rank_of Y) ) by Th32, CLASSES1:def 8;
then ( card Y c= the_rank_of Y & the_rank_of Y c= card Y ) by CLASSES1:43, CLASSES1:def 8;
then card Y = the_rank_of Y by XBOOLE_0:def 10;
then the_rank_of X c< card Y by A4, A5, A6, XBOOLE_0:def 8;
then the_rank_of X in card Y by ORDINAL1:21;
then Rank (the_rank_of X) in Y by A6, CLASSES1:42;
then Y is_Tarski-Class_of Rank (the_rank_of X) by CLASSES1:def 3;
hence R c= Y by CLASSES1:def 4; :: thesis:

end;

end;