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:15
.= X by LATTICES:14 ; :: thesis: verum