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