:: deftheorem defines satisfying_N17* NELSON_1:def 37 :
for L being non empty NelsonStr holds
( L is satisfying_N17* iff for a, b being Element of L holds - (a "\/" b) = (- a) "/\" (- b) );