let p be prime Nat; :: thesis: for G being finite Group st ( for a being Element of G holds a is p -power ) holds
G is p -group
let G be finite Group; :: thesis: ( ( for a being Element of G holds a is p -power ) implies G is p -group )
assume A1: for a being Element of G holds a is p -power ; :: thesis: G is p -group
assume not G is p -group ; :: thesis: contradiction
then for r being Nat holds card G <> p |^ r ;
then consider s being Element of NAT such that
A2: ( s is prime & s divides card G ) and
A3: s <> p by Th1;
consider b being Element of G such that
A4: ord b = s by A2, GROUP_10:11;
b is p -power by A1;
then ex r1 being Nat st ord b = p |^ r1 ;
hence contradiction by A2, A4, A3, NAT_3:6; :: thesis: verum