:: deftheorem defines left-cancelable MONOID_0:def 17 :
for IT being non empty multMagma holds
( IT is left-cancelable iff the multF of IT is left-cancelable );