Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Desargues Theorem In Projective 3-Space

Eugeniusz Kusak
Warsaw University, Bialystok
Supported by RPBP.III-24.C6.


Proof of the Desargues theorem in Fanoian projective at least 3-dimensional space.

MML Identifier: PROJDES1

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

Contents (PDF format)


[1] Wojciech Leonczuk and Krzysztof Prazmowski. Projective spaces. Journal of Formalized Mathematics, 2, 1990.
[2] Wojciech Skaba. The collinearity structure. Journal of Formalized Mathematics, 2, 1990.

Received August 13, 1990

[ Download a postscript version, MML identifier index, Mizar home page]