let L be Nelson_Algebra; :: thesis: for x, y, z being Element of L st - x < - y holds
- (z => x) < - (z => y)
let x, y, z be Element of L; :: thesis: ( - x < - y implies - (z => x) < - (z => y) )
assume A1: - x < - y ; :: thesis: - (z => x) < - (z => y)
A2: - (z => x) < z "/\" (- x) by Def10;
z "/\" (- x) < z "/\" (- y) by A1, Lm1;
then A3: - (z => x) < z "/\" (- y) by A2, Def3;
z "/\" (- y) < - (z => y) by Def9;
hence - (z => x) < - (z => y) by A3, Def3; :: thesis: verum