:: deftheorem defines realize-max-dist-in JORDAN24:def 1 :
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for a, b being Point of (TOP-REAL n) holds
( a,b realize-max-dist-in A iff ( a in A & b in A & ( for x, y being Point of (TOP-REAL n) st x in A & y in A holds
dist (a,b) >= dist (x,y) ) ) );