let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x being Element of G holds \delta ((x _3),(x _0)) = x
let x be Element of G; :: thesis: \delta ((x _3),(x _0)) = x
thus x = Expand ((x _2),x) by Th37
.= \delta ((x + (x _2)),(x _0)) by Th42
.= \delta ((x _3),(x _0)) by LATTICES:def 5 ; :: thesis: verum