:: deftheorem defines c= MEMBERED:def 10 :
for X being rational-membered set
for Y being set holds
( X c= Y iff for w being Rational st w in X holds
w in Y );