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

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