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

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

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

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

end;

suppose X1: ( x = 1 & y = 3 ) ; :: thesis: ex1234/\ . (x,y) = ex1234/\ . (y,x)

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

end;

suppose X1: ( x = 3 & y = 1 ) ; :: thesis: ex1234/\ . (x,y) = ex1234/\ . (y,x)

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

end;

suppose X1: ( not ( x = 1 & y = 3 ) & not ( x = 3 & y = 1 ) ) ; :: thesis: ex1234/\ . (x,y) = ex1234/\ . (y,x)

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

end;

end;