:: deftheorem defines ` SUBSET_1:def 4 :
for E being set
for A being Subset of E holds A ` = E \ A;