let a, b, c, d be Real; dist (|[a,b]|,|[c,d]|) = sqrt (((a - c) ^2) + ((b - d) ^2))
A1:
( |[a,b]| `1 = a & |[a,b]| `2 = b & |[c,d]| `1 = c & |[c,d]| `2 = d )
by EUCLID:52;
reconsider P = |[a,b]|, Q = |[c,d]| as Point of (Euclid 2) by EUCLID:22;
dist (|[a,b]|,|[c,d]|) =
dist (P,Q)
by TOPREAL6:def 1
.=
(Pitag_dist 2) . (P,Q)
by METRIC_1:def 1
.=
sqrt (((a - c) ^2) + ((b - d) ^2))
by A1, TOPREAL3:7
;
hence
dist (|[a,b]|,|[c,d]|) = sqrt (((a - c) ^2) + ((b - d) ^2))
; verum