theorem Th73: :: JORDAN:73

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