let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G st G is cancelable holds
H is cancelable
let H be non empty SubStr of G; :: thesis: ( G is cancelable implies H is cancelable )
assume A1: G is cancelable ; :: thesis: H is cancelable
then A2: ( H₁(H) c= H₁(G) & ( for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ) ) by Th15, Th25;

now

let a, b, c be Element of H; :: thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
reconsider a' = a, b' = b, c' = c as Element of G by A2, TARSKI:def 3;
( a * b = a' * b' & a * c = a' * c' & b * a = b' * a' & c * a = c' * a' ) by Th27;
hence ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A1, Th15; :: thesis: verum

end;

hence H is cancelable by Th15; :: thesis: verum