Add results about Trace and "any" set systems.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -360,6 +360,33 @@ Qed.
 End Set_system_Facts5.
 
 
+Section Trace_Facts.
+
+Context {U : Type}.
+Variable P : set_system U.
+Variable V : set U.
+
+Lemma Trace_Open : is_Open P -> is_Open (Trace P V).
+Proof.
+rewrite 2!is_Open_equiv; intros [HP1 [HP2 [HP3 HP4]]]; repeat split.
+apply Trace_wEmpty; easy.
+apply Trace_wFull; easy.
+apply Trace_Inter; easy.
+apply Trace_Unionf_any; easy.
+Qed.
+
+Lemma Trace_Closed : is_Closed P -> is_Closed (Trace P V).
+Proof.
+rewrite 2!is_Closed_equiv; intros [HP1 [HP2 [HP3 HP4]]]; repeat split.
+apply Trace_wEmpty; easy.
+apply Trace_wFull; easy.
+apply Trace_Union; easy.
+apply Trace_Interf_any; easy.
+Qed.
+
+End Trace_Facts.
+
+
 Section Basis_Facts1.
 
 Context {U Idx : Type}.