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

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