:: deftheorem defines c= MEMBERED:def 8 :
for X being ext-real-membered set
for Y being set holds
( X c= Y iff for e being ExtReal st e in X holds
e in Y );