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