:: deftheorem defines satisfying_N14* NELSON_1:def 35 :
for L being non empty NelsonStr holds
( L is satisfying_N14* iff for a, b being Element of L holds (- a) => (a => b) = Top L );