Add alternative result.

3a81b48e · François Clément · 268f865e · 3a81b48e
Commit 3a81b48e authored 2 years ago by François Clément
--- a/Lebesgue/Set_theory/Set_system/Topology.v
+++ b/Lebesgue/Set_theory/Set_system/Topology.v
@@ -55,6 +55,11 @@ intros B HB; induction HB; apply Open_Gen; easy.
 intros B HB; apply Open_Gen; auto.
 Qed.

+Lemma Basis_is_gen_alt : T = Uac_Ifc_wF PB.
+Proof.
+rewrite <- Open_equiv; apply Basisp_is_gen.
+Qed.
+
 End Basis_Facts1.