:: deftheorem defines add-unital GROUP_1A:def 1 :
for IT being addMagma holds
( IT is add-unital iff ex e being Element of IT st
for h being Element of IT holds
( h + e = h & e + h = h ) );