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

## Zermelo Theorem and Axiom of Choice

Grzegorz Bancerek
Warsaw University, Bialystok

### Summary.

The article is continuation of [2] and [1], and the goal of it is show that Zermelo theorem (every set has a relation which well orders it - proposition (26)) and axiom of choice (for every non-empty family of non-empty and separate sets there is set which has exactly one common element with arbitrary family member - proposition (27)) are true. It is result of the Tarski's axiom A introduced in [5] and repeated in [6]. Inclusion as a settheoretical binary relation is introduced, the correspondence of well ordering relations to ordinal numbers is shown, and basic properties of equinumerosity are presented. Some facts are based on [4].

#### MML Identifier: WELLORD2

The terminology and notation used in this paper have been introduced in the following articles [6] [7] [8] [3] [2] [1]

Contents (PDF format)

#### Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The well ordering relations. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Kazimierz Kuratowski and Andrzej Mostowski. \em Teoria mnogosci. PTM, Wroc\-law, 1952.
[5] Alfred Tarski. \"Uber Unerreichbare Kardinalzahlen. \em Fundamenta Mathematicae, 30:176--183, 1938.
[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[8] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.