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