theorem :: NELSON_1:31

for L being Nelson_Algebra
for a, b, c being Element of L st b < c holds
( a "\/" b < a "\/" c & a "/\" b < a "/\" c ) by Lm1;