theorem Th3: :: CLASSES3:3

for X being set
for A being Ordinal holds
( X in Rank A iff ex B being Ordinal st
( B in A & X in bool (Rank B) ) )