:: deftheorem defines [#] SUBSET_1:def 3 :
for E being set holds [#] E = E;