let r1, s1, r2, 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 A1:
( u = |[r1,s1]| & v = |[r2,s2]| )
; dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
A2:
( |[r1,s1]| `1 = r1 & |[r1,s1]| `2 = s1 )
by EUCLID:52;
A3:
( |[r2,s2]| `1 = r2 & |[r2,s2]| `2 = s2 )
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, TOPREAL3:7
; verum