theorem :: GROUPP_1:23

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