theorem ThTrivialCyclicGroupCriterion: :: GROUP_24:76

for n being non zero Nat holds
( not INT.Group n is trivial iff n > 1 ) by NAT_1:53, ThTrivialCyclicGroupCriterion1;