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