The blue line is the perpendicular bisector of the green line segment. Prove the red points are concyclic.