let n be Element of 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