:: deftheorem defines {} SUBSET_1:def 2 :
for E being set holds {} E = {} ;