let L be B_Lattice; :: thesis: for X being Element of L holds X \+\ (Bottom L) = X
let X be Element of L; :: thesis: X \+\ (Bottom L) = X
thus X \+\ (Bottom L) = X "\/" ((Bottom L) \ X) by Th67
.= X "\/" (Bottom L) by LATTICES:40
.= X by LATTICES:39 ; :: thesis: verum