set L = ExWALattice ;
reconsider x = 1, y = 2, z = 3 as Element of ExWALattice by ENUMSET1:def 3;
reconsider xx = x, yy = y, zz = z as Element of {0,1,2,3,4} ;
yy ex1234"/\" zz = min (yy,zz) by ExMeetDef
.= 2 by XXREAL_0:def 9 ;
then t1: x "/\" (y "/\" z) = x "/\" y by EXNDef
.= xx ex1234"/\" yy by EXNDef
.= min (xx,yy) by ExMeetDef
.= 1 by XXREAL_0:def 9 ;
xx ex1234"/\" yy = min (xx,yy) by ExMeetDef
.= 1 by XXREAL_0:def 9 ;
then (x "/\" y) "/\" z = x "/\" z by EXNDef
.= xx ex1234"/\" zz by EXNDef
.= 3 by ExMeetDef ;
hence not ExWALattice is meet-associative by LATTICES:def 7, t1; :: thesis: verum