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