let p be natural prime number ; :: thesis: for G being finite Group
for H being Subgroup of G st G is p -group holds
expon (H,p) <= expon (G,p)
let G be finite Group; :: thesis: for H being Subgroup of G st G is p -group holds
expon (H,p) <= expon (G,p)
let H be Subgroup of G; :: thesis: ( G is p -group implies expon (H,p) <= expon (G,p) )
assume A1: G is p -group ; :: thesis: expon (H,p) <= expon (G,p)
then card G = p |^ (expon (G,p)) by def2;
then ex r being natural number st
( card H = p |^ r & r <= expon (G,p) ) by GROUP_2:178, Th2;
hence expon (H,p) <= expon (G,p) by A1, def2; :: thesis: verum