theorem Th21: :: ORDINAL1:25

for X being set holds
not for x being set holds
( x in X iff x is Ordinal )