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