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 A1: ( p is prime & card G = p ) ; :: thesis: ex a being Element of G st ord a = p
then G is cyclic Group by GR_CY_1:45;
hence ex a being Element of G st ord a = p by A1, GR_CY_1:43; :: thesis: verum