Fixed-point lemma for normal functions

The fixed-point lemma for normal functions is a basic result in axiomatic set theory stating that any normal function has arbitrarily large fixed points (Levy 1979: p. 117). It was first proved by Oswald Veblen in 1908.
Background and formal statement.
A normal function is a class function formula_1 from the class Ord of ordinal numbers to itself such that:
It can be shown that if formula_1 is normal then formula_1 commutes with suprema; for any nonempty set formula_11 of ordinals,
Indeed, if formula_13 is a successor ordinal then formula_13 is an element of formula_11 and the equality follows from the increasing property of formula_1. If formula_13 is a limit ordinal then the equality follows from the continuous property of formula_1.
A fixed point of a normal function is an ordinal formula_19 such that formula_20.
The fixed point lemma states that the class of fixed points of any normal function is nonempty and in fact is unbounded: given any ordinal formula_21, there exists an ordinal formula_19 such that formula_23 and formula_20.
The continuity of the normal function implies the class of fixed points is closed (the supremum of any subset of the class of fixed points is again a fixed point). Thus the fixed point lemma is equivalent to the statement that the fixed points of a normal function form a closed and unbounded class.
Proof.
The first step of the proof is to verify that "f"(γ) ≥ γ for all ordinals γ and that "f" commutes with suprema. Given these results, inductively define an increasing sequence <α"n"> ("n" < ω) by setting α0 = α, and α"n"+1 = "f"(α"n") for "n" ∈ ω. Let β = sup {α"n" : "n" ∈ ω}, so β ≥ α. Moreover, because "f" commutes with suprema, 
The last equality follows from the fact that the sequence <α"n"> increases. formula_25
As an aside, it can be demonstrated that the β found in this way is the smallest fixed point greater than or equal to α.
Example application.
The function "f" : Ord → Ord, "f"(α) = ωα is normal (see initial ordinal). Thus, there exists an ordinal θ such that θ = ωθ. In fact, the lemma shows that there is a closed, unbounded class of such θ.