...

[helm.git] / helm / software / matita / library / formal_topology / basic_pairs.ma

diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 475445720202266f7b9503b696d2e66c21fb2ab9..0d51724de7114ad3eb7c2d3936856a13933ed313 100644 (file)
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -133,7 +133,13 @@ definition BP: category1.
     apply ((id_neutral_left1 ????)‡#);]
 qed.
 
-definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+  [ apply (ext ? ? (rel o));
+  | intros;
+    apply (.= #‡H);
+    apply refl1]
+qed.
 
 definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
  λo.extS ?? (rel o).