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