let L be Nelson_Algebra; :: thesis: for a, x, y being Element of L st x < y holds
a => x < a => y
let a, x, y be Element of L; :: thesis: ( x < y implies a => x < a => y )
assume x < y ; :: thesis: a => x < a => y
then a "/\" (a => x) < y by Th16;
hence a => x < a => y by Def4; :: thesis: verum