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 d7b19fead092f0fad635768f151d98f1f75c5a28..40586037f1c26c81408d326cd077c49c4ca4f0d3 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
@@ -108,8 +108,8 @@ 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.
+Inductive Subset (P : set_system U) : set_system U :=
+  | Sub : forall B, P B -> incl B A -> Subset P B.
 
 Definition Lift : subset_system A -> set_system U := liftp_any A.
 Definition Lift_full : subset_system A -> set_system U :=