let L be Lattice; :: thesis: for p, q, r being Element of L st p [= r holds
p "/\" q [= r
let p, q, r be Element of L; :: thesis: ( p [= r implies p "/\" q [= r )
assume p [= r ; :: thesis: p "/\" q [= r
then A1: p "/\" q [= r "/\" q by LATTICES:9;
r "/\" q [= r by LATTICES:6;
hence p "/\" q [= r by A1, LATTICES:7; :: thesis: verum