Теорема бабочки

Теорема, которой даётся название и которая не теряется в куче подобных ей - или крайне полезная или очень красивая.
Теорема бабочки - на мой взгляд относится ко второму типу, хотя она несомненна может быть применена в подходящем случае. Звучит она следующим образом:

Пусть $P$ - середина хорды $EF$. Через точку $P$ проведены две произвольные хорды $BD$ и $CA$. Отрезки $AB$ и $CD$ пересекают хорду $EF$ в точках $X$ и $Y$ соответственно. Тогда $P$ - середина отрезка $XY$.

Для начала, давайте проверим так ли это. Выберите пункт проверить и попробуйте поизменять график.

Теорема о бабочке была доказана в 1815 году английским математиком Уильямом Джорджем Горнером (кто знаком, именно в честь него названа схема Горнера деления многочленов). Первый раз теорема увидела свет в английском журнале "Gentleman's Diary". Приведём одно из доказательств теоремы о бабочке.

Доказательство.

1. Опустим перпендикуляры из точек $X$ и $Y$ на прямые $AC$ и $BD$ ( нажмите "Показать решение" на чертеже).
2. Т.к. треугольники $BXX_2$ и $CYY_1$ подобны, то $$\frac{XX_2}{YY_1}=\frac{BX}{CY}$$
3. Треугольник $XPX_1$  подобен  $YPY_1$, а треугольник $XPX_2$ подобен $YPY_2$, следовательно $$\frac{XX_1}{YY_1}=\frac{PX}{PY}=\frac{XX_2}{YY_2}$$
4. Так как треугольник $AXX_1$ подобен треугольнику $DYY_2$, то $$\frac{XX_1}{YY_2}=\frac{AX}{DY}$$
5. Заметим, что $EP=PF$. Обозначив для удобства $EP=PF=k$  в результате получаем:
   $$\frac{PX^2}{PY^2}=\frac{XX_1 \times XX_2}{YY_1 \times YY_2}= \frac{AX \times XB}{DY \times YC}=\frac{EX \times XF}{FY \times YE}=\frac{(k-PX)(k+PX)}{(k-PY)(k+PY)}=\frac{k^2 - PX^2}{k^2 - PY^2}.$$
   Значит, $\frac{PX^2}{PY^2}=\frac{k^2-PX^2}{k^2-PY^2},$ т.е. $PX^2 (k^2-PY^2)=PY^2(k^2-PX^2)$.
   Раскрыв скобки получаем $PX^2=PY^2$ что и значит что $PX=PY$.

Замечу, что это далеко не единственное доказательство. Ещё девять других интересных доказательств можно найти в заметке Александра Спивака "Десять бабочек". Задачи связанные с теоремой можно найти в замечательной книге Коксетера и Грейтцера "Новые встречи с геометрией".
От себя хочу добавить, что у задачи есть дополнение. Если продолжить хорду $EF$ до прямой, и провести прямые $BC$ и $AD$, то точки пересечения этих прямых с $EF$ так же будут равноудалены от точки $P$. Попробуйте сами построить такой график и доказать это утверждение.