let G be finite Group; :: thesis: for q being Prime st q in support (prime_factorization (card G)) holds

ex a being Element of G st

( a <> 1_ G & ord a = q )

let q be Prime; :: thesis: ( q in support (prime_factorization (card G)) implies ex a being Element of G st

( a <> 1_ G & ord a = q ) )

assume q in support (prime_factorization (card G)) ; :: thesis: ex a being Element of G st

( a <> 1_ G & ord a = q )

then q in support (pfexp (card G)) by NAT_3:def 9;

then consider g being Element of G such that

A1: ord g = q by GROUP_10:11, NAT_3:36;

A2: 1 < q by INT_2:def 4;

take g ; :: thesis: ( g <> 1_ G & ord g = q )

thus ( g <> 1_ G & ord g = q ) by A1, A2, GROUP_1:42; :: thesis: verum

ex a being Element of G st

( a <> 1_ G & ord a = q )

let q be Prime; :: thesis: ( q in support (prime_factorization (card G)) implies ex a being Element of G st

( a <> 1_ G & ord a = q ) )

assume q in support (prime_factorization (card G)) ; :: thesis: ex a being Element of G st

( a <> 1_ G & ord a = q )

then q in support (pfexp (card G)) by NAT_3:def 9;

then consider g being Element of G such that

A1: ord g = q by GROUP_10:11, NAT_3:36;

A2: 1 < q by INT_2:def 4;

take g ; :: thesis: ( g <> 1_ G & ord g = q )

thus ( g <> 1_ G & ord g = q ) by A1, A2, GROUP_1:42; :: thesis: verum