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

Wojciech Leonczuk

Warsaw University, Bialystok

Henryk Oryszczyszyn

Warsaw University, Bialystok

Krzysztof Prazmowski

Warsaw University, Bialystok
Summary.

We introduce the notion of plane in affine space and
investigate fundamental properties of them. Further we introduce the relation
of parallelism defined for arbitrary subsets. In particular we are concerned
with parallelisms which hold between lines and planes and between planes.
We also define a function which assigns to every line and every point the
unique line passing through the point and parallel to the given line.
With the help of the introduced notions we prove that every at least
3dimensional affine space is Desarguesian and translation.
Supported by RPBP.III24.C2.
MML Identifier:
AFF_4
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[5]
[1]
[2]
[3]
Contents (PDF format)
Bibliography
 [1]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Analytical ordered affine spaces.
Journal of Formalized Mathematics,
2, 1990.
 [2]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Ordered affine spaces defined in terms of directed parallelity  part I.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Henryk Oryszczyszyn and Krzysztof Prazmowski.
Parallelity and lines in affine spaces.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [5]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received December 5, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]