:: deftheorem Def6 defines natural-membered MEMBERED:def 6 :
for X being set holds
( X is natural-membered iff for x being object st x in X holds
x is natural );