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