theorem Th87: :: JORDAN:87

for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D holds
LSeg (|[0,3]|,(UMP D)) c= north_halfline (UMP D)