X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsupremum.ma;h=7bb684fd897ea243cded37e668e7ba9cfa026cc7;hb=858e703335b47065529d481891863d380a2156d7;hp=54e9d98f0c30a07472c19bca4fba55e44e99d535;hpb=bde2f037924b8854d5ed4e6b133c306156a1fcf5;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 54e9d98f0..7bb684fd8 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -363,13 +363,18 @@ qed.
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
 definition square_segment ≝ 
-  λO:ordered_set.λa,b:O.λx: O squareO.
-    And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
+  λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
+    in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
  
 definition convex ≝
-  λO:ordered_set.λU:O squareO → Prop.
-    ∀p.U p → \fst p ≤ \snd p → ∀y. 
-      square_segment O (\fst p) (\snd p) y → U y.
+  λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
+    ∀s.U s → le O (\fst s) (\snd s) → 
+     ∀y. 
+       le O (\fst y) (\snd s) → 
+       le O (\fst s) (\fst y) →
+       le O (\snd y) (\snd s) →
+       le O (\fst y) (\snd y) →
+       U y.
   
 (* Definition 2.11 *)  
 definition upper_located ≝