let G be strict Group; :: thesis: for N being strict normal Subgroup of G st G is commutative holds

G ./. N is commutative

let N be strict normal Subgroup of G; :: thesis: ( G is commutative implies G ./. N is commutative )

assume G is commutative ; :: thesis: G ./. N is commutative

then G ` = (1). G by GROUP_5:75;

then G ` = (1). N by GROUP_2:63;

hence G ./. N is commutative by GROUP_6:30; :: thesis: verum

G ./. N is commutative

let N be strict normal Subgroup of G; :: thesis: ( G is commutative implies G ./. N is commutative )

assume G is commutative ; :: thesis: G ./. N is commutative

then G ` = (1). G by GROUP_5:75;

then G ` = (1). N by GROUP_2:63;

hence G ./. N is commutative by GROUP_6:30; :: thesis: verum