let n be non zero Nat; :: thesis: ( INT.Group n is trivial iff n = 1 )
( INT.Group n is trivial iff card (INT.Group n) = 1 ) by ThTrivialCriterion;
hence ( INT.Group n is trivial iff n = 1 ) ; :: thesis: verum