theorem Th9: :: LATTICES:11

for L being D_Lattice
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)