:: deftheorem Def3 defines real-membered MEMBERED:def 3 :
for X being set holds
( X is real-membered iff for x being object st x in X holds
x is real );