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 H2(G) is cancelable ; :: according to MONOID_0:def 19 :: thesis: ( G is left-cancelable & G is right-cancelable )
hence ( H2(G) is left-cancelable & H2(G) is right-cancelable ) ; :: according to MONOID_0:def 17,MONOID_0:def 18 :: thesis: verum
end;
assume ( H2(G) is left-cancelable & H2(G) is right-cancelable ) ; :: according to MONOID_0:def 17,MONOID_0:def 18 :: thesis: G is cancelable
hence H2(G) is cancelable ; :: according to MONOID_0:def 19 :: thesis: verum