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 0b3780caf0a0a899cb4d313f4d66a13c2c3e1370..6436346a1b5b188b5f53ebef7fda2faf0c44bcaf 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
@@ -118,13 +118,11 @@ Variable A : set U.
 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 : 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 Lift : subset_system A -> set_system U := liftp_any A.
+Definition Lift_full : subset_system A -> set_system U := fun PA B => PA (trace A B).
 
 (* Definition 226 p. 40 (v3) *)
-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).
+Definition Trace : set_system U -> subset_system A := tracep_any A.
 
 End Trace_Def.