:: deftheorem Defx5 defines example33"/\" LATTAD_1:def 19 :
for x, y being Element of {1,2,3} holds
( ( x = 1 & y = 1 implies x example33"/\" y = 1 ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies x example33"/\" y = 2 ) & ( y = 3 implies x example33"/\" y = 3 ) );