let A be non empty set ; :: thesis: RRing A is commutative Ring
A1: RRing A is Abelian by Th25;
A2: RRing A is add-associative by Th25;
A3: RRing A is right_complementable
proof
let x be Element of (RRing A); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
consider t being Element of (RRing A) such that
A4: x + t = 0. (RRing A) by Th25;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. (RRing A)
thus x + t = 0. (RRing A) by A4; :: thesis: verum
end;
A5: RRing A is right_zeroed by Th25;
A6: RRing A is distributive by Th25;
A7: RRing A is well-unital by Th25;
A8: RRing A is associative by Th25;
RRing A is commutative by Th25;
hence RRing A is commutative Ring by A1, A2, A5, A3, A8, A7, A6; :: thesis: verum