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 Th41
.= x _0 by Th37 ; :: thesis: verum