let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (a "/\" (- a)) "/\" (b "\/" (- b)) = a "/\" (- a)
let a, b be Element of L; :: thesis: (a "/\" (- a)) "/\" (b "\/" (- b)) = a "/\" (- a)
(- b) "/\" (- (- b)) < (- a) "\/" a by Def13;
then - (b "\/" (- b)) < (- a) "\/" a by Th1;
then - (b "\/" (- b)) < (- a) "\/" (- (- a)) by ROBBINS3:def 6;
then - (b "\/" (- b)) < - (a "/\" (- a)) by Th8;
then a "/\" (- a) <= b "\/" (- b) by Th5, Def13;
hence (a "/\" (- a)) "/\" (b "\/" (- b)) = a "/\" (- a) ; :: thesis: verum