let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: thesis: for x being Element of G holds \delta (x _3 ),(x _0 ) = x
let x be Element of G; :: thesis: \delta (x _3 ),(x _0 ) = x
thus x = Expand (x _2 ),x by Th37
.= \delta (x + (x _2 )),(x _0 ) by Th42
.= \delta (x _3 ),(x _0 ) by LATTICES:def 5 ; :: thesis: verum