let G be Group; :: thesis: for H being Subgroup of G st G is commutative Group holds
H is commutative
let H be Subgroup of G; :: thesis: ( G is commutative Group implies H is commutative )
assume A1: G is commutative Group ; :: thesis: H is commutative
thus for h1, h2 being Element of H holds h1 * h2 = h2 * h1 :: according to GROUP_1:def 12 :: thesis: verum

proof

let h1, h2 be Element of H; :: thesis: h1 * h2 = h2 * h1
reconsider g1 = h1, g2 = h2 as Element of G by Th42;
thus h1 * h2 = g1 * g2 by Th43
.= g2 * g1 by A1, Lm2
.= h2 * h1 by Th43 ; :: thesis: verum

end;