now

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 by STRUCT_0:def 12; :: thesis: verum