+
+definition lower_located ≝
+ λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y →
+ (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i).
+
+notation < "s \nbsp 'is_upper_located'" non associative with precedence 50
+ for @{'upper_located $s}.
+notation > "s 'is_upper_located'" non associative with precedence 50
+ for @{'upper_located $s}.
+interpretation "Ordered set upper locatedness" 'upper_located s =
+ (cic:/matita/dama/supremum/upper_located.con _ s).
+
+notation < "s \nbsp 'is_lower_located'" non associative with precedence 50
+ for @{'lower_located $s}.
+notation > "s 'is_lower_located'" non associative with precedence 50
+ for @{'lower_located $s}.
+interpretation "Ordered set lower locatedness" 'lower_located s =
+ (cic:/matita/dama/supremum/lower_located.con _ s).