consider R being non degenerated comRing;
take R ; :: thesis: ( R is add-associative & R is left_zeroed & R is right_zeroed )
thus ( R is add-associative & R is left_zeroed & R is right_zeroed ) ; :: thesis: verum