∀ (L : FirstOrder.Language) (M : Type u_1) [inst : L.Structure M] (x : Set M),
  ↑((FirstOrder.Language.Substructure.closure L).toFun x) ≤ x →
    (FirstOrder.Language.Substructure.closure L).toFun x = (FirstOrder.Language.Substructure.closure L).toFun x