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 Th37
.= \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 Th49
.= \delta ((\beta x),(\delta (((x _1) + (x _3)),(x _0)))) by Th50
.= \delta ((\beta x),x) by Th53 ; :: thesis: verum