theorem Th7: :: YELLOW11:7

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