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
Summary.

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.III24.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)
Bibliography
 [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]