let L be D_Lattice; :: thesis: for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z
let X, Y, Z be Element of L; :: thesis: ( (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z )
assume (X "/\" Y) "\/" (X "/\" Z) = X ; :: thesis: X [= Y "\/" Z
then X "/\" (Y "\/" Z) = X by LATTICES:def 11;
hence X [= Y "\/" Z by LATTICES:4; :: thesis: verum