Proof of Completeness of ℝ, Infimum Form: A Nonempty Subset of ℝ Bounded Below Has an Infimum

Since $s$ is a subclass of the set $\mathbb{R}$, it is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i).

By The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), $\mathbb{R}$ with $+$, $\cdot$, $0$, $1$ and $\le$ is an ordered field, and by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (ii) every subset of $\mathbb{R}$ other than the empty set that is bounded above has a supremum. So $F=\mathbb{R}$ satisfies the hypothesis of Infima, the Archimedean Property, Density of the Rationals and Rational Approximation from Below in an Ordered Field Whose Nonempty Sets Bounded Above Have Suprema, and by Infima, the Archimedean Property, Density of the Rationals and Rational Approximation from Below in an Ordered Field Whose Nonempty Sets Bounded Above Have Suprema (i) every nonempty subset of $\mathbb{R}$ that is bounded below has an infimum.

The subset $s$ is nonempty (it has an element $u$, while $\emptyset$ has none by The Empty Set, the Unordered Pair and the Singleton (i)) and bounded below, so it has an infimum $m$ in $(\mathbb{R},\le)$. Moreover $m$ is a set (by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv) and Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iii), $m$ lies in $\operatorname{Lb}(s)$, which is contained in $\mathbb{R}$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (i), and elements of classes are sets by Classes, Membership, Sets and Proper Classes (i)).