let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3))
let x be Element of G; :: thesis: \delta ((\beta x),x) = - ((x _1) + (x _3))
thus - ((x _1) + (x _3)) = \delta (((- ((x _1) + (x _3))) + (x + (- (x _3)))),(\delta ((x + (- (x _3))),(- ((x _1) + (x _3)))))) by Th36
.= \delta ((\beta x),(\delta ((x + (- (x _3))),(- ((x _1) + (x _3)))))) by LATTICES:def 5
.= \delta ((\beta x),(\delta (((x _1) + (x _3)),(\delta ((x _3),x))))) by Th47
.= \delta ((\beta x),(\delta (((x _1) + (x _3)),(x _0)))) by Th48
.= \delta ((\beta x),x) by Th51 ; :: thesis: verum