let n be Element of 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:37;
then dist p,A <= dist p,{q} by Th41;
hence dist p,A <= dist p,q by Th43; :: thesis: verum