Corollary B: any two distinct lines of an STS(7) meet in exactly one point

Theorem lines_meet. Let $S$ be an arbitrary object of type "Steiner triple system on 7 points" (the only hypothesis). This type is defined in the bundle as a structure consisting of:

• a finite set $\mathcal{L}_S$ of subsets of the 7-element point set $\{0,1,\dots,6\}$ (the "lines");
• the condition that every line has exactly 3 elements: $|l| = 3$ for all $l \in \mathcal{L}_S$;
• the condition that for any two points $x \neq y$ there is exactly one line $l \in \mathcal{L}_S$ with $x \in l$ and $y \in l$ (existence and uniqueness).

No other condition is imposed on $S$ (in particular, nothing requires $S$ to be isomorphic to any specific configuration). The statement asserts: for every line $l \in \mathcal{L}_S$ and every line $l' \in \mathcal{L}_S$ with $l \neq l'$ (as subsets of points),

i.e. any two distinct lines of $S$ share exactly one point — neither zero points nor two or more.

Remarks on scope: the theorem quantifies over all such systems $S$ on exactly 7 points; it is not restricted to $S$ being "Fano" in the sense of the imported predicate $\mathrm{IsFano}$ (which says some bijection $e$ of the 7 points maps $\mathcal{L}_S$ onto the lines $\{\{i, i+1, i+3\} : i \in \mathbb{Z}/7\}$, addition mod 7), and neither that predicate, the concrete system fano, nor the "role colouring" definition from the imported files appears in the statement. The hypothesis set is satisfiable (the concrete system with lines $\{i, i+1, i+3\}$, $i \in \mathbb{Z}/7$, is a Steiner triple system on 7 points by the bundle's own construction), so the statement is not vacuous. If $\mathcal{L}_S$ had fewer than two lines the claim would hold trivially, but the pair-covering condition on 7 points forces lines to exist.