| context | $X$ |
| definiendum | $A\in \mathrm{FallingSequence}(X) $ |
| postulate | $A\in \mathrm{InfSequence}(X) $ |
| $n\in \mathbb N$ |
| postulate | $A_{n+1}\subseteq A_n $ |
For falling sequences we have: $\lim_{n\to\infty}A_n=\bigcap_{n=1}^\infty A_n$.
For growing sequences we have: $\lim_{n\to\infty}A_n=\bigcup_{n=1}^\infty A_n$.
| predicate | $A_n\downarrow \hat A \equiv A\in \mathrm{FallingSequence}(X)\ \land\ \lim_{n\to\infty}A_n=\hat A$ |