theorem Th80: :: JORDAN:80

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