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 ; :: thesis: (a * b) * c = a * (b * c)
H₁(H) c= H₁(G) by Th25;
then reconsider a' = a, b' = b, c' = c, ab = a * b, bc = b * c as Element of by TARSKI:def 3;
thus (a * b) * c = ab * c' by Th27
.= (a' * b') * c' by Th27
.= a' * (b' * c') by A1, Lm2
.= a' * bc by Th27
.= a * (b * c) by Th27 ; :: thesis: verum

end;

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