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 Th37
.= \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 Th52 ; :: thesis: verum