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