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