diff --git a/Lebesgue/Subset_R.v b/Lebesgue/Subset_R.v
index 85d5d2b586f7833d23546b73a1f31e8b0d7ebf6f..ead5822e2bc2de42fc4feb5f4ccebbc778e3242c 100644
--- a/Lebesgue/Subset_R.v
+++ b/Lebesgue/Subset_R.v
@@ -17,7 +17,7 @@ COPYING file for more details.
 From Coq Require Import Lia Reals Lra.
 From Coquelicot Require Import Coquelicot.
 
-Require Import R_compl Rbar_compl.
+Require Import R_compl Rbar_compl countable_sets topo_bases_R.
 Require Import Subset Subset_dec Subset_seq.
 Require Import Subset_system_base.
 
@@ -532,9 +532,6 @@ Definition R_subset_open : (R -> Prop) -> Prop :=
 End R_subset_open_Def.
 
 
-Require Import nat_compl countable_sets topo_bases_R.
-
-
 Section R_subset_open_Facts.
 
 (** Correctness results. *)