Definability in substructure orderings, IV: Finite lattices

Let ${\mathcal{L}}$ be the ordered set of isomorphism types of finite lattices, where the ordering is by embeddability. We study first-order definability in this ordered set. Our main result is that for every finite lattice L, the set {?, ? ^opp} is definable, where ? and ? ^opp are the isomorphism types of L and its opposite (L turned upside down). We shall show that the only non-identity automorphism of ${\mathcal{L}}$ is the map ${\ell \mapsto \ell^{\rm opp}}$ .