theorem Th4: :: CLASSES3:4

for X, Y being set holds
( Y in Rrank X iff ex Z being set st
( Z in X & Y in bool (Rrank Z) ) )