:: deftheorem defines @ ENS_1:def 15 :
for V being non empty set
for a being Object of (Ens V) holds @ a = a;