:: deftheorem Def13 defines satisfying_N12 NELSON_1:def 19 :
for L being non empty NelsonStr holds
( L is satisfying_N12 iff for a, b being Element of L holds a "/\" (- a) < b );