for G being finite Group
for p being prime Nat
for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds
G is commutative