diff --git a/Lebesgue/Set_theory/Set_system/Set_system_any.v b/Lebesgue/Set_theory/Set_system/Set_system_any.v
index 7852a9a4ebf45d1324eb650293a0b427d5bbed71..2684a132dc0539d7e7837900a434ce495d80003a 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_any.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_any.v
@@ -503,17 +503,6 @@ apply Union_any_closure_Gen.
 apply Union_any_closure_monot, incl_add_r.
 Qed.
 
-(*
-Lemma Uac_Ifc_wFull :
-  wFull genU -> Uac_Ifc_wF = Union_any_closure (Inter_finite_closure genU).
-Proof.
-intros H; unfold Uac_Ifc_wF; f_equal; apply Ext_equiv; split; intros A HA.
-destruct HA as [HA | HA]; try easy;
-    rewrite HA; apply Inter_finite_closure_Gen; easy.
-apply incl_add_r; easy.
-Qed.
-*)
-
 Lemma Uac_Ifc_wF_is_Open : is_Open Uac_Ifc_wF.
 Proof.
 apply Union_any_closure_is_Open.
@@ -547,105 +536,26 @@ Qed.
 
 Lemma Open_equiv : Open genU = Uac_Ifc_wF.
 Proof.
-apply Ext_equiv; split; intros A HA.
-(* *)
-induction HA as [A HA | | | A N HA1 HA2 | Idx fA HIdx HfA1 HfA2].
-apply Uac_Ifc_wF_Gen; easy.
-rewrite <- unionp_any_nullary; apply Uac; easy.
-apply Union_any_closure_Gen; right; easy.
-(* . *)
-destruct (choice (fun (i : {n | n < S N}) QB =>
-    Incl QB (Inter_finite_closure_wF genU) /\
-    A (proj1_sig i) = unionp_any QB)) as [QB HQB].
-  intros [n Hn]; simpl; induction (HA2 n Hn) as [QB HQB].
-  exists QB; repeat split; easy.
-assert (HA3 : inter_finite A N = unionp_any (interf_any QB)).
-  admit.
-rewrite HA3; apply Uac.
-intros C HC.
-
-
-Search incl interf_any.
-
-
-admit.
-
-
-(* . *)
-
-admit.
-
-(* *)
-induction HA as [Q HQ1].
-destruct (empty_dec Q) as [HQ2 | HQ2].
-rewrite empty_equiv in HQ2; rewrite HQ2, unionp_any_nullary; apply Open_wEmpty.
+rewrite <- Uac_Ifc_wF_is_Open; apply Open_ext.
+apply Incl_trans with Uac_Ifc_wF; [apply Uac_Ifc_wF_Gen | apply Open_Gen].
+intros A HA; induction HA as [Q HQ].
+destruct (empty_dec Q) as [HQ' | HQ'].
+rewrite empty_equiv in HQ'; rewrite HQ', unionp_any_nullary; apply Open_wEmpty.
 apply Open_Union_any; try easy.
-apply Incl_trans with (Inter_finite_closure genU); try easy.
-intros A HA.
-
-
-
-; induction HA; apply Open_Inter_finite.
-intros; apply Open_Gen; auto.
-Admitted.
+apply Incl_trans with (Inter_finite_closure_wF genU); try easy.
+intros A [HA | HA].
+induction HA as [B N HB]; apply Open_Inter_finite; intros; apply Open_Gen; auto.
+rewrite HA; apply Open_wFull.
+Qed.
 
 Lemma Inter_finite_closure_is_Basisp :
-  wFull genU -> is_Basisp (Open genU) (Inter_finite_closure genU).
+  is_Basisp (Open genU) (Inter_finite_closure_wF genU).
 Proof.
 intros.
 rewrite Open_equiv; try easy.
 apply is_Basisp_Union_any_closure.
 Qed.
 
-(*
-intros H; split.
-intros A [B N HB]; apply Open_Inter_finite; intros; apply Open_Gen; auto.
-intros A HA; apply set_ext_equiv; split.
-(* *)
-induction HA as [A HA | | | A N HA1 HA2 | Idx fA HIdx HfA1 HfA2]; try easy.
-(* . *)
-intros x Hx; exists A; repeat split; try easy.
-apply Inter_finite_closure_Gen; easy.
-(* . *)
-intros x _; exists fullset; repeat split; try easy.
-rewrite <- (inter_finite_cst fullset 0); easy.
-(* . *)
-intros x Hx.
-destruct (choice (fun (i : {n | n < S N}) B =>
-    Inter_finite_closure genU B /\ incl B (A (proj1_sig i)))) as [C HC].
-  intros [n Hn]; destruct (HA2 n Hn x (Hx n Hn)) as [B HB].
-  exists B; repeat split; easy.
-exists (interf_any C); rewrite interf_any_inter_finite_eq; repeat split.
-(* .. *)
-intros n Hn; destruct (Compare_dec.lt_dec n (S N)); try easy.
-rewrite (proof_irrelevance _ _ Hn).
-destruct (HC (exist _ n Hn)) as [H1 _].
-induction H1.
-
-admit.
-
-(* .. *)
-intros y Hy n Hn; specialize (Hy n Hn); simpl in Hy.
-destruct (Compare_dec.lt_dec n (S N)); try easy.
-rewrite (proof_irrelevance _ _ Hn) in Hy.
-destruct (HC (exist _ n Hn)) as [_ H2]; auto.
-(* .. *)
-intros n Hn; specialize (Hx n Hn).
-destruct (Compare_dec.lt_dec n (S N)); try easy.
-rewrite (proof_irrelevance _ _ Hn).
-specialize (HC (exist _ n Hn)).
-
-admit.
-
-(* . *)
-intros x [i Hx]; destruct (HfA2 i x Hx) as [B [[HB1 HB2] HB3]].
-exists B; repeat split; try easy.
-intros y Hy; exists i; auto.
-(* *)
-intros x [B [[HB1 HB2] HB3]]; auto.
-Admitted.
-*)
-
 End Basis_Facts3.