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