let x, y be Element of ExNearLattice; :: thesis: ex123\/ . (x,y) = ex123\/ . (y,x)
reconsider xx = x, yy = y as Element of {0,1,2} ;

per cases ( ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) ;

suppose V1: ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) ; :: thesis: ex123\/ . (x,y) = ex123\/ . (y,x)

then xx ex123"\/" yy = max (xx,yy) by UPDef;
then V3: ex123\/ . (x,y) = max (xx,yy) by EXUDef;
yy ex123"\/" xx = max (yy,xx) by V1, UPDef;
hence ex123\/ . (x,y) = ex123\/ . (y,x) by V3, EXUDef; :: thesis: verum

end;

suppose V1: ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) ; :: thesis: ex123\/ . (x,y) = ex123\/ . (y,x)

then xx ex123"\/" yy = 0 by UPDef;
then V3: ex123\/ . (x,y) = 0 by EXUDef;
yy ex123"\/" xx = 0 by V1, UPDef;
hence ex123\/ . (x,y) = ex123\/ . (y,x) by V3, EXUDef; :: thesis: verum

end;

end;