for p being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P & p in P holds
- 3 < p `2