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:56;
A3:
( |[r2,s2]| `1 = r2 & |[r2,s2]| `2 = s2 )
by EUCLID:56;
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:12
; verum