theorem Th79: :: JORDAN:79

for P being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| )