Consider the following theorem:
Let $f\colon E \to E$ have the propery that $f(x)\geq x$, where $(E,\leq)$ is a non-void partially ordered set with the property that every totally ordered subset of $E$ has a least upper bound. Then there is an element $a$ in $E$ such that $a=f(a)$.
My first question is:
does this theorem hold for sets like $[0,1[$? In general, does it hold for generic subsets of $\mathbb{R}$?
This theorem "implies" the Hausdorff maximality theorem, that is "every partially ordered system contains a maximally ordered subsystem."
Proof. If $E$ has no maximal element, then to every $A \in E$ there corresponds an $f(A)$ containing $A$ properly. Thus the preceding theorem is contradicted by the function $f\colon E \to E. \quad \blacksquare$
My second question is:
in proving this statement it seems that we are not taking into account only the fixed point theorem, but the fact that the function $f$ is not defined "concretely". Are we invoking implicitly the axiom of choice?