deffunc H2( set ) -> set = the_rank_of $1; set RANKS = { H2(x) where x is Element of X1 : x in X1 } ; A11:
for x being set st x in X holds x inRank M
byA5; { H2(x) where x is Element of X1 : x in X1 } c= M
then reconsider RANKS1 = { H2(x) where x is Element of X1 : x in X1 } as Subset of M ;
ex N1 being Ordinal st ( N1 in M & ( for x being set st x in X1 holds the_rank_of x in N1 ) )