theorem :: LATTAD_1:66

ex L being non empty LattStr st
( ( for x being Element of L holds
( x = 1 or x = 2 or x = 3 ) ) & ( for x, y being Element of L holds
( ( x "/\" y = 1 implies ( x = 1 & y = 1 ) ) & ( x = 1 & y = 1 implies x "/\" y = 1 ) & ( not x "/\" y = 2 or y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) & ( ( y = 2 or ( y = 1 & ( x = 2 or x = 3 ) ) ) implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of L holds
( ( not x "\/" y = 1 or x = 1 or ( x = 2 & y = 1 ) ) & ( ( x = 1 or ( x = 2 & y = 1 ) ) implies x "\/" y = 1 ) & ( x "\/" y = 2 implies ( x = 2 & ( y = 2 or y = 3 ) ) ) & ( x = 2 & ( y = 2 or y = 3 ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & L is GAD_Lattice )