let X be set ; :: thesis: ( the_rank_of X is finite implies X is finite )
assume the_rank_of X is finite ; :: thesis: X is finite
then the_rank_of X in NAT by CARD_1:61;
then A1: Rank (the_rank_of X) is finite by CARD_2:67;
X c= Rank (the_rank_of X) by CLASSES1:def 9;
hence X is finite by A1; :: thesis: verum