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