Simplify some proofs.

Some renaming.
Proof of is_Basisp_Union_any_closure completed.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -180,13 +180,10 @@ Qed.
 
 Lemma Open_Union_any : Union_any (Open genU).
 Proof.
-intros PA [A0 HA0] HPA.
-rewrite unionp_any_unionf_any_eq; apply Open_Unionf_any.
-apply inhabits; exists A0; easy.
-intros [A HA]; auto.
+apply Unionf_any_Union_any_equiv, Open_Unionf_any.
 Qed.
 
-Lemma Union_any_inter_is_Open :
+Lemma Union_any_closure_is_Open :
   forall (P : set_system U),
     unionp_any P = fullset -> Union_any_inter P ->
     is_Open (Union_any_closure P).
@@ -261,13 +258,10 @@ Qed.
 
 Lemma Closed_Inter_any : Inter_any (Closed genU).
 Proof.
-intros PA [A0 HA0] HPA.
-rewrite interp_any_interf_any_eq; apply Closed_Interf_any.
-apply inhabits; exists A0; easy.
-intros [A HA]; auto.
+apply Interf_any_Inter_any_equiv, Closed_Interf_any.
 Qed.
 
-Lemma Inter_any_union_is_Closed :
+Lemma Inter_any_closure_is_Closed :
   forall (P : set_system U),
     interp_any P = emptyset -> Inter_any_union P ->
     is_Closed (Inter_any_closure P).
@@ -349,7 +343,7 @@ apply Closed_complp_any_is_complp_any_Open.
 apply complp_any_Open_is_Closed_complp_any.
 Qed.
 
-Lemma is_Open_is_Closed_complp_any :
+Lemma is_Open_is_Closed_complp_any_equiv :
   forall (P : set_system U), is_Open P <-> is_Closed (complp_any P).
 Proof.
 intros; rewrite is_Open_equiv, is_Closed_equiv.
@@ -357,10 +351,10 @@ rewrite <- wFull_wEmpty_complp_any, <- wEmpty_wFull_complp_any,
     <- Inter_Union_complp_any, <- Unionf_any_Interf_any_complp_any; easy.
 Qed.
 
-Lemma is_Closed_is_Open_complp_any :
+Lemma is_Closed_is_Open_complp_any_equiv :
   forall (P : set_system U), is_Closed P <-> is_Open (complp_any P).
 Proof.
-intros; rewrite is_Open_is_Closed_complp_any, complp_any_invol; easy.
+intros; rewrite is_Open_is_Closed_complp_any_equiv, complp_any_invol; easy.
 Qed.
 
 End Set_system_Facts5.
@@ -408,22 +402,18 @@ Qed.
 
 Variable P : set_system U.
 
-Hypothesis HP1 : unionp_any P = fullset.
-Hypothesis HP2 : Union_any_inter P.
-
-Lemma is_Basisp_alt : is_Basisp (Union_any_closure P) P.
+Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure P) P.
 Proof.
 split.
 apply Union_any_closure_Gen.
 intros A HA; induction HA as [Q HQ].
-apply set_ext_equiv; split; intros x [B [HB1 HB2]].
+apply set_ext_equiv; split; intros x [B [HB Hx]].
 (* *)
-exists B; repeat split; try easy; auto.
+exists B; repeat split; auto.
 intros y Hy; exists B; easy.
 (* *)
-destruct HB1 as [HB0 HB1]; exists B; split; auto.
-
-Admitted.
+destruct HB as [HB1 HB2]; auto.
+Qed.
 
 End Basis_Facts1.