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

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

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

end;

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

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

end;

end;