for L being Nelson_Algebra
for a being Element of L holds - (- a) = a by ROBBINS3:def 6;