theorem Th86: :: JORDAN:86

for p being Point of (TOP-REAL 2)
for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D & p in LSeg ((LMP D),|[0,(- 3)]|) holds
p `2 <= (LMP D) `2