A total order of $Fin n$ is represented by a permutation $π$, with $π v$ the position of $v$. Consecutive pairs are counted by their earlier endpoint: $u$ contributes exactly when some $v$ has natural-number position $(π u).val + 1$ and precisely one of $u$ and $v$ lies in the set. Comparing the natural values, rather than adding inside $Fin n$, avoids turning the last and first positions into an artificial cyclic pair.

The crossing number is a natural supremum. Every crossing count is at most $n - 1$, so the set is bounded; for an empty family the natural convention $sSup ∅ = 0$ gives the expected crossing number zero. $IsWelzlOrder$ is a $Prop$-valued bound rather than a structure carrying data derivable from the order and the set system.