let n be Element of NAT ; :: thesis: for A being non empty compact Subset of
for p being Point of ex q being Point of st
( q in A & dist p,A = dist p,q )
let A be non empty compact Subset of ; :: thesis: for p being Point of ex q being Point of st
( q in A & dist p,A = dist p,q )
let p be Point of ; :: thesis: ex q being Point of st
( q in A & dist p,A = dist p,q )
consider q, p' being Point of such that
A1: q in A and
A2: ( p' in {p} & dist_min A,{p} = dist q,p' ) 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