let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: for x being Element of G holds \delta ((Double x),(x _0)) = x
let x be Element of G; :: thesis: \delta ((Double x),(x _0)) = x
thus \delta ((Double x),(x _0)) = Expand (x,x)
.= x by Th36 ; :: thesis: verum