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