set R = the non degenerated comRing;
take the non degenerated comRing ; :: thesis: ( the non degenerated comRing is Abelian & the non degenerated comRing is left_zeroed & the non degenerated comRing is right_zeroed & the non degenerated comRing is add-cancelable & the non degenerated comRing is well-unital & the non degenerated comRing is add-associative & the non degenerated comRing is associative & the non degenerated comRing is commutative & the non degenerated comRing is distributive )
thus ( the non degenerated comRing is Abelian & the non degenerated comRing is left_zeroed & the non degenerated comRing is right_zeroed & the non degenerated comRing is add-cancelable & the non degenerated comRing is well-unital & the non degenerated comRing is add-associative & the non degenerated comRing is associative & the non degenerated comRing is commutative & the non degenerated comRing is distributive ) ; :: thesis: verum