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