let X be set ; :: thesis: the_rank_of (varcl X) = the_rank_of X
A1: X c= Rank (the_rank_of X) by CLASSES1:def 8;
set a = the_rank_of X;
( the_rank_of X c= succ (the_rank_of X) & succ (the_rank_of X) c= succ (succ (the_rank_of X)) ) by ORDINAL3:1;
then the_rank_of X c= succ (succ (the_rank_of X)) by XBOOLE_1:1;
then A2: Rank (the_rank_of X) c= Rank (succ (succ (the_rank_of X))) by CLASSES1:43;

now

let x, y be set ; :: thesis: ( [x,y] in Rank (the_rank_of X) implies x c= Rank (the_rank_of X) )
assume [x,y] in Rank (the_rank_of X) ; :: thesis: x c= Rank (the_rank_of X)
then x in Rank (the_rank_of X) by A2, CLASSES1:51;
hence x c= Rank (the_rank_of X) by ORDINAL1:def 2; :: thesis: verum

end;

then varcl X c= Rank (the_rank_of X) by A1, VARCL;
hence the_rank_of (varcl X) c= the_rank_of X by CLASSES1:73; :: according to XBOOLE_0:def 10 :: thesis: the_rank_of X c= the_rank_of (varcl X)
X c= varcl X by VARCL;
hence the_rank_of X c= the_rank_of (varcl X) by CLASSES1:75; :: thesis: verum