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