let p be natural prime number ; :: thesis: for G being finite Group
for H being Subgroup of G
for a being Element of G st H is p -group & a in H holds
a is p -element
let G be finite Group; :: thesis: for H being Subgroup of G
for a being Element of G st H is p -group & a in H holds
a is p -element
let H be Subgroup of G; :: thesis: for a being Element of G st H is p -group & a in H holds
a is p -element
let a be Element of G; :: thesis: ( H is p -group & a in H implies a is p -element )
assume that
A1: H is p -group and
A2: a in H ; :: thesis: a is p -element
a is Element of H by A2, STRUCT_0:def 5;
then consider b being Element of H such that
A5: b = a ;
consider r being natural number such that
A6: ord b = p |^ r by A1, def1;
ord a = p |^ r by A5, GROUP_8:5, A6;
hence a is p -element by def1; :: thesis: verum