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