Kit for def:cauchy-sequence-nbg

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i<n$. A condition on $x_{0},\dots,x_{n-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}$, $\mathbb{R}$, the order $\le$, the strict order $<$ and the element $0$ of $\mathbb{R}$, and the distance $d_{\mathbb{R}}$ on $\mathbb{R}$ are parameters. Sequences are as in Sequences (i), and Cauchy sequences as in Cauchy Sequences of Real Numbers (i).

(i) Cauchy sequences. The condition "$x_{i}$ is a Cauchy sequence in $\mathbb{R}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) The class of Cauchy sequences. There is a class $K$ such that, for every class $a$, $a\in K$ if and only if $a$ is a Cauchy sequence in $\mathbb{R}$.