∀C:ordered_uniform_space.property_sigma C →
∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
match i with