:: deftheorem Def6 defines left_add-cancelable ALGSTR_0:def 6 :
for M being addMagma holds
( M is left_add-cancelable iff for x being Element of M holds x is left_add-cancelable );