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