let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x))
let x, y be Element of G; :: thesis: \delta (x,(- y)) = \delta (y,(- x))
thus \delta (x,(- y)) = - ((- x) + (- y))
.= \delta (y,(- x)) ; :: thesis: verum