theorem Th1: :: ORDINAL6:1

for X being set holds
( X is ordinal-membered iff for x being set st x in X holds
x is ordinal )