consider R being domRing;
take R ; :: thesis: ( R is Abelian & R is left_zeroed & R is right_zeroed & R is add-associative & R is right_complementable & R is well-unital & R is associative & R is commutative & R is distributive & R is domRing-like )
thus ( R is Abelian & R is left_zeroed & R is right_zeroed & R is add-associative & R is right_complementable & R is well-unital & R is associative & R is commutative & R is distributive & R is domRing-like ) ; :: thesis: verum