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 Th37
.= \delta (((x _4) + (x _0)),(\delta ((x _4),(\delta ((x _3),x))))) by Th50
.= \delta (((x _3) + (x _1)),(\delta ((x _4),(\delta ((x _3),x))))) by Th44
.= \delta (((x _3) + (x _1)),(Expand ((x _3),x))) by Th46
.= \delta (((x _3) + (x _1)),x) by Th37 ;
hence \delta (((x _1) + (x _3)),x) = x _0 ; :: thesis: verum