now

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

end;

hence not - a is zero by STRUCT_0:def 12; :: thesis: verum