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
A2: H₁(H) c= H₁(G) by Th25;

now

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

end;

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