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