:: deftheorem defines cancelable MONOID_0:def 8 :
for D being non empty set
for IT being BinOp of D holds
( IT is cancelable iff for a, b, c being Element of D st ( IT . (a,b) = IT . (a,c) or IT . (b,a) = IT . (c,a) ) holds
b = c );