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.III24.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 dimensionfree affine geometry.
\em Bull. Acad. Polon. Sci. Ser. Sci. Math.,
27(1112):875882, 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.
Received November 23, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]