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

assume - a = 0. L ; :: thesis: contradiction
then - (- a) = 0. L by RLVECT_1:12;
hence contradiction by RLVECT_1:17; :: thesis: verum

end;

hence not - a is zero ; :: thesis: verum