:: deftheorem Def2 defines satisfying_A1 NELSON_1:def 7 :
for L being non empty NelsonStr holds
( L is satisfying_A1 iff for a being Element of L holds a < a );