let R be non empty non degenerated right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: 0. R <> - (1. R)
assume 0. R = - (1. R) ; :: thesis: contradiction
then 0. R = - (- (1. R)) by RLVECT_1:12
.= 1. R by RLVECT_1:17 ;
hence contradiction ; :: thesis: verum