let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q)
let p, q be Point of (TOP-REAL n); :: thesis: dist_min ({p},{q}) = dist (p,q)
consider p9, q9 being Point of (TOP-REAL n) such that
A1: p9 in {p} and
A2: ( q9 in {q} & dist_min ({p},{q}) = dist (p9,q9) ) by Th42;
p = p9 by A1, TARSKI:def 1;
hence dist_min ({p},{q}) = dist (p,q) by A2, TARSKI:def 1; :: thesis: verum