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 that
A1: X [= Y and
A2: Z [= V ; :: thesis: X \ V [= Y \ Z
A3: X \ V [= Y \ V by A1, LATTICES:27;
Y \ V [= Y \ Z by A2, Th39;
hence X \ V [= Y \ Z by A3, LATTICES:25; :: thesis: verum