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