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 Th23;

now :: thesis: for a, b, c being Element of H st ( a * b = a * c or b * a = c * a ) holds
b = c

let a, b, c be Element of H; :: thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
reconsider a9 = a, b9 = b, c9 = c as Element of G by A2;
A3: ( b * a = b9 * a9 & c * a = c9 * a9 ) by Th25;
( a * b = a9 * b9 & a * c = a9 * c9 ) by Th25;
hence ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A1, A3, Th13; :: thesis: verum

end;

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