theorem FirstOrder.Language.FormulaSet.consistent_chain_upper_bound {L : Language} {n : ℕ} (S : Set (L.FormulaSet n)) (h₁ : ∀ Γ ∈ S, Consistent Γ) (h₂ : IsChain Set.Subset S) (h₃ : S.Nonempty) : ∃ (Γ : L.FormulaSet n), Consistent Γ ∧ ∀ Δ ∈ S, Δ ⊆ Γ

theorem FirstOrder.Language.FormulaSet.lindenbaum {L : Language} {n : ℕ} (Γ : L.FormulaSet n) (h : Consistent Γ) : ∃ (Δ : L.FormulaSet n), Γ ⊆ Δ ∧ Consistent Δ ∧ Complete Δ