Add Subset + change order of variables P and V.

Now, we have (Subset V : set_system U -> set_system U),
(Lift V : set (subset V) -> set_system U), and
(Trace V : set_system U -> set (subset V)).

Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v

@@ -113,14 +113,16 @@ End Base_Def.
 Section Trace_Def.
 
 Context {U : Type}. (* Universe. *)
-Variable P : set_system U.
 Variable V : set U.
+Variable P : set_system U.
 
-(* Definition 226 p. 40 (v3) *)
-Inductive Trace : set (subset V) := Tr : forall B, P B -> Trace (trace V B).
+Inductive Subset : set_system U := Sub : forall A, P A -> incl A V -> Subset A.
 
 Definition Lift : set (subset V) -> set_system U := fun P A => P (trace V A).
 
+(* Definition 226 p. 40 (v3) *)
+Inductive Trace : set (subset V) := Tr : forall A, P A -> Trace (trace V A).
+
 End Trace_Def.