let L be WA_Lattice; :: thesis: for x, y, z being Element of L st L is distributive & x [= y & y [= z holds
x [= z
let x, y, z be Element of L; :: thesis: ( L is distributive & x [= y & y [= z implies x [= z )
assume A0: L is distributive ; :: thesis: ( not x [= y or not y [= z or x [= z )
assume A1: ( x [= y & y [= z ) ; :: thesis: x [= z
x "/\" z = x "/\" (y "\/" z) by A1, LATTICES:def 3
.= (x "/\" y) "\/" (x "/\" z) by A0, LATTICES:def 11
.= x "\/" (x "/\" z) by A1, LATTICES:4
.= x by LATTICES:def 8 ;
hence x [= z by LATTICES:4; :: thesis: verum