let L be B_Lattice; :: thesis: for X, Y, Z, V being Element of L st X [= Y & Z [= V holds
X \ V [= Y \ Z
let X, Y, Z, V be Element of L; :: thesis: ( X [= Y & Z [= V implies X \ V [= Y \ Z )
assume ( X [= Y & Z [= V ) ; :: thesis: X \ V [= Y \ Z
then ( X \ V [= Y \ V & Y \ V [= Y \ Z ) by Th22, LATTICES:9;
hence X \ V [= Y \ Z by LATTICES:7; :: thesis: verum