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