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) by Th47
.= X ; :: thesis: verum