let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: 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