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