:: deftheorem defines satisfying_N9* NELSON_1:def 30 :
for L being non empty NelsonStr holds
( L is satisfying_N9* iff for a, b being Element of L holds (a "/\" b) => a = Top L );