let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x being Element of G holds \delta ((x _3),x) = x _0
let x be Element of G; :: thesis: \delta ((x _3),x) = x _0
set alpha = ((- (x _3)) + (x _1)) + (- (Double x));
x = Expand (((- (x _3)) + (x _0)),x) by Th36
.= \delta (((- (x _3)) + (x _1)),(- ((\delta ((x _3),(x _0))) + x))) by LATTICES:def 5
.= \delta (((- (x _3)) + (x _1)),(- (Double x))) by Th45 ;
then A1: - (Double x) = \delta ((((- (x _3)) + (x _1)) + (- (Double x))),x) by Th36;
A2: x = \delta ((Double x),(x _0)) by Th40
.= \delta (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + x),(x _0)) by A1 ;
- (x _3) = Expand (((x _1) + (- (Double x))),(- (x _3))) by Th36
.= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((x _1) + (- (Double x))),(- (x _3))))) by LATTICES:def 5
.= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((x _0) + (x + (Double x))),(\delta ((Double x),(x _1)))))) by Th47
.= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((Double x) + (x _1)),(\delta ((Double x),(x _1)))))) by LATTICES:def 5
.= - ((- (((- (x _3)) + (x _1)) + (- (Double x)))) + (x _1)) by Th36 ;
hence \delta ((x _3),x) = \delta (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + ((x _0) + x)),x)
.= Expand (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + x),(x _0)) by A2, LATTICES:def 5
.= x _0 by Th36 ;
:: thesis: verum