let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0
let x be Element of G; :: thesis: \delta (((x _1) + (x _3)),x) = x _0
x _0 = Expand ((x _4),(x _0)) by Th36
.= \delta (((x _4) + (x _0)),(\delta ((x _4),(\delta ((x _3),x))))) by Th48
.= \delta (((x _3) + (x _1)),(\delta ((x _4),(\delta ((x _3),x))))) by Th42
.= \delta (((x _3) + (x _1)),(Expand ((x _3),x))) by Th44
.= \delta (((x _3) + (x _1)),x) by Th36 ;
hence \delta (((x _1) + (x _3)),x) = x _0 ; :: thesis: verum