Thanks!

Sarah Amstutz

Thank you for the kind words.

Of course I should have mentioned this. The backward step if not obvious is standard. It's very much like that for Ceva's theorem:

https://www.cut-the-knot.com/Generalization/ceva.shtml.

Let there be three points such that AF/BF * BD/CD * CE/AE = 1 holds. Assume on the contrary that the points are not collinear. Pick up any two. Say D and E. Draw the line DE and find its intersection F' with AB. Then by the "forward" step AF'/BF' * BD/CD * CE/AE = 1. From which AF'/BF' = AF/BF. By subtracting 1
from both sides one gets AB/AF' = AB/AF, from which F' = F.

I have inserted this paragraph into the proof. Many thanks for pointing out this omission.

All the best,
Alexander Bogomolny