theorem :: JORDAN:92

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)]|,(LMP D))) /\ D = {(LMP D)}