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 p', q' being Point of (TOP-REAL n) such that
A1: p' in {p} and
A2: ( q' in {q} & dist_min {p},{q} = dist p',q' ) by Th42;
p = p' by A1, TARSKI:def 1;
hence dist_min {p},{q} = dist p,q by A2, TARSKI:def 1; :: thesis: verum