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