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 9;
set a = the_rank_of X;
A2: the_rank_of X c= succ (the_rank_of X) by ORDINAL3:1;
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 A2;
then A3: Rank (the_rank_of X) c= Rank (succ (succ (the_rank_of X))) by CLASSES1:37;
now :: thesis: for x, y being set st [x,y] in Rank (the_rank_of X) holds
x c= Rank (the_rank_of X)
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 A3, CLASSES1:45;
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, Def1;
hence the_rank_of (varcl X) c= the_rank_of X by CLASSES1:65; :: according to XBOOLE_0:def 10 :: thesis: the_rank_of X c= the_rank_of (varcl X)
X c= varcl X by Def1;
hence the_rank_of X c= the_rank_of (varcl X) by CLASSES1:67; :: thesis: verum