:: deftheorem defines = MEMBERED:def 17 :
for X, Y being integer-membered set holds
( X = Y iff for i being Integer holds
( i in X iff i in Y ) );