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