take G = INT.Group 2; :: thesis: ( not G is trivial & G is cyclic & G is strict & G is finite )
thus ( not G is trivial & G is cyclic & G is strict & G is finite ) by ThTrivialCyclicGroupCriterion; :: thesis: verum