:: deftheorem defines c= MEMBERED:def 12 :
for X being natural-membered set
for Y being set holds
( X c= Y iff for n being Nat st n in X holds
n in Y );