let L be WA_Lattice; :: thesis: for x, y being Element of L holds x "/\" y [= x
let x, y be Element of L; :: thesis: x "/\" y [= x
(x "/\" y) "\/" x = x by LATTICES:def 8;
hence x "/\" y [= x by LATTICES:def 3; :: thesis: verum