The green lines are perpendicular bisectors of the blue and orange line segments. Prove the red points are concyclic.