[proofplan] The key insight is that a well-ordering provides a unique "first missing element" whenever we have a proper subset. Given a proper initial segment $Y$ of a well-ordered set $(X, <)$, the complement $X \setminus Y$ is non-empty, so it admits a minimum $x$. The initial-segment property of $Y$ and the minimality of $x$ together force $Y = I_x = \{y \in X : y < x\}$, with both containments established by a direct trichotomy argument. Uniqueness follows because distinct choices of $x$ produce distinct sets $I_x$ in any linear order. [/proofplan] [step:Extract the first missing element $x := \min(X \setminus Y)$] Since $Y$ is a proper initial segment of $X$, by definition $Y \subsetneq X$, so the set $X \setminus Y$ is non-empty. Because $(X, <)$ is well-ordered, every non-empty subset of $X$ has a least element. Define \begin{align*} x := \min(X \setminus Y). \end{align*} Then $x \in X \setminus Y$, so $x \in X$ and $x \notin Y$, and $x \leq z$ for every $z \in X \setminus Y$. [guided] We want to show $Y = I_x$ for some $x \in X$. Where should $x$ come from? Since $Y$ is the set of "things below $x$," the element $x$ itself must not lie in $Y$ but must be "just above" $Y$. The natural candidate is therefore the smallest element of $X$ that is *not* in $Y$. We must justify that such a smallest element exists. Two conditions are needed: 1. **Non-emptiness of $X \setminus Y$.** This uses the assumption that $Y$ is a *proper* initial segment, meaning $Y \subsetneq X$. Hence there is at least one element of $X$ not in $Y$, so $X \setminus Y \neq \varnothing$. 2. **Existence of a minimum of $X \setminus Y$.** This uses the well-ordering hypothesis: by the definition of a well-order, every non-empty subset of $X$ has a least element. Applying this to the non-empty set $X \setminus Y$ yields the minimum. We therefore define \begin{align*} x := \min(X \setminus Y), \end{align*} which satisfies $x \in X$, $x \notin Y$, and $x \leq z$ for every $z \in X$ with $z \notin Y$. [/guided] [/step] [step:Show $I_x \subseteq Y$ using the minimality of $x$] Let $y \in I_x$, so $y \in X$ and $y < x$. We must show $y \in Y$. Suppose for contradiction that $y \notin Y$. Then $y \in X \setminus Y$, so by minimality of $x$ we have $x \leq y$. But we also have $y < x$, yielding $x \leq y < x$, a contradiction. Hence $y \in Y$, proving $I_x \subseteq Y$. [/step] [step:Show $Y \subseteq I_x$ using the initial-segment property of $Y$] Let $y \in Y$. We show $y < x$, i.e. $y \in I_x$. By trichotomy of the linear order $<$ on $X$, exactly one of $y < x$, $y = x$, $y > x$ holds. **Case $y = x$.** Then $x = y \in Y$, contradicting $x \notin Y$ (which holds by construction since $x \in X \setminus Y$). **Case $y > x$.** Since $Y$ is an initial segment of $X$, by definition $z \in Y$ and $w < z$ together imply $w \in Y$. Applying this with $z = y$ and $w = x$ (recall $x < y$), we obtain $x \in Y$, again contradicting $x \notin Y$. Therefore $y < x$, so $y \in I_x$. This gives $Y \subseteq I_x$. [guided] We must show every $y \in Y$ satisfies $y < x$. The tool available is trichotomy: exactly one of $y < x$, $y = x$, or $y > x$ holds. We rule out the last two. **Ruling out $y = x$.** If $y = x$, then since $y \in Y$ we would get $x \in Y$. But $x \in X \setminus Y$ by construction, so $x \notin Y$. Contradiction. **Ruling out $y > x$.** This is the critical step where the *initial-segment* hypothesis on $Y$ is used. Recall the defining property: $Y$ is an initial segment of $X$ when, for all $z \in Y$ and all $w \in X$ with $w < z$, we have $w \in Y$. In other words, $Y$ is closed downward under $<$. We apply this closure property with $z = y \in Y$ and $w = x$. The hypothesis $w < z$ becomes $x < y$, which is exactly the assumption of this case. The conclusion $w \in Y$ becomes $x \in Y$ — again contradicting $x \notin Y$. By elimination, $y < x$, so $y \in I_x$. [/guided] [/step] [step:Conclude equality $Y = I_x$ and verify uniqueness of $x$] Combining the two containments from the previous steps gives $Y = I_x$. For uniqueness, suppose $x, x' \in X$ both satisfy $Y = I_x = I_{x'}$. We show $x = x'$. By trichotomy, if $x \neq x'$ then either $x < x'$ or $x' < x$. Assume (without loss of generality, by symmetry of the argument) that $x < x'$. Then $x \in I_{x'}$ by definition of $I_{x'}$, so $x \in Y$. But also $Y = I_x$, so $x \in I_x$, meaning $x < x$ — impossible since $<$ is irreflexive. The reverse case $x' < x$ is identical with the roles swapped. Hence $x = x'$, and $x$ is the unique element of $X$ with $Y = I_x$. [guided] We have $I_x \subseteq Y$ from the previous-to-last step and $Y \subseteq I_x$ from the last step, so \begin{align*} Y = I_x. \end{align*} For uniqueness, suppose $x$ and $x'$ both represent $Y$, i.e. $I_x = I_{x'} = Y$. We use trichotomy on $(X, <)$ to eliminate $x \neq x'$. Suppose $x < x'$. Then $x \in I_{x'} = Y = I_x$, so $x \in I_x$, which by definition of $I_x$ means $x < x$. This contradicts the irreflexivity of the strict order $<$ on a well-ordered set. The case $x' < x$ is symmetric: swapping the roles of $x$ and $x'$ gives $x' < x'$, again impossible. The only remaining possibility is $x = x'$, establishing uniqueness. This completes the proof. [/guided] [/step]