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

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