I think maybe you're overlooking "a *well-founded* relation ⊏ is a well-ordering...

		GrantMoyer on July 2, 2024 \| parent \| context \| favorite \| on: A proof of proof by infinite descent I think maybe you're overlooking "a well-founded relation ⊏ is a well-ordering …". < on the reals is not well-founded. Remember, a well-founded relation requires all leftward chains to be finite. Together with the rest of the given definition, it implies a unique least element.

Yes you are right. My bad. I edited my original comment.