let L be Lattice; :: thesis: for p, r, q being Element of L st p [= r holds
p "/\" q [= r
let p, r, q be Element of L; :: thesis: ( p [= r implies p "/\" q [= r )
assume p [= r ; :: thesis: p "/\" q [= r
then ( p "/\" q [= r "/\" q & q "/\" p [= q "/\" r & r "/\" q [= r & q "/\" r = r "/\" q ) by LATTICES:23, LATTICES:27;
hence p "/\" q [= r by LATTICES:25; :: thesis: verum