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