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

Ordered Affine Spaces Defined in Terms of Directed Parallelity --- Part I

Henryk Oryszczyszyn
Warsaw University, Bialystok
Krzysztof Prazmowski
Warsaw University, Bialystok


In the article we consider several geometrical relations in given arbitrary ordered affine space defined in terms of directed parallelity. In particular we introduce the notions of the nondirected parallelity of segments, of collinearity, and the betweenness relation determined by the given relation of directed parallelity. The obtained structures satisfy commonly accepted axioms for affine spaces. At the end of the article we introduce a formal definition of affine space and affine plane (defined in terms of parallelity of segments).

Supported by RPBP.III-24.C2.

MML Identifier: DIRAF

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

Contents (PDF format)


[1] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[3] Henryk Oryszczyszyn and Krzysztof Prazmowski. Analytical ordered affine spaces. Journal of Formalized Mathematics, 2, 1990.
[4] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[5] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[6] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[7] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received May 4, 1990

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