let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: thesis: for x being Element of G holds \delta ((x _1 ) + (x _3 )),x = x _0
let x be Element of G; :: thesis: \delta ((x _1 ) + (x _3 )),x = x _0
x _0 = Expand (x _4 ),(x _0 ) by Th37
.= \delta ((x _4 ) + (x _0 )),(\delta (x _4 ),(\delta (x _3 ),x)) by Th50
.= \delta ((x _3 ) + (x _1 )),(\delta (x _4 ),(\delta (x _3 ),x)) by Th44
.= \delta ((x _3 ) + (x _1 )),(Expand (x _3 ),x) by Th46
.= \delta ((x _3 ) + (x _1 )),x by Th37 ;
hence \delta ((x _1 ) + (x _3 )),x = x _0 ; :: thesis: verum