let r1, r2, s1, s2 be Real; for u, v being Point of (Euclid 2) st u = |[r1,s1]| & v = |[r2,s2]| holds
dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
let u, v be Point of (Euclid 2); ( u = |[r1,s1]| & v = |[r2,s2]| implies dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2)) )
assume that
A1:
u = |[r1,s1]|
and
A2:
v = |[r2,s2]|
; dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
A3:
|[r1,s1]| `1 = r1
by EUCLID:52;
A4:
|[r2,s2]| `2 = s2
by EUCLID:52;
A5:
|[r2,s2]| `1 = r2
by EUCLID:52;
A6:
|[r1,s1]| `2 = s1
by EUCLID:52;
thus dist (u,v) =
(Pitag_dist 2) . (u,v)
by METRIC_1:def 1
.=
sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
by A1, A2, A3, A6, A5, A4, TOPREAL3:7
; verum