:: deftheorem defines => NELSON_1:def 2 :
for L being non empty NelsonStr
for a, b being Element of L holds a => b = the Iimpl of L . (a,b);