:: deftheorem defines = FILTER_2:def 1 :
for D being non empty set
for X1, X2 being Subset of D holds
( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) );