Consider the following attempt at a ``thought-free'' proof of Morley's Theorem.
Let $(x_1,y_1)$, $(x_2,y_2)$ and $(x_3,y_3)$ denote three vertices of a generic triangle.
Let $(a_1,b_1)$, $(a_2,b_2)$ and $(a_3,b_3)$ denote three more points in the plane.
For all $\lbrace i,j,k\rbrace=\lbrace 1,2,3\rbrace$, we want to impose the condition that the line determined by $(x_i,y_i)$ and $(a_k,b_k)$ bisects the angle from $(a_j,b_j)$ to $(x_i,y_i)$ to $(x_j,y_j)$. Capturing this algebraically amounts to equating two squared cosines: $$ \frac{((x_i-a_k)(x_i-a_j)+(y_i-b_k)(y_i-b_j))^2} {((x_i-a_k)^2+(y_i-b_k)^2)((x_i-a_j)^2+(y_i-b_j)^2)}$$ $$ = \frac{((x_i-a_k)(x_i-x_j)+(y_i-b_k)(y_i-x_j))^2} {((x_i-a_k)^2+(y_i-b_k)^2)((x_i-x_j)^2+(y_i-x_j)^2)} $$ which simplifies first to $$ ((x_i-a_k)(x_i-a_j)+(y_i-b_k)(y_i-b_j))^2((x_i-x_j)^2+(y_i-x_j)^2)$$ $$ - ((x_i-a_k)(x_i-x_j)+(y_i-b_k)(y_i-x_j))^2((x_i-a_j)^2+(y_i-b_j)^2)=0. $$ Then expanding the left side and dividing out by the condition $$ -a_jy_i - b_jx_j + x_ib_j - x_ix_j + y_ix_j + a_jx_j$$ (of having $(a_j,b_j)$,$(x_i,y_i)$ and $(x_j,y_j)$ collinear) leaves $$C_{ijk}:=a_jy_i^3-x_i^3b_j+2x_ix_jy_ib_j-2x_ia_jy_ix_j-2a_ky_i^3+2x_i^3b_k+b_k^2x_ix_j+y_i^3x_j-x_i^3x_j$$ $$-a_k^2y_ix_j+2a_kx_ib_kx_j-2a_kx_jb_ky_i-2a_kb_kb_jy_i+2x_ja_kb_kb_j+2x_jb_ky_ib_j-2x_ja_ky_ib_j$$ $$-2x_jx_ib_kb_j+2a_ky_i^2b_j-a_k^2x_ib_j+2a_kx_i^2b_j+b_k^2x_ib_j-2b_k^2y_ix_i+2a_k^2x_iy_i+x_ja_k^2b_j$$ $$-x_jb_k^2b_j-a_jx_jb_k^2+a_jx_ja_k^2-a_ja_k^2y_i+a_jb_k^2y_i-2a_jb_kx_i^2-2a_jb_ky_i^2-2x_ja_kx_ib_j$$ $$+2a_jx_ja_ky_i-2a_jx_ja_kb_k-2a_jx_ja_kx_i+2a_jx_jb_ky_i+2a_jx_ib_kx_j+2a_ja_kx_ib_k+2a_kx_jy_i^2$$ $$-2y_i^2b_kx_j+b_k^2y_ix_j+2x_i^2a_kx_j+x_i^2y_ix_j-2x_i^2b_kx_j-x_ix_jy_i^2-a_k^2x_ix_j+x_i^2x_ja_j$$ $$-x_jy_i^2b_j+a_jy_ix_i^2-a_jy_i^2x_j+x_i^2b_jx_j-x_ib_jy_i^2-2a_kb_kx_i^2+2a_kb_ky_i^2-2a_ky_ix_i^2+2x_ib_ky_i^2\ .$$
Now for Morley's theorem we would like to conclude that points $(a_1,b_1)$, $(a_2,b_2)$ and $(a_3,b_3)$ form an equilateral triangle. We can easily write down polynomials in $a_1,b_1,a_2,b_2,a_3$ and $b_3$ all of whose vanishing would capture this. For example, it would suffice to prove the vanishing of $$I_{123}:=-2a_1a_2+a_2^2+2b_1^2-2b_1b_2+b_2^2+2a_1a_3-a_3^2-2b_1b_3+b_3^2\ .$$
Since we hope $I_{123}$ will vanish whenever $C_{123},C_{213},C_{312},C_{132},C_{231},C_{321}$ do, we look to find $I_{123}$ in (the radical of) the ideal $$C:=\langle C_{123},C_{213},C_{312},C_{132},C_{231},C_{321}\rangle.$$ Unfortunately, as one can see from the above, all the generators of $C$ vanish if $x_1=y_1=x_2=y_2=x_3=y_3=0$, and so the same must hold for every element of $C$. Nevertheless $I_{123}$ does not vanish on this condition.
The classical nullstellensatz leaves only one way out: the vanishing of $I_{123}$ doesn't follow from the vanishing of all the $C_{ijk}$ without the exploitation of some restriction on the range of the variables such as confining them to the reals.
Question: What insight does the machinery of real algebraic geometry shed on the shape of a proof of Morley's Theorem along the lines of this sketch?