:: deftheorem Def7 defines cyclic GR_CY_1:def 7 :
for IT being Group holds
( IT is cyclic iff ex a being Element of IT st multMagma(# the carrier of IT, the multF of IT #) = gr {a} );