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 )

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

( 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

given Z being set such that A3:
( Z in X & Y in bool (Rrank Z) )
; :: thesis: Y in Rrank X
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;( 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

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