Add alternatives.

Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v

@@ -114,15 +114,17 @@ Section Trace_Def.
 
 Context {U : Type}. (* Universe. *)
 Variable A : set U.
-Variable P : set_system U.
-Variable PA : subset_system A.
 
-Inductive Subset : set_system U := Sub : forall B, P B -> incl B A -> Subset B.
+Inductive Subset : set_system U -> set_system U :=
+  | Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.
 
-Definition Lift : set_system U := fun B => PA (trace A B).
+Definition Lift : subset_system A -> set_system U := image (lift A).
+Definition Lift' : subset_system A -> set_system U := fun PA B => PA (trace A B).
 
 (* Definition 226 p. 40 (v3) *)
-Inductive Trace : subset_system A := Tr : forall B, P B -> Trace (trace A B).
+Definition Trace : set_system U -> subset_system A := image (trace A).
+Inductive Trace' : set_system U -> subset_system A :=
+  | Tr : forall (P : set_system U) B, P B -> Trace' P (trace A B).
 
 End Trace_Def.