:: deftheorem ExMeetDef defines ex1234"/\" LATWAL_2:def 13 :
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 = 3 ) & ( ( x = 1 & y = 3 ) or ( x = 3 & y = 1 ) or x ex1234"/\" y = min (x,y) ) );