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 misses X \ Y & X "/\" Y misses Y \ X ) by Th70;
hence X "/\" Y misses X \+\ Y by Th69; :: thesis: verum