∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.LocalizationAwayPreserves P →
    RingHom.OfLocalizationSpanTarget P →
      RingHom.OfLocalizationSpan P →
        RingHom.StableUnderCompositionWithLocalizationAwayTarget P → RingHom.PropertyIsLocal P