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

Wojciech A. Trybulec

Warsaw University

Supported by RPBP.III24.C1.
Summary.

This article is based on {\it ``Foundations of Geometry''} by Karol Borsuk and
Wanda Szmielew ([1]).
The fourth axiom of incidency is weakened. In [1]
it has the form
{\it for any plane there exist three
noncollinear points in the plane}
and in the article
{\it for any plane there exists one point in the plane}.
The original axiom is proved.
The article includes: theorems concerning collinearity of points
and coplanarity of points and lines, basic theorems concerning lines
and planes, fundamental existence theorems, theorems concerning intersection
of lines and planes.
MML Identifier:
INCSP_1
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[4]
[2]
[6]
[3]
[7]
Contents (PDF format)
Bibliography
 [1]
Karol Borsuk and Wanda Szmielew.
\em Foundations of Geometry.
North Holland, 1960.
 [2]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Andrzej Trybulec.
Domains and their Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Andrzej Trybulec.
Enumerated sets.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [6]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received April 14, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]