theorem lemma18_proj_isSeparated {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Proj.toSpecZero 𝒜)

Lemma 18: the structure morphism Proj 𝒜 → Spec (𝒜_0) is separated.