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

The Collinearity Structure

Wojciech Skaba
Nicolaus Copernicus University, Torun
Supported by RPBP.III-24.B5.


The text includes basic axioms and theorems concerning the collinearity structure based on Wanda Szmielew [2], pp. 18-20. Collinearity is defined as a relation on Cartesian product $\mizleftcart S, S, S \mizrightcart$ of set $S$. The basic text is preceeded with a few auxiliary theorems (e.g: ternary relation). Then come the two basic axioms of the collinearity structure: A1.1.1 and A1.1.2 and a few theorems. Another axiom: Aks dim, which states that there exist at least 3 non-collinear points, excludes the trivial structures (i.e. pairs $\llangle S, \mizleftcart S, S, S \mizrightcart\rrangle$). Following it the notion of a line is included and several additional theorems are appended.

MML Identifier: COLLSP

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

Contents (PDF format)


[1] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[2] Wanda Szmielew. \em From Affine to Euclidean Geometry, volume 27. PWN -- D.Reidel Publ. Co., Warszawa -- Dordrecht, 1983.
[3] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[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.

Received May 9, 1990

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