:: deftheorem defines = MEMBERED:def 15 :
for X, Y being real-membered set holds
( X = Y iff for r being Real holds
( r in X iff r in Y ) );