let a, b, c, d be Real; :: thesis: 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)) ; :: thesis: verum