:: deftheorem UPDef defines ex1234"\/" LATWAL_2:def 12 :
for x, y being Element of {0,1,2,3,4} holds
( ( ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) ) implies x ex1234"\/" y = 1 ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or x ex1234"\/" y = max (x,y) ) );