for L being Nelson_Algebra
for a, x, y being Element of L st x < y holds
a "/\" (a => x) < y