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