let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: 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 Th37
.= \delta ((x _1 ) + (x _2 )),(\delta (x _3 ),(x _0 )) by Th45
.= \delta ((x _1 ) + (x _2 )),x by Th47 ; :: thesis: verum