let L be B_Lattice; :: thesis: for X, Y being Element of L holds X \ Y misses Y
let X, Y be Element of L; :: thesis: X \ Y misses Y
(X \ Y) "/\" Y = X "/\" ((Y ` ) "/\" Y) by LATTICES:def 7
.= X "/\" (Bottom L) by LATTICES:47
.= Bottom L by LATTICES:40 ;
hence X \ Y misses Y by Def4; :: thesis: verum