:: deftheorem defines <= NELSON_1:def 4 :
for L being non empty NelsonStr
for a, b being Element of L holds
( a <= b iff a = a "/\" b );