definition order_continuity ≝
λC:ordered_uniform_space.∀a:sequence C.∀x:C.
(a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).
definition order_continuity ≝
λC:ordered_uniform_space.∀a:sequence C.∀x:C.
(a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).