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 :: thesis: for a, b, c being Element of H holds (a * b) * c = a * (b * c)

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

end;

hence H is associative ; :: thesis: verum