let X, Y be set ; :: thesis: ( X in Y implies the_rank_of X in the_rank_of Y )
assume A1: X in Y ; :: thesis: the_rank_of X in the_rank_of Y
Y c= Rank (the_rank_of Y) by Def9;
hence the_rank_of X in the_rank_of Y by A1, Th66; :: thesis: verum