let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n)
for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds
dist p9,q9 = |.(p - q).|
let p, q be Point of (TOP-REAL n); :: thesis: for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds
dist p9,q9 = |.(p - q).|
let p9, q9 be Point of (Euclid n); :: thesis: ( p = p9 & q = q9 implies dist p9,q9 = |.(p - q).| )
assume A1: ( p = p9 & q = q9 ) ; :: thesis: dist p9,q9 = |.(p - q).|
reconsider pp = p, qq = q as Element of REAL n by EUCLID:25;
dist p9,q9 = |.(pp - qq).| by A1, Th20;
hence dist p9,q9 = |.(p - q).| by EUCLID:73; :: thesis: verum