for n being Element of NAT
for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )