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