theorem Th74: :: JORDAN:74

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
P /\ (rectangle ((- 1),1,(- 3),3)) = {|[(- 1),0]|,|[1,0]|}