let p be Element of NAT ; :: thesis: for G being finite strict Group st p is prime & card G = p holds

ex a being Element of G st ord a = p

let G be finite strict Group; :: thesis: ( p is prime & card G = p implies ex a being Element of G st ord a = p )

assume that

A1: p is prime and

A2: card G = p ; :: thesis: ex a being Element of G st ord a = p

G is cyclic Group by A1, A2, GR_CY_1:21;

hence ex a being Element of G st ord a = p by A2, GR_CY_1:19; :: thesis: verum

ex a being Element of G st ord a = p

let G be finite strict Group; :: thesis: ( p is prime & card G = p implies ex a being Element of G st ord a = p )

assume that

A1: p is prime and

A2: card G = p ; :: thesis: ex a being Element of G st ord a = p

G is cyclic Group by A1, A2, GR_CY_1:21;

hence ex a being Element of G st ord a = p by A2, GR_CY_1:19; :: thesis: verum