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 ( ( x = 0 & y = 0 ) or ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or ( not ( x = 0 & y = 2 ) & not ( x = 2 & y = 0 ) ) ) ;

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

hence ex123/\ . (x,y) = ex123/\ . (y,x) ; :: thesis: verum

end;

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

ex123/\ . (x,y) = xx ex123"/\" yy by EXNDef
.= 2 by ExMeetDef, X1
.= yy ex123"/\" xx by ExMeetDef, X1
.= ex123/\ . (y,x) by EXNDef ;
hence ex123/\ . (x,y) = ex123/\ . (y,x) ; :: thesis: verum

end;

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

ex123/\ . (x,y) = xx ex123"/\" yy by EXNDef
.= 2 by ExMeetDef, X1
.= yy ex123"/\" xx by ExMeetDef, X1
.= ex123/\ . (y,x) by EXNDef ;
hence ex123/\ . (x,y) = ex123/\ . (y,x) ; :: thesis: verum

end;

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

ex123/\ . (x,y) = xx ex123"/\" yy by EXNDef
.= min (xx,yy) by ExMeetDef, X1
.= yy ex123"/\" xx by ExMeetDef, X1
.= ex123/\ . (y,x) by EXNDef ;
hence ex123/\ . (x,y) = ex123/\ . (y,x) ; :: thesis: verum

end;

end;