let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: 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 Th37 ; :: thesis: verum