let n be Element of NAT ; :: thesis: for p, q being Point of holds dist_min {p},{q} = dist p,q
let p, q be Point of ; :: thesis: dist_min {p},{q} = dist p,q
consider p', q' being Point of 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