theorem ThTrivialCyclicGroupCriterion1: :: GROUP_24:75

for n being non zero Nat holds
( INT.Group n is trivial iff n = 1 )