Use new generic results from Set_system_any.v.

Lebesgue/Set_theory/Set_system/Topology.v

@@ -46,18 +46,16 @@ unfold PB_A; intros B HB; apply Open_Gen; easy.
 intros B HB; apply Open_Gen; auto.
 Qed.
 
-Lemma Basisp_covers_all : unionp_any PB = fullset.
+Lemma Basisp_fullset : unionp_any PB = fullset.
 Proof.
-rewrite (proj2 HPB fullset).
-apply set_ext_equiv; split; intros x [B HB]; exists B; easy.
-rewrite <- HT; apply Open_wFull.
+rewrite <- full_equiv; apply is_Basisp_full with T; try easy.
+apply is_Open_equiv; easy.
 Qed.
 
 Lemma Basisp_Union_any_inter : Union_any_inter PB.
 Proof.
-destruct HPB as [HPB1 HPB2]; intros B1 B2 HB1 HB2.
-exists (fun B => PB B /\ incl B (inter B1 B2)); split; try easy.
-apply HPB2; rewrite <- HT; apply Open_Inter; apply Open_Gen; auto.
+apply is_Basisp_inter with T; try easy.
+apply is_Open_equiv; easy.
 Qed.
 
 End Basis_Facts3.