:: deftheorem Def1 defines dist TOPREAL6:def 1 :
for n being Nat
for a, b being Point of (TOP-REAL n)
for b₄ being Real holds
( b₄ = dist (a,b) iff ex p, q being Point of (Euclid n) st
( p = a & q = b & b₄ = dist (p,q) ) );