X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Frelations.ma;h=5e2274047031ecc5cc02f2fc12c07f4b0d7d47de;hb=121d6d7cd72ae57a4ed838ef02ae98f3bafb6e9d;hp=1ab9ec3f15f9e810afc1c7c2093a625beaf05a48;hpb=1110bdf814f976ef0a36a024d2cba847ce06347e;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 1ab9ec3f1..5e2274047 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -108,12 +108,12 @@ qed.
 interpretation "subset comprehension" 'comprehension s p =
  (comprehension s (mk_unary_morphism __ p _)).
 
-definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
   [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros;
-     [ apply (. #‡(#‡H)); assumption
-     | apply (. #‡(#‡H\sup -1)); assumption]]
+  | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
+     [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
+     | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
 qed.
 
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.