EDB — 1ZK

[1ZK]An ordered field \(F\) is archimedean if \(∀ x,y∈ F\) with \(x{\gt}0,y{\gt}0\) there is a \(n∈ℕ\) for which \(n x{\gt}y\). (See [20R]↺↻ for the definition of \(n x\)).