let G be Group; :: thesis: for H being strict Subgroup of G st G is commutative Group holds
H is normal
let H be strict Subgroup of G; :: thesis: ( G is commutative Group implies H is normal )
assume G is commutative Group ; :: thesis: H is normal
hence for a being Element of G holds H |^ a = multMagma(# the carrier of H, the multF of H #) by Th86; :: according to GROUP_3:def 13 :: thesis: verum