For a well-ordered set , let contain the points whose strict initial segments are nonempty and have no greatest element, and iterate this operation transfinitely, taking intersections at limit stages. Every nonempty derivative loses at least its least element. If no derivative became empty, choosing one point from each successive difference would inject the ordinal supplied by Hartogs theorem for into , a contradiction.
Codex Wiki