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