diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
index 6436346a1b5b188b5f53ebef7fda2faf0c44bcaf..45bdfd43e4eca691feeb4dc2647ff24329bc5ec8 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
@@ -115,6 +115,7 @@ Section Trace_Def.
 Context {U : Type}. (* Universe. *)
 Variable A : set U.
 
+(* TODO: find another name! *)
 Inductive Subset : set_system U -> set_system U :=
   | Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.