theorem Th2: :: ORDINAL6:2

for X being set holds
( X is ordinal-membered iff On X = X )