let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds dist (p,p) = 0
let p be Point of (TOP-REAL n); :: thesis: dist (p,p) = 0
ex a, b being Point of (Euclid n) st
( a = p & b = p & dist (a,b) = dist (p,p) ) by Def1;
hence dist (p,p) = 0 by METRIC_1:1; :: thesis: verum