take INT.Ring ; :: thesis: ( INT.Ring is strict & INT.Ring is Euclidian & INT.Ring is domRing-like & not INT.Ring is degenerated & INT.Ring is distributive & INT.Ring is commutative )
thus ( INT.Ring is strict & INT.Ring is Euclidian & INT.Ring is domRing-like & not INT.Ring is degenerated & INT.Ring is distributive & INT.Ring is commutative ) ; :: thesis: verum