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