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