diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v b/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
index db6c545b53347bbca2adcee632ab431342ebc62d..c9e466b41e1389a5b0020a429040c5e77c1ca9de 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
@@ -377,48 +377,13 @@ rewrite <- trace_union_seq; apply Im, HP, HB.
 apply union_seq_ext; intros n; symmetry; apply HB.
 Qed.
 
-(* Is that true? *)
-Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace V P).
-Proof.
-intros HP A HA1 HA2.
-assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
-  intros n; induction (HA2 n) as [B HB]; exists B; easy.
-destruct (choice _ HA3) as [B HB1].
-assert (HB2 : decr_seq B).
-  intros n. admit.
-replace (inter_seq A) with (inter_seq (tracem_seq V B)).
-rewrite <- trace_inter_seq; apply Im, HP; try apply HB1; easy.
-apply inter_seq_ext; intros n; symmetry; apply HB1.
-Admitted.
+(* These results are wrong!
 
-(* Is that true? *)
+Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace V P).
 Lemma Trace_Union_monot_seq : Union_monot_seq P -> Union_monot_seq (Trace V P).
-Proof.
-intros HP A HA1 HA2.
-assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
-  intros n; induction (HA2 n) as [B HB]; exists B; easy.
-destruct (choice _ HA3) as [B HB1].
-assert (HB2 : incr_seq B).
-  intros n. admit.
-replace (union_seq A) with (union_seq (tracem_seq V B)).
-rewrite <- trace_union_seq; apply Im, HP; try apply HB1; easy.
-apply union_seq_ext; intros n; symmetry; apply HB1.
-Admitted.
-
-(* Is that true? *)
 Lemma Trace_Union_disj_seq : Union_disj_seq P -> Union_disj_seq (Trace V P).
-Proof.
-intros HP A HA1 HA2.
-assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
-  intros n; induction (HA2 n) as [B HB]; exists B; easy.
-destruct (choice _ HA3) as [B HB1].
-assert (HB2 : disj_seq B).
-  intros n1 n2 Hn.
 
- admit.
-replace (union_seq A) with (union_seq (tracem_seq V B)).
-rewrite <- trace_union_seq; apply Im, HP; try apply HB1; easy.
-apply union_seq_ext; intros n; symmetry; apply HB1.
-Admitted.
+Indeed, monotonic or disjoint traces do not imply that the initial sequence is.
+Thus, we cannot use the hypothesis... *)
 
 End Seq_Facts3.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_seq.v b/Lebesgue/Set_theory/Set_system/Set_system_seq.v
index 6b7cb6e8dd0177f03c836b37bc3a17db36bddf99..191d45300df6d462ecaa02fb52afd3a6a9240abe 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_seq.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_seq.v
@@ -1167,20 +1167,9 @@ Context {U : Type}.
 Variable P : set_system U.
 Variable V : set U.
 
+(* These results are wrong since unitary results are!
 Lemma Trace_Monotone_class : is_Monotone_class P -> is_Monotone_class (Trace V P).
-Proof.
-rewrite 2!Monotone_class_equiv; intros [HP1 HP2]; split; try easy.
-apply Trace_Inter_monot_seq; easy.
-apply Trace_Union_monot_seq; easy.
-Qed.
-
-Lemma Trace_Lsyst : is_Lsyst P -> is_Lsyst (Trace V P).
-Proof.
-rewrite 2!Lsyst_equiv; intros [HP1 [HP2 HP3]]; repeat split.
-apply Trace_wFull; easy.
-apply Trace_Compl; easy.
-apply Trace_Union_disj_seq; easy.
-Qed.
+Lemma Trace_Lsyst : is_Lsyst P -> is_Lsyst (Trace V P). *)
 
 Lemma Trace_Sigma_ring : is_Sigma_ring P -> is_Sigma_ring (Trace V P).
 Proof.