for G being finite commutative Group
for m being Nat
for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal )