:: deftheorem Def7 defines satisfying_N6 NELSON_1:def 13 :
for L being non empty NelsonStr holds
( L is satisfying_N6 iff for a, b, c being Element of L st a < c & b < c holds
a "\/" b < c );