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

Wojciech A. Trybulec

Warsaw University

Grzegorz Bancerek

Warsaw University, Bialystok
Summary.

The goal of this article is to prove Kuratowski  Zorn lemma. We prove it
in a number of forms (theorems and schemes).
We introduce the following notions:
a relation is a quasi (or partial, or linear) order,
a relation quasi (or partially, or linearly) orders a set,
minimal and maximal element in a relation,
inferior and superior element of a relation,
a set has lower (or upper) Zorn property w.r.t. a relation.
We prove basic theorems concerning those notions and theorems
that relate them to the notions introduced in [8].
At the end of the article we prove some theorems that belong rather
to [10], [12] or [2].
Supported by RPBP.III24.C1.
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[5]
[9]
[10]
[3]
[12]
[11]
[4]
[2]
[6]
[8]
[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]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Beata Padlewska.
Families of sets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [8]
Wojciech A. Trybulec.
Partially ordered sets.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Edmund Woronowicz and Anna Zalewska.
Properties of binary relations.
Journal of Formalized Mathematics,
1, 1989.
Received September 19, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]