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