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