for G being finite cyclic Group
for n, m being Nat st card G = n * m holds
ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G )