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

Hessenberg Theorem


Eugeniusz Kusak
Warsaw University, Bialystok
Wojciech Leonczuk
Warsaw University, Bialystok

Summary.

We prove the Hessenberg theorem which states that every Pappian projective space is Desarguesian.

Supported by RPBP.III-24.C6.

MML Identifier: HESSENBE

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

Contents (PDF format)

Bibliography

[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 October 2, 1990

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