From 3a81b48e3d372d788153e24bc284c7f9fe8543ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 1 Jul 2022 18:52:14 +0200
Subject: [PATCH] Add alternative result.

---
 Lebesgue/Set_theory/Set_system/Topology.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Lebesgue/Set_theory/Set_system/Topology.v b/Lebesgue/Set_theory/Set_system/Topology.v
index d1ae692f..e7362228 100644
--- 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.
 
 
-- 
GitLab