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