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