for p being prime Nat
for G being finite Group
for H being Subgroup of G
for a being Element of G st H is p -group & a in H holds
a is p -power