:: deftheorem defines @ ENS_1:def 14 :
for V being non empty set
for A being Element of V holds @ A = A;