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