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

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