:: deftheorem defines @ NAT_LAT:def 11 :
for m being Element of NatPlus_Lattice holds @ m = m;