:: deftheorem defneg defines negative-disjoint REALALG1:def 7 :
for L being non empty addLoopStr
for S being Subset of L holds
( S is negative-disjoint iff S /\ (- S) = {(0. L)} );