for G being Group
for a being Element of G holds gr {a} is cyclic Group