:: deftheorem Def3 defines satisfying_A1b NELSON_1:def 8 :
for L being non empty NelsonStr holds
( L is satisfying_A1b iff for a, b, c being Element of L st a < b & b < c holds
a < c );