theorem Th93: :: JORDAN:93

for A, P being Subset of (TOP-REAL 2) st P is compact & |[(- 1),0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P holds
A c= closed_inside_of_rectangle ((- 1),1,(- 3),3)