# Real positive number/Root/Unique existence/Fact/Proof

Proof

We define recursively nested intervals . We set

and we take for an arbitrary real number with . Suppose that the interval bounds are defined up to index , the intervals fulfil the containment condition and that

holds. We set

and

Hence one bound remains and one bound is replaced by the arithmetic mean of the bounds of the previous interval. In particular, the stated properties hold for all intervals and we have a sequence of nested intervals. Let denote the real number defined by this nested intervals according to fact. Because of exercise, we have

Due to fact, we get

Because of the construction of the interval bounds and due to fact, this is but also , hence .