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