theorem Th16: :: NELSON_1:22

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