theorem Th13: :: MONOID_0:13

for G being non empty multMagma holds
( G is cancelable iff for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c )