for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C holds
LSeg (|[0,3]|,(UMP C)) misses P