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