theorem :: CLASSES1:84

for x, y being set holds
( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )