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