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 Th22;
hence INT.Group n is cyclic by Th17; :: thesis: verum