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