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

Projective Planes

Michal Muzalewski
Warsaw University, Bialystok


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.

MML Identifier: PROJPL_1

The terminology and notation used in this paper have been introduced in the following articles [1] [5] [3] [4] [2]

Contents (PDF format)

  1. Projective Spaces
  2. Projective Planes
  3. Some Useful Propositions


[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]