let L be WA_Lattice; :: thesis: for x, y, z being Element of L st x [= z & y [= z holds
(x "\/" y) "\/" z = x "\/" (y "\/" z)
let x, y, z be Element of L; :: thesis: ( x [= z & y [= z implies (x "\/" y) "\/" z = x "\/" (y "\/" z) )
assume AA: ( x [= z & y [= z ) ; :: thesis: (x "\/" y) "\/" z = x "\/" (y "\/" z)
then A0: ( x "\/" z = z & y "\/" z = z ) by LATTICES:def 3;
( x "/\" z = x & y "/\" z = y ) by LATTICES:4, AA;
hence (x "\/" y) "\/" z = x "\/" (y "\/" z) by A0, DefW33; :: thesis: verum