∀ {X : AlgebraicGeometry.Scheme},
  X.IsSeparated ↔
    AlgebraicGeometry.IsClosedImmersion
      (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))