let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds a < (- (a "/\" b)) => (- b)
let a, b be Element of L; :: thesis: a < (- (a "/\" b)) => (- b)
((- a) "\/" (- b)) "/\" a < - b by Lm4;
then a < ((- a) "\/" (- b)) => (- b) by Def4;
hence a < (- (a "/\" b)) => (- b) by Th8; :: thesis: verum