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