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)
(a "\/" b) ` = (((a `) `) "\/" b) ` by ROBBINS3:def 6
.= (((a `) `) "\/" ((b `) `)) ` by ROBBINS3:def 6
.= (((a `) "/\" (b `)) `) ` by Def1
.= (a `) "/\" (b `) by ROBBINS3:def 6 ;
hence - (a "\/" b) = (- a) "/\" (- b) ; :: thesis: verum