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 = max (yy,zz) by UPDef
.= 2 by XXREAL_0:def 10 ;
then t1: x "\/" (y "\/" z) = x "\/" z by EXUDef
.= xx ex123"\/" zz by EXUDef
.= 0 by UPDef ;
xx ex123"\/" yy = max (xx,yy) by UPDef
.= 1 by XXREAL_0:def 10 ;
then (x "\/" y) "\/" z = y "\/" z by EXUDef
.= yy ex123"\/" zz by EXUDef
.= max (yy,zz) by UPDef
.= 2 by XXREAL_0:def 10 ;
hence not ExNearLattice is join-associative by LATTICES:def 5, t1; :: thesis: verum