X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs_to_o-basic_pairs.ma;h=3e2fe8f354ee116ad0e851d568893eaa14182b2a;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=9e85452d585eebbb7b558a0d0a521f000689364f;hpb=23043db144b24b8cd2072800b61137bb396f891e;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
index 9e85452d5..3e2fe8f35 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
@@ -126,7 +126,8 @@ theorem BP_to_OBP_faithful:
  apply e;
 qed.
 
-theorem BP_to_OBP_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
+theorem BP_to_OBP_full: 
+   ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
  intros; 
  cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
  cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);