theorem Th17: :: YELLOW_5:17

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