 Fixed-point theorem for the untyped lambda calculus

Every lambda term $F$ has a fixed point: the termsatisfies $X{\equiv }_{\beta }F(X)$. Equivalently, a fixed-point combinator such assatisfies $YF{\equiv }_{\beta }F(YF)$ for every $F$.