平山：$K$ は九点円の中心
宿田：ふくｓ(殴
平山：$AK$ の定義に $K$ 使いたくないな
宿田：$L,M$ がふわふわしている
兒玉：$BC$ に関して $O$ と対称な点 $O’$？
平山：そっちの方がマシ…なはず…
兒玉：どこかに相似があると信じてる
平山：めっちゃ直角あるからなあ、なんか
平山：$BO’$ と $CM$ も直角に交わるのか
宿田：円 $BLO$ と $CMO$ の交点とか見る？
平山：要するに $O$ から $LM$ への垂線の足やん
兒玉：よく考えたら $AO’$ ってsymmedianじゃん
平山：嘘では？
兒玉：嘘でした…
兒玉：とはいえ接線の交点 $P$ を取るべき？
宿田：相似や共円の一つも見つからんのやばいな
平山：$AO’$ 目線に変えたの微妙説が、特に嬉しさが
兒玉：わかる
平山：$H$ を復元します… 垂線の足 $D,E,F$ と
平山：$DE\parallel MP$ なので、$CF$ と $DE$ の交点 $Y$ で $OMP$ と $HYD$ 相似
平山：同様に $OLP$ で $HXD$ が相似で、四点相似になる
宿田：その相似は見えんなあ
平山：あとは $XY$ と $AK$ の垂直を示せばよくて、$L,M$ は不要
宿田：そう来るか
平山：こう見ると $L,M$ の置き方まあまあ露骨だな
宿田：これもう $ABC$ 要らなくね
平山：$K$ が $DEF$ の外心なのを使うはずで
兒玉：これ見たことあって、$DEF$ の外心と傍心見るやつです
宿田：$KX^{2}-KY^{2}$ って計算できて、円 $DEF$ への方べきの差
平山：突然すごいことを言うね君
宿田：$AX^{2}-AY^{2}$ も傍接円を見ると計算出来て
平山：あー $A$ って傍心だったな… (そっから？)
宿田：あとは $DE,EF,FD$ で表せて、適当に
平山：すごい終わらせ方された…

• 工事中

$A$, $B$, $C$ から対辺におろした垂線の足を $D$, $E$, $F$とし, $\Gamma$ の $B$ における接線と $C$ における接線との交点を $P$, 直線 $BE$ と $DF$ の交点を $X$, 直線 $CF$ と $DE$ の交点を $Y$ とする. 簡単な角度計算により $HX\mathrel{//}LO$, $HY\mathrel{//}MO$, $HD\mathrel{//}OP$, $XD\mathrel{//}LP$, $YD\mathrel{//}MP$ がわかる. よって, 四角形 $HXDY$ と $OLPM$ は相似であり, 特に $XY\mathrel{//}LM$ であるから, $AK\perp XY$ を示せばよい. 以下 $AX^2-AY^2=KX^2-KY^2$ を示す.

$K$ は三角形 $ABC$ の九点円の中心, つまり三角形 $DEF$ の外接円の中心であり, $A$ は三角形 $DEF$ の傍心であることに注意する. 三角形 $DEF$ の外接円の半径を $R$, $EF=d$, $FD=e$, $DE=f$, $s=(d+e+f)/2$ とおく. このとき \[ KX^2-KY^2=(KX^2-R^2)-(KY^2-R^2)=(-DX\cdot FX)-(-DY\cdot EY)=\frac{ef}{d+e}\cdot\frac{df}{d+e}-\frac{fe}{d+f}\cdot\dfrac{de}{d+f} \] である. また, $\angle{D}$ 内の三角形 $DEF$ の傍接円の半径を $r$ とし, $A$ から直線 $DE$, $DF$ におろした垂線の足をそれぞれ $H_e$, $H_f$ とおくと, \[ AX^2-AY^2=(r^2+H_fX^2)-(r^2+H_eY^2)=(s-e+FX)^2-(s-f+EY)^2 =\biggl(s-e+\frac{de}{d+f}\biggr)^2-\biggl(s-f+\frac{df}{d+e}\biggr)^2 \] である. ここで, \[ \biggl(s-e+\frac{de}{d+f}\biggr)^2+\dfrac{fe}{d+f}\cdot\frac{de}{d+f}=\biggl(\frac{d-e+f}{2}\biggr)^2+(d-e+f)\biggl(\frac{de}{d+f}\biggr)+\frac{d^2e^2+de^2f}{(d+f)^2}=\biggl(\frac{d-e+f}{2}\biggr)^2+de=\frac{d^2+e^2+f^2+2de+2df-2ef}{4} \] となり, これは $e$ と $f$ に対して対称であるから, \[ \biggl(s-f+\frac{df}{d+e}\biggr)^2+\frac{ef}{d+e}\cdot\frac{df}{d+e} \] も同じ値になるので, 示された.