Re: [mizar] How to search for a lemma?

["Robert M. Solovay" <solovay@math.berkeley.edu>]

On Tue, 18 Mar 2003, Freek Wiedijk wrote:
> where < is the order of the ordered field F.  There are many
> non-Archimedean ordered fields, but I think that the field of
> the real numbers is the unique Archimedean complete ordered
> field.

	It's also true that every complete ordered field is Archimedian.
{If not, the set of integers has an upper bound, hence a least upper
bound, say x. But then, easily, x -1 is also an upper bound of Int,
contradicting leastness.}

	--Bob Solovay