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