:: deftheorem Def5 defines satisfying_N4 NELSON_1:def 11 :
for L being non empty NelsonStr holds
( L is satisfying_N4 iff for a, b being Element of L holds a =-> b = (a => b) "/\" ((- b) => (- a)) );