theorem Th5: :: GR_CY_1:5
for G being Group
for a, b being Element of G holds
( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )