let L be Lattice; :: thesis: for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z
let X, Y, Z be Element of L; :: thesis: X "/\" Y [= X "\/" Z
( X "/\" Y [= X & X [= X "\/" Z ) by LATTICES:22, LATTICES:23;
hence X "/\" Y [= X "\/" Z by LATTICES:25; :: thesis: verum