theorem Th31: :: CIRCCMB3:31

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