let X, Y be set ; :: thesis: ( Y in Rrank X implies ex x being object st

( x in X & Y c= Rrank x ) )

assume Y in Rrank X ; :: thesis: ex x being object st

( x in X & Y c= Rrank x )

then ex Z being set st

( Z in X & Y in bool (Rrank Z) ) by Th4;

hence ex x being object st

( x in X & Y c= Rrank x ) ; :: thesis: verum

( x in X & Y c= Rrank x ) )

assume Y in Rrank X ; :: thesis: ex x being object st

( x in X & Y c= Rrank x )

then ex Z being set st

( Z in X & Y in bool (Rrank Z) ) by Th4;

hence ex x being object st

( x in X & Y c= Rrank x ) ; :: thesis: verum