:: deftheorem Def7 defines In SUBSET_1:def 8 :
for x being object
for X being set st x in X holds
In (x,X) = x;