:: deftheorem Def1 defines ordinal-membered ORDINAL6:def 1 :
for X being set holds
( X is ordinal-membered iff ex a being Ordinal st X c= a );