Formal proof for A subset of the real numbers, well ordered with the normal order of $\mathbb R$, is at most $\aleph_0$ I tried to write a formal proof for the theorem: $A$ subset of $\mathbb R$ well ordered by the normal order $\implies A$ is at most of cardinality $\aleph_0$.

Any suggestions?

Thanks.
Now that your question has been answered, let me point out that it may be interesting to observe furthermore that all the countable well-orderings are in fact represented by suborders of $\langle\mathbb{R},\lt\rangle$, and even of $\langle\mathbb{Q},\lt\rangle$. Let me give two proofs. 

The first proof is an elementary exercise in transfinite induction. One shows that every countable ordinal $\alpha$ embeds into $\mathbb{Q}$. Note that $0$ embeds trivially. If an ordinal $\alpha$ embeds, then by composing with an isomorphism of $\mathbb{Q}$ with an interval in $\mathbb{Q}$, we may suppose the embedding is bounded above, and thereby extend it to an embedding of $\alpha+1$. If $\lambda$ is a countable limit ordinal, with $\lambda=\text{sup}_n\alpha_n$, then by induction we may map $\alpha_n$ into $\mathbb{Q}\cap (n,n+1)$, and this is an embedding of an ordinal at least as large as $\lambda$. QED

The second proof is simply to argue that $\langle\mathbb{Q},\lt\rangle$ is universal for countable linear orders: every countable linear order embeds into $\mathbb{Q}$. This is proved by using just the "forth" part of Cantor's famous back-and-forth argument, namely, given a linear order $L=\langle\{p_n\mid n\in\mathbb{N}\},\lt_L\rangle$, then map $p_n$ to a rational $q_n$ so that one has a order-preserving map at each finite stage. The next element $p_{n+1}$ relates to the previous elements either by being above them all, between two of them, or below them all, and we may choose a corresponding $q_{n+1}$ of the same type. So we get an order-preserving  map $L\to \mathbb{Q}$. Thus, in particular, every countable well-ordering embeds into $\mathbb{Q}$. QED
A sketch proof...

Consider $\mathbb{R}$ as the set of equivalence classes of Cauchy sequences of rationals. We define "the normal" partial order on $\mathbb{R}$ by $x \leq y$ iff $(x = y)$ OR $(\forall \langle x_{i} \rangle)(\forall \langle y_{i} \rangle)(\langle x_{i} \rangle \in x$ AND $\langle y_{i} \rangle \in y \rightarrow (\exists n)(n \in \mathbb{N} \rightarrow (\forall m)(m &gt; n \rightarrow x_{m} &lt; y_{m}))))$. For $A$ to be well-ordered under this partial order there can only be at most $\aleph_{0}$ distinct $n$ in the last part of the definition as they are drawn from $\mathbb{N}$.