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:103;
then A1: Rank (the_rank_of X) is finite by CARD_3:57;
X c= Rank (the_rank_of X) by CLASSES1:def 8;
hence X is finite by A1; :: thesis: verum