let L be Lattice; :: thesis: for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z
let X, Z, Y be Element of L; :: thesis: ( X [= Z implies X \ Y [= Z )
assume X [= Z ; :: thesis: X \ Y [= Z
then A1: X "/\" (Y ` ) [= Z "/\" (Y ` ) by LATTICES:27;
Z "/\" (Y ` ) [= Z by LATTICES:23;
hence X \ Y [= Z by A1, LATTICES:25; :: thesis: verum