take G = INT.Group ; :: thesis: ( not G is trivial & G is cyclic & G is strict & G is infinite )
thus ( not G is trivial & G is cyclic & G is strict & G is infinite ) ; :: thesis: verum