let p be prime Nat; :: 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 Nat st
( card H = p |^ r & r <= expon (G,p) ) by Th2, GROUP_2:148;
hence expon (H,p) <= expon (G,p) by A1, Def2; :: thesis: verum