let n be Nat; :: thesis: ( n > 0 implies INT.Group n is cyclic )
assume n > 0 ; :: thesis: INT.Group n is cyclic
then ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 by Th46;
hence INT.Group n is cyclic by Th41; :: thesis: verum