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

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

end;

hence H is commutative ; :: thesis: verum