let n be Nat; :: thesis: for A being non empty compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
let A be non empty compact Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
let p be Point of (TOP-REAL n); :: thesis: ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )
consider q, p9 being Point of (TOP-REAL n) such that
A1: q in A and
A2: ( p9 in {p} & dist_min (A,{p}) = dist (q,p9) ) by Th42;
take q ; :: thesis: ( q in A & dist (p,A) = dist (p,q) )
thus q in A by A1; :: thesis: dist (p,A) = dist (p,q)
thus dist (p,A) = dist (p,q) by A2, TARSKI:def 1; :: thesis: verum