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:17
.= Bottom L by LATTICES:47 ; :: thesis: verum