Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

## Parallelity Spaces

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

### Summary.

In the monography [6] W. Szmielew introduced the parallelity planes $\langle S$; $\parallel \rangle$, where $\parallel \subseteq S\times S\times S\times S$. In this text we omit upper bound axiom which must be satisfied by the parallelity planes (see also E.Kusak [4]). Further we will list those theorems which remain true when we pass from the parallelity planes to the parallelity spaces. We construct a model of the parallelity space in Abelian group $\langle F\times F\times F; +_F, -_F, {\bf 0}_F \rangle$, where $F$ is a field.

Supported by RPBP.III-24.C6.

#### MML Identifier: PARSP_1

The terminology and notation used in this paper have been introduced in the following articles [8] [3] [11] [9] [7] [2] [1] [10] [5]

Contents (PDF format)

#### Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[4] Eugeniusz Kusak. A new approach to dimension-free affine geometry. \em Bull. Acad. Polon. Sci. Ser. Sci. Math., 27(11--12):875--882, 1979.
[5] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[6] Wanda Szmielew. \em From Affine to Euclidean Geometry, volume 27. PWN -- D.Reidel Publ. Co., Warszawa -- Dordrecht, 1983.
[7] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[8] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[9] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[10] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[11] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.