take INT.Ring ; :: thesis: ( INT.Ring is Euclidian & INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is well-unital & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & not INT.Ring is degenerated )
thus ( INT.Ring is Euclidian & INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is well-unital & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & not INT.Ring is degenerated ) ; :: thesis: verum