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