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.III-24.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 non-collinear 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.