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