take INT.Ring ; :: thesis: ( INT.Ring is strict & not INT.Ring is finite & INT.Ring is good )
thus ( INT.Ring is strict & not INT.Ring is finite & INT.Ring is good ) ; :: thesis: verum