Corollary A: an STS(7) has $7$ lines, three through each point

Read-back of seven_lines.

Setting. The point set is $[7] = \{0,1,\dots,6\}$, the seven elements of $\mathrm{Fin}\,7$. The theorem has one hypothesis, a structure $S$ of type "$\mathrm{STS}(7)$". Expanding that definition, $S$ is exactly the following data together with two properties:

• a finite set $\mathcal{L} = \mathcal{L}(S)$ of subsets of $[7]$, called lines. Because $\mathcal{L}$ is a set, a line cannot appear twice.
• (size three) every line $\ell \in \mathcal{L}$ has exactly $|\ell| = 3$ points;
• (unique line through a pair) for all points $x, y \in [7]$ with $x \neq y$, there is exactly one $\ell \in \mathcal{L}$ with $x \in \ell$ and $y \in \ell$.

Nothing else is assumed about $S$. There are no further hypotheses and no typeclass assumptions. The hypothesis is satisfiable: the imported file builds one such structure, the "Fano" system whose lines are $\{i, i+1, i+3\}$ (addition mod $7$) for $i \in [7]$. The same imported files also define IsFano, which says a system is isomorphic to that Fano system under some bijection of the points, and RoleColouring. None of these three definitions (IsFano, fano, RoleColouring) appears in the statement.

Claim. For every such $S$, both of the following hold:

Put simply, every Steiner triple system on exactly $7$ points (as defined above) has exactly $7$ lines, and every point lies on exactly $3$ lines.

Scope. The statement covers only $n = 7$ points. It does not claim that $S$ is isomorphic to the Fano plane, and it says nothing about other values of $n$.