theorem :: CLASSES1:45

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