let H be Subgroup of G; :: thesis: H is p -group
consider m being Nat such that
A1: card G = p |^ m by GROUP_10:def 17;
ex r being Nat st
( card H = p |^ r & r <= m ) by A1, Th2, GROUP_2:148;
hence H is p -group ; :: thesis: verum