let X, Y be set ; :: thesis: ( Y in Rrank X iff ex Z being set st
( Z in X & Y in bool (Rrank Z) ) )
thus ( Y in Rrank X implies ex Z being set st
( Z in X & Y in bool (Rrank Z) ) ) :: thesis: ( ex Z being set st
( Z in X & Y in bool (Rrank Z) ) implies Y in Rrank X )

proof

assume Y in Rrank X ; :: thesis: ex Z being set st
( Z in X & Y in bool (Rrank Z) )
then consider B being Ordinal such that
A1: ( B in the_rank_of X & Y in bool (Rank B) ) by Th3;
consider a being set such that
A2: ( a in X & B c= the_rank_of a ) by A1, CLASSES1:70;
Rank B c= Rrank a by A2, CLASSES1:37;
then Y c= Rrank a by A1;
hence ex Z being set st
( Z in X & Y in bool (Rrank Z) ) by A2; :: thesis: verum

end;

given Z being set such that A3: ( Z in X & Y in bool (Rrank Z) ) ; :: thesis: Y in Rrank X
succ (the_rank_of Z) c= the_rank_of X by A3, CLASSES1:68, ORDINAL1:21;
then A4: Rank (succ (the_rank_of Z)) c= Rrank X by CLASSES1:37;
Y in Rank (succ (the_rank_of Z)) by A3, CLASSES1:30;
hence Y in Rrank X by A4; :: thesis: verum