let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds ((- a) "\/" (- b)) "/\" a < - b
let a, b be Element of L; :: thesis: ((- a) "\/" (- b)) "/\" a < - b
(- b) "/\" a <= - b by LATTICES:4, LATTICES:6;
then A1: (- b) "/\" a < - b by Th5;
(- a) "/\" a < - b by Def13;
then ((- a) "/\" a) "\/" ((- b) "/\" a) < (- b) "\/" (- b) by A1, Lm2;
hence ((- a) "\/" (- b)) "/\" a < - b by LATTICES:def 11; :: thesis: verum