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)
- (b "\/" (- b)) = (- b) "/\" (- (- b)) by Th1
.= b "/\" (- b) by ROBBINS3:def 6 ;
then - (b "\/" (- b)) < - (a "/\" (- a)) by Def13;
hence a "/\" (- a) <= b "\/" (- b) by Def13, Th5; :: thesis: verum