take INT.Ring ; :: thesis: ( INT.Ring is strict & INT.Ring is infinite )
thus ( INT.Ring is strict & INT.Ring is infinite ) ; :: thesis: verum