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