:: deftheorem Def4 defines satisfying_N3 NELSON_1:def 10 :
for L being non empty NelsonStr holds
( L is satisfying_N3 iff for x, a, b being Element of L holds
( a "/\" x < b iff x < a => b ) );