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 Th37
.= \delta ((- (x _3 )) + (x _1 )),(- ((\delta (x _3 ),(x _0 )) + x)) by LATTICES:def 5
.= \delta ((- (x _3 )) + (x _1 )),(- (Double x)) by Th47 ;
then A1: - (Double x) = \delta (((- (x _3 )) + (x _1 )) + (- (Double x))),x by Th37;
A2: x = \delta (Double x),(x _0 ) by Th41
.= \delta ((- (((- (x _3 )) + (x _1 )) + (- (Double x)))) + x),(x _0 ) by A1 ;
- (x _3 ) = Expand ((x _1 ) + (- (Double x))),(- (x _3 )) by Th37
.= \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 Th49
.= \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 Th37 ;
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 Th37 ;
:: thesis: verum