for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[0,3]|,|[0,(- 3)]|) meets C