:: deftheorem defines = MEMBERED:def 18 :
for X, Y being natural-membered set holds
( X = Y iff for n being Nat holds
( n in X iff n in Y ) );