:: deftheorem defines c= MEMBERED:def 11 :
for X being integer-membered set
for Y being set holds
( X c= Y iff for i being Integer st i in X holds
i in Y );