Kleene fixed-point theorem

In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:
The ascending Kleene chain of "f" is the chain
obtained by iterating "f" on the least element ⊥ of "L". Expressed in a formula, the theorem states that
where formula_7 denotes the least fixed point.
Although Tarski's fixed point theorem 
does not consider how fixed points can be computed by iterating "f" from some seed (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.
Proof.
We first have to show that the ascending Kleene chain of formula_3 exists in formula_9. To show that, we prove the following:
As a corollary of the Lemma we have the following directed ω-chain:
From the definition of a dcpo it follows that formula_19 has a supremum, call it formula_20 What remains now is to show that formula_21 is the least fixed-point.
First, we show that formula_21 is a fixed point, i.e. that formula_23. Because formula_3 is Scott-continuous, formula_25, that is formula_26. Also, since formula_27 and because formula_14 has no influence in determining the supremum we have: formula_29. It follows that formula_23, making formula_21 a fixed-point of formula_3.
The proof that formula_21 is in fact the "least" fixed point can be done by showing that any element in formula_19 is smaller than any fixed-point of formula_3 (because by property of supremum, if all elements of a set formula_36 are smaller than an element of formula_9 then also formula_38 is smaller than that same element of formula_9). This is done by induction: Assume formula_40 is some fixed-point of formula_3. We now prove by induction over formula_42 that formula_43. The base of the induction formula_44 obviously holds: formula_45 since formula_14 is the least element of formula_9. As the induction hypothesis, we may assume that formula_48. We now do the induction step: From the induction hypothesis and the monotonicity of formula_3 (again, implied by the Scott-continuity of formula_3), we may conclude the following: formula_51 Now, by the assumption that formula_40 is a fixed-point of formula_53 we know that formula_54 and from that we get formula_55