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:5, LATTICES:6;
hence X "/\" Y [= X "\/" Z by LATTICES:7; :: thesis: verum