Being neither a minimum element nor a successor of any element implies being a limit point

Question

I am proving the following theorem

Suppose $<_{X}$ strictly order $X$ and $c \in X$ is neither a minimum element of $X$ nor a successor of any $x \in X$. Then $c$ is a limit point.

I think I have constructed a reasonable proof for this statement. However, the proof seems verbose, and it looks more like a logic game rather than a common proof in mathematics. I am seeking opinions on how to write this proof more succinctly.

Proof. Assume that $c$ is not a minimum element. Then there exists some $y \in X$ such that $y <_{X} c$.

Next assume that $c$ is not a successor of any $x \in X$. According to the definition of a successor, we know that for any $x \in X$, either $c \leq_{X} x$, or there exists some $y$, $x <_{X} y$ and $y <_{X} c$. This statement is equivalent to the following statement: for any $x \in X$, either $\lnot\left(x <_{X} c\right)$, or there exists some $y$, $x <_{X} y$ and $y <_{X} c$. This is further equivalent to the following statement: for any $x \in X$, if $x <_{X} c$, then there exists some $y$, $x <_{X} y$ and $y <_{X} c$.

It is now clear that $c$ is a limit point, given the definition of a limit point. As a result, $c \in X$ being neither a minimum element of $X$ nor a successor of any $x \in X$ implies that $c$ is a limit point.

Answer 1

It’s okay, but it really is a bit wordy. You could safely cut it down to something like this:

Suppose that $c$ is neither a minimum element nor a successor. Let $P=\{x\in X:x<_Xc\}$; by hypothesis $P\ne\varnothing$. Let $x\in P$; $c$ is not the successor of $x$, so there is a $y\in X$ such that $x<_Xy<_Xc$. This is the case for each $x\in P$, so by definition $c$ is a limit point.

That really is all that you need to say.