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
X \ (Bottom L) = X "/\" (Top L) by LATTICE4:30
.= X ;
hence X \ (Bottom L) = X ; :: thesis: verum