:: deftheorem defines = MEMBERED:def 13 :
for X, Y being complex-membered set holds
( X = Y iff for c being Complex holds
( c in X iff c in Y ) );