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

now

let a, b be Element of H; :: thesis: a * b = b * a
H₁(H) c= H₁(G) by Th25;
then reconsider a' = a, b' = b as Element of G by TARSKI:def 3;
thus a * b = a' * b' by Th27
.= b' * a' by A1, Lm1
.= b * a by Th27 ; :: thesis: verum

end;

hence H is commutative by Lm1; :: thesis: verum