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