diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f938fac2e..b81edda14 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -16,6 +16,9 @@
 - in `realfun.v`:
   + lemmas `cvg_pinftyP`, `cvg_ninftyP`
 
+- in `topology.v`:
+  + lemma `in_nearW`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/topology.v b/theories/topology.v
index 123ab26ce..4eff4ff4f 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -7176,3 +7176,13 @@ Qed.
 Local Close Scope relation_scope.
 
 #[global] Hint Resolve uniform_regular : core.
+
+Lemma in_nearW (R : topologicalType) (P : R -> Prop) (S : set R) :
+  @open R^o S ->
+ {in S, forall x, P x} ->
+ {in S, forall x, \near x, P x}.
+Proof.
+move=> oS HP z /set_mem Sz.
+rewrite -nbhs_nearE nbhsE/=.
+by exists S; last move=> x /mem_set/HP.
+Qed.