∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  K.Nonempty →
    (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
      (Quotient.mk' '' K).Countable →
        FirstOrder.Language.Hereditary K →
          FirstOrder.Language.JointEmbedding K → FirstOrder.Language.Amalgamation K → FirstOrder.Language.IsFraisse K