theorem Th44: :: CLASSES1:44

for x, y being set
for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )