let G be finite Group; :: thesis: for p being natural prime number st p divides card G holds
ex g being Element of st ord g = p
let p be natural prime number ; :: thesis: ( p divides card G implies ex g being Element of st ord g = p )
reconsider p' = p as prime Element of NAT by ORDINAL1:def 13;
A1: 1 < p' by NAT_4:12;
consider P being strict Subgroup of G such that
A2: P is_Sylow_p-subgroup_of_prime p by Th12;
P is_p-group_of_prime p by A2, Def19;
then consider H being finite Group such that
A3: P = H and
A4: H is_p-group_of_prime p by Def18;
consider r being natural number such that
A5: card H = p |^ r by A4, Def17;
assume A6: p divides card G ; :: thesis: ex g being Element of st ord g = p

now

assume r = 0 ; :: thesis: contradiction
then card H = 1 by A5, NEWTON:9;
then card G = 1 * (index P) by A3, GROUP_2:177;
hence contradiction by A6, A2, Def19; :: thesis: verum

end;

then 0 + 1 < r + 1 by XREAL_1:8;
then 1 <= r by NAT_1:13;
then 1 - 1 <= r - 1 by XREAL_1:11;
then reconsider r' = r - 1 as Element of NAT by INT_1:16;
0 + 1 < (p' |^ r') + 1 by XREAL_1:8;
then 1 <= p |^ r' by NAT_1:13;
then A7: 1 * p <= (p |^ r') * p by XREAL_1:66;
set H' = (Omega). H;
A8: card H = (card ((Omega). H)) * (index ((Omega). H)) by GROUP_2:177
.= (card ((Omega). H)) * 1 by GROUP_2:180 ;
p |^ r = p |^ (r' + 1)
.= (p |^ r') * p by NEWTON:11 ;
then card ((Omega). H) > 1 by A5, A7, A1, XXREAL_0:2;
then consider g being Element of such that
A9: g <> 1_ ((Omega). H) by GR_CY_1:31;
reconsider H'' = gr {g} as strict Group ;
A10: H'' is cyclic Group by GR_CY_2:10;
reconsider H'' = H'' as finite strict Group ;
set n = card H'';

A11: now

assume card H'' = 1 ; :: thesis: contradiction
then ord g = 1 by GR_CY_1:27;
hence contradiction by A9, GROUP_1:85; :: thesis: verum

end;

card H'' >= 1 by GROUP_1:90;
then card H'' > 1 by A11, XXREAL_0:1;
then p divides card H'' by A5, A8, Lm8, GROUP_2:178;
then consider H''' being strict Subgroup of H'' such that
A12: card H''' = p' and
for G2 being strict Subgroup of H'' st card G2 = p' holds
G2 = H''' by A10, GR_CY_2:28;
consider h' being Element of such that
A13: ord h' = p by A12, GROUP_8:1;
H'' is Subgroup of G by A3, GROUP_2:65;
then reconsider H''' = H''' as strict Subgroup of G by GROUP_2:65;
reconsider h' = h' as Element of ;
reconsider h = h' as Element of by GROUP_2:51;
take h ; :: thesis: ord h = p
thus ord h = p by A13, GROUP_8:5; :: thesis: verum