let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds - (b =-> (a "/\" b)) < - a
let a, b be Element of L; :: thesis: - (b =-> (a "/\" b)) < - a
A1: ((- b) "\/" (- a)) "/\" b < - a by Lm4;
then A2: (- (a "/\" b)) "/\" b < - a by Th8;
- ((- (a "/\" b)) => (- b)) < (- (a "/\" b)) "/\" (- (- b)) by Def10;
then - ((- (a "/\" b)) => (- b)) < (- (a "/\" b)) "/\" b by ROBBINS3:def 6;
then A3: - ((- (a "/\" b)) => (- b)) < - a by A2, Def3;
A4: b "/\" (- (b "/\" a)) < - a by A1, Th8;
- (b => (a "/\" b)) < b "/\" (- (a "/\" b)) by Def10;
then A5: - (b => (a "/\" b)) < - a by A4, Def3;
- (b =-> (a "/\" b)) = (- ((- (a "/\" b)) => (- b))) "\/" (- (b => (a "/\" b))) by Th8;
hence - (b =-> (a "/\" b)) < - a by A3, A5, Def7; :: thesis: verum