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