∀
  (x :
    ↑{ carrier := { carrier := PEmpty.{u_1 + 1}, str := instTopologicalSpacePEmpty },
          presheaf :=
            (CategoryTheory.Functor.const
                  (TopologicalSpace.Opens ↑{ carrier := PEmpty.{u_1 + 1}, str := instTopologicalSpacePEmpty })ᵒᵖ).obj
              { carrier := PUnit.{u_1 + 1}, commRing := PUnit.commRing },
          IsSheaf := AlgebraicGeometry.Scheme.empty._proof_1,
          isLocalRing := AlgebraicGeometry.Scheme.empty._proof_2 }.toTopCat)
  (U : TopologicalSpace.OpenNhds x), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (↑U).inclusion')