a well-ordered subset of \R is countable

Stream: Is there code for X?

[Kenny Lau]

do we know that a well-ordered subset of \R is countable?

[Kenny Lau]

proof: successor function exists

[Kevin Buzzard]

Conversely I believe any countable ordinal can be order-embedded in R

[David Wärn]

We should at least have Kevin's converse result soon, as a special case of "any countable order embeds in any dense order"