for G being finite Group holds
( G is cyclic iff ex a being Element of G st ord a = card G )