let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: thesis: for x being Element of G holds (x _3 ) + x = x _4
let x be Element of G; :: thesis: (x _3 ) + x = x _4
thus (x _3 ) + x = (x _0 ) + (((Double x) + x) + x) by LATTICES:def 5
.= x _4 by LATTICES:def 5 ; :: thesis: verum