let R be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x being Element of R holds
( x = 0. R iff - x = 0. R )
let x be Element of R; :: thesis: ( x = 0. R iff - x = 0. R )
thus ( x = 0. R implies - x = 0. R ) by RLVECT_1:12; :: thesis: ( - x = 0. R implies x = 0. R )
assume - x = 0. R ; :: thesis: x = 0. R
then - (- x) = 0. R by RLVECT_1:12;
hence x = 0. R by RLVECT_1:17; :: thesis: verum