let n be Nat; :: thesis: for A being non empty Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)
let A be non empty Subset of (TOP-REAL n); :: thesis: for p, q being Point of (TOP-REAL n) st q in A holds
dist (p,A) <= dist (p,q)
let p, q be Point of (TOP-REAL n); :: thesis: ( q in A implies dist (p,A) <= dist (p,q) )
assume q in A ; :: thesis: dist (p,A) <= dist (p,q)
then {q} c= A by ZFMISC_1:31;
then dist (p,A) <= dist (p,{q}) by Th41;
hence dist (p,A) <= dist (p,q) by Th43; :: thesis: verum