:: deftheorem defines @ ENS_1:def 16 :
for V being non empty set
for m being Element of Maps V holds @ m = m;