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