let L be Nelson_Algebra; :: thesis: for a, x, y being Element of L st x < y holds
a "/\" (a => x) < y
let a, x, y be Element of L; :: thesis: ( x < y implies a "/\" (a => x) < y )
assume A1: x < y ; :: thesis: a "/\" (a => x) < y
A2: a "/\" (a => x) = a "/\" ((- a) "\/" x) by Th14;
A3: a "/\" ((- a) "\/" x) = (a "/\" (- a)) "\/" (a "/\" x) by LATTICES:def 11;
A4: a "/\" x < x by Th6;
a "/\" (- a) < x by Def13;
then a "/\" (a => x) < x by A3, A2, A4, Def7;
hence a "/\" (a => x) < y by A1, Def3; :: thesis: verum