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