∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {R : Type u}
  [inst : CommRing R] {f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)} [P.IsClosedUnderIsomorphisms],
  AlgebraicGeometry.geometrically P f ↔
    ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K],
      P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))))