MDLD/axiom of Archimedes (R)

Start=axiom of Archimedes (R) Target=Ordered field/Archimedean property/Definition