theorem Th8: :: YELLOW11:8

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