for p being prime Nat
for G being finite Group
for H being Subgroup of G st G is p -group holds
expon (H,p) <= expon (G,p)