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
A2: Y c= Rank (the_rank_of Y) by Def8;
thus the_rank_of X in the_rank_of Y by A1, A2, Th74; :: thesis: verum