:: deftheorem defines left_add-cancelable ALGSTR_0:def 3 :
for M being addMagma
for x being Element of M holds
( x is left_add-cancelable iff for y, z being Element of M st x + y = x + z holds
y = z );