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