theorem :: LATTAD_1:65

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
( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of L holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & L is GAD_Lattice & L is not AD_Lattice )