take INT.Group p ; :: thesis: ( INT.Group p is p -group & INT.Group p is finite & INT.Group p is cyclic & INT.Group p is commutative & INT.Group p is strict )
thus ( INT.Group p is p -group & INT.Group p is finite & INT.Group p is cyclic & INT.Group p is commutative & INT.Group p is strict ) ; :: thesis: verum