:: deftheorem defines satisfying_N5* NELSON_1:def 26 :
for L being non empty NelsonStr holds
( L is satisfying_N5* iff for a, b being Element of L holds (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a) );