let X be set ; :: thesis: for x, y being object st x in X & y in Rrank x holds
y in Rrank X
let x, y be object ; :: thesis: ( x in X & y in Rrank x implies y in Rrank X )
assume A1: ( x in X & y in Rrank x ) ; :: thesis: y in Rrank X
reconsider x = x, y = y as set by TARSKI:1;
the_rank_of x in the_rank_of X by A1, CLASSES1:68;
then Rrank x c= Rrank X by ORDINAL1:def 2, CLASSES1:36;
hence y in Rrank X by A1; :: thesis: verum