Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994
Association of Mizar Users
Projective Planes

Michal Muzalewski

Warsaw University, Bialystok
Summary.

The line of points $a$, $b$, denoted by $a\cdot b$ and the point of lines
$A$, $B$ denoted by $A\cdot B$ are defined. A few basic theorems related to these
notions are proved. An inspiration for such approach comes from so called
Leibniz program. Let us recall that the Leibniz program is a
program of algebraization of geometry using purely geometric
notions. Leibniz formulated his program in opposition to
algebraization method developed by Descartes.
The terminology and notation used in this paper have been
introduced in the following articles
[1]
[5]
[3]
[4]
[2]

Projective Spaces

Projective Planes

Some Useful Propositions
Bibliography
 [1]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Wojciech Leonczuk and Krzysztof Prazmowski.
Incidence projective spaces.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Wojciech A. Trybulec.
Axioms of incidency.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received July 28, 1994
[
Download a postscript version,
MML identifier index,
Mizar home page]