theorem :: CLASSES3:5

for X being set
for x, y being object st x in X & y in Rrank x holds
y in Rrank X