∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}.
⌊n,\fst (a n)⌋ is_decreasing ∧
(\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
intros; apply (segment_preserves_infimum s a x H);
qed.
*)
∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}.
⌊n,\fst (a n)⌋ is_decreasing ∧
(\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
intros; apply (segment_preserves_infimum s a x H);
qed.
*)