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

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