consider R being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ;
take R ; :: thesis: ( R is add-associative & R is right_zeroed & R is right_complementable & R is Abelian & R is commutative & R is associative & R is left_unital & R is distributive & R is almost_left_invertible & not R is degenerated )
thus ( R is add-associative & R is right_zeroed & R is right_complementable & R is Abelian & R is commutative & R is associative & R is left_unital & R is distributive & R is almost_left_invertible & not R is degenerated ) ; :: thesis: verum