let L be B_Lattice; :: thesis: for X being Element of L holds X \+\ X = Bottom L
let X be Element of L; :: thesis: X \+\ X = Bottom L
thus X \+\ X = X \ X by LATTICES:1
.= Bottom L by LATTICES:20 ; :: thesis: verum