Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
OneDimensional Congruence of Segments, Basic Facts and Midpoint Relation

Barbara Konstanta

Siedlce Agricultural, and Pedagogical University

Urszula Kowieska

Siedlce Agricultural, and Pedagogical University

Grzegorz Lewandowski

Siedlce Agricultural, and Pedagogical University

Krzysztof Prazmowski

Warsaw University, Bialystok
Summary.

We study a theory of onedimensional congruence of segments.
The theory is characterized by a suitable formal axiom system; as a model of
this system one can take the structure obtained from any weak directed
geometrical bundle, with the congruence interpreted as in the case of
``classical" vectors. Preliminary consequences of our axiom system are
proved, basic relations of maximal distance and of midpoint are defined, and
several fundamental properties of them are established.
Supported by RPBP.III24.C3.
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[2]
[5]
[3]
[6]
[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.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [5]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received October 4, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]