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