for X, Y being set st Y in Rrank X holds
ex x being object st
( x in X & Y c= Rrank x )