:: deftheorem defines =-> NELSON_1:def 21 :
for L being non empty bounded satisfying_N4 NelsonStr
for a, b being Element of L holds a =-> b = (a => b) "/\" ((- b) => (- a));