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 _0)) = x
let x be Element of G; :: thesis: \delta (((x _1) + (x _3)),(x _0)) = x
thus x = Expand (((x _1) + (x _2)),x) by Th36
.= \delta (((x _1) + ((x _2) + x)),(\delta (((x _1) + (x _2)),x))) by LATTICES:def 5
.= \delta (((x _1) + (x _3)),(\delta (((x _1) + (x _2)),x))) by LATTICES:def 5
.= \delta (((x _1) + (x _3)),(x _0)) by Th50 ; :: thesis: verum