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