now :: thesis: not - a = 0. L

hence
not - a is zero
; :: thesis: verumassume
- a = 0. L
; :: thesis: contradiction

then - (- a) = 0. L by RLVECT_1:12;

hence contradiction by RLVECT_1:17; :: thesis: verum

end;then - (- a) = 0. L by RLVECT_1:12;

hence contradiction by RLVECT_1:17; :: thesis: verum