let N be Nat; for p1, p2 being Point of (TOP-REAL N)
for x1, x2 being Point of (Euclid N) st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist (x1,x2)
let p1, p2 be Point of (TOP-REAL N); for x1, x2 being Point of (Euclid N) st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist (x1,x2)
let x1, x2 be Point of (Euclid N); ( x1 = p1 & x2 = p2 implies |.(p1 - p2).| = dist (x1,x2) )
assume A1:
( x1 = p1 & x2 = p2 )
; |.(p1 - p2).| = dist (x1,x2)
reconsider x19 = x1, x29 = x2 as Element of REAL N ;
(Pitag_dist N) . (x19,x29) =
|.(x19 - x29).|
by EUCLID:def 6
.=
|.(p1 - p2).|
by A1
;
hence
|.(p1 - p2).| = dist (x1,x2)
by METRIC_1:def 1; verum