let G be non empty multMagma ; :: thesis: ( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
thus ( G is cancelable implies ( G is left-cancelable & G is right-cancelable ) ) :: thesis: ( G is left-cancelable & G is right-cancelable implies G is cancelable )

proof

assume H₂(G) is cancelable ; :: according to MONOID_0:def 19 :: thesis: ( G is left-cancelable & G is right-cancelable )
hence ( H₂(G) is left-cancelable & H₂(G) is right-cancelable ) by Th2; :: according to MONOID_0:def 17,MONOID_0:def 18 :: thesis: verum

end;

assume ( H₂(G) is left-cancelable & H₂(G) is right-cancelable ) ; :: according to MONOID_0:def 17,MONOID_0:def 18 :: thesis: G is cancelable
hence H₂(G) is cancelable by Th2; :: according to MONOID_0:def 19 :: thesis: verum