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