theorem :: LATWAL_1:17

for L being WA_Lattice
for x, y, z being Element of L st L is distributive & x [= y & y [= z holds
x [= z