:: deftheorem Def7 defines right_add-cancelable ALGSTR_0:def 7 :
for M being addMagma holds
( M is right_add-cancelable iff for x being Element of M holds x is right_add-cancelable );