let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G st G is associative holds
H is associative
let H be non empty SubStr of G; :: thesis: ( G is associative implies H is associative )
assume A1: G is associative ; :: thesis: H is associative

now

let a, b, c be Element of H; :: thesis: (a * b) * c = a * (b * c)
H₁(H) c= H₁(G) by Th25;
then reconsider a9 = a, b9 = b, c9 = c, ab = a * b, bc = b * c as Element of G by TARSKI:def 3;
thus (a * b) * c = ab * c9 by Th27
.= (a9 * b9) * c9 by Th27
.= a9 * (b9 * c9) by A1, Lm2
.= a9 * bc by Th27
.= a * (b * c) by Th27 ; :: thesis: verum

end;

hence H is associative by Lm2; :: thesis: verum