Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Zermelo's Theorem


Bogdan Nowak
Lodz University
Slawomir Bialecki
Lodz University

Summary.

The article contains direct proof of Zermelo's theorem about the existence of a well ordering for any set and the lemma the proof depends on.

Supported by RPBP.III-24.C9.

MML Identifier: WELLSET1

The terminology and notation used in this paper have been introduced in the following articles [4] [3] [5] [2] [1]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The well ordering relations. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[4] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[5] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received October 27, 1989


[ Download a postscript version, MML identifier index, Mizar home page]