distinct improper points then $[a,b]_{\operatorname{L^\infty}}$ is the improper line through $a, b$. So $$\label{eq:implines}
  \lines^\infty := \bset{ [a,b]_{\operatorname{L^\infty}}\colon a,b\in S\setminus\pointsout }$$ is the set of all improper lines of $\fixproj$. Now, the incidence between an improper point $a$ and an improper line $k$ may be formally expressed as follows: $$a\in k\iff (\exists b,c\in S)\bigl[\, k = [b,c]_{\operatorname{L^\infty}} \Land \operatorname{L^\infty}(a,b,c) \,\bigr].$$ Finally the underlying projective space $$\fixproj = \struct{S,\linesout\cup \lines^\infty}$$ and the horizon $\bstruct{S^\infty, \lines^\infty}$ are both definable in $\fixout$ which constitutes our main theorem \[thm:main-proj\].

Partial projective spaces {#sec:pps}
=========================

Following the idea of partial projective planes founded in [@hall], as well as the idea of partial affine spaces investigated in [@partaffine], a *partial projective space* $\pps$ can be defined as a projective space $\fixproj=\struct{S, \lines}$ with a family $\rlines$ of its lines deleted. Hence $\pps = \struct{S, \ppslines}$, where $\ppslines = \lines\setminus\rlines$ is the set of undeleted lines. Further we assume that $\fixproj$ is at least 3-dimensional and $$\label{eq:pps}
  \text{\itshape there is a line in $\ppslines$ through every point on every plane of\/ $\fixproj$.}$$ The condition is equivalent to requirement that for every point $a$ and a line $l$ of $\fixproj$ such that $a\notin l$ there is a line 