theorem Th5: :: NELSON_1:9

for L being Nelson_Algebra
for a, b being Element of L holds
( a <= b iff ( a < b & - b < - a ) )