vanishing on all rank-$k$ matrices (for a recent combinatorial proof of this fact, see [@Sturmfels05 Example 4.12]; in characteristic $0$ this fact is known as the Second Fundamental Theorem for the orthogonal group). Hence the ideal $I_n(K)$ of Theorem \[thm:Main\] is the intersection of the ideal $J_n$ generated by the $3 \times
3$-minors of $(y_{ij})_{i,j=1,\ldots,n}$ with the ring $K[y_{ij}
\mid i>j]$. Theorem \[thm:2factorGB\] implies that one obtains a Gröbner basis of $J_n$, relative to the restriction of the monomial order on $K[y_{ij} \mid i,j \in {{\mathbb N}}, i\geq j]$ to $K[y_{ij} \mid 1 \leq
j < i \leq n]$ by applying all increasing maps $\{1,\ldots,{l(p)}\}
\to \{1,\ldots,n\}$ to all $p \in B \cap K[y_{ij} \mid i >j] $ with ${l(p)} \leq n$. Such an increasing map can be extended to an element of ${\operatorname{Sym}}(n)$, and Remark \[re:PentadMinor\] concludes the proof.

We conclude with some remarks on the computation that proved Theorem \[thm:2factorGB\]. First we need to verify EGB4.

\[lm:FiniteS\] For all $b_0,b_1 \in K[y_{ij} \mid i,j \in {{\mathbb N}},  i \geq j]$ the set $({\mathrm{Inc}({{\mathbb N}})}b_0) \times ({\mathrm{Inc}({{\mathbb N}})}b_1)$ is the union of a finite number of ${\mathrm{Inc}({{\mathbb N}})}$-orbits.

Consider all pairs $(S_0,S_1)$ of sets $S_0,S_1 \subseteq {{\mathbb N}}$ with 