:: deftheorem UPDef defines ex123"\/" LATWAL_1:def 7 :
for x, y being Element of {0,1,2} holds
( ( ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) ) implies x ex123"\/" y = 0 ) & ( ( x = 0 & y = 2 ) or ( x = 2 & y = 0 ) or x ex123"\/" y = max (x,y) ) );