let L be Lattice; :: thesis: for X, Y, Z being Element of L st X [= Z holds
X \ Y [= Z
let X, Y, Z 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:9;
Z "/\" (Y `) [= Z by LATTICES:6;
hence X \ Y [= Z by A1, LATTICES:7; :: thesis: verum