set f = Eucl_dist n;
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: according to JORDAN_A:def 2 :: thesis: for N being Neighbourhood of (Eucl_dist n) . p ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N
let N be Neighbourhood of (Eucl_dist n) . p; :: thesis: ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N
consider r being Real such that
A1: 0 < r and
A2: N = ].(((Eucl_dist n) . p) - r),(((Eucl_dist n) . p) + r).[ by RCOMP_1:def 6;
p in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then p in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def 2;
then consider p1, p2 being object such that
A3: p1 in the carrier of (TOP-REAL n) and
A4: p2 in the carrier of (TOP-REAL n) and
A5: p = [p1,p2] by ZFMISC_1:84;
reconsider p1 = p1, p2 = p2 as Point of (TOP-REAL n) by A3, A4;
reconsider p19 = p1, p29 = p2 as Element of (Euclid n) by TOPREAL3:8;
A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider q1 = p1, q2 = p2 as Point of (TopSpaceMetr (Euclid n)) ;
reconsider U = Ball (p19,(r / 2)) as a_neighborhood of q1 by A1, GOBOARD6:91, XREAL_1:215;
reconsider W = Ball (p29,(r / 2)) as a_neighborhood of q2 by A1, GOBOARD6:91, XREAL_1:215;
reconsider V = [:U,W:] as a_neighborhood of p by A5, A6, Lm1;
take V ; :: thesis: (Eucl_dist n) .: V c= N
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in (Eucl_dist n) .: V or s in N )
assume A7: s in (Eucl_dist n) .: V ; :: thesis: s in N
then reconsider s = s as Real ;
consider q being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A8: q in V and
A9: (Eucl_dist n) . q = s by A7, FUNCT_2:65;
q in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then q in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def 2;
then consider q1, q2 being object such that
A10: q1 in the carrier of (TOP-REAL n) and
A11: q2 in the carrier of (TOP-REAL n) and
A12: q = [q1,q2] by ZFMISC_1:84;
reconsider q1 = q1, q2 = q2 as Point of (TOP-REAL n) by A10, A11;
reconsider q19 = q1, q29 = q2 as Element of (Euclid n) by TOPREAL3:8;
reconsider q199 = q19, q299 = q29, p199 = p19, p299 = p29 as Element of REAL n ;
A13: q19 in Ball (p19,(r / 2)) by A8, A12, ZFMISC_1:87;
A14: q29 in Ball (p29,(r / 2)) by A8, A12, ZFMISC_1:87;
A15: dist (q19,p19) < r / 2 by A13, METRIC_1:11;
A16: dist (q29,p29) < r / 2 by A14, METRIC_1:11;
A17: |.(q1 - p1).| < r / 2 by A15, SPPOL_1:5;
|.(q2 - p2).| < r / 2 by A16, SPPOL_1:5;
then A18: |.(q1 - p1).| + |.(q2 - p2).| < (r / 2) + (r / 2) by A17, XREAL_1:8;
A19: for p, q being Point of (TOP-REAL n) holds (Eucl_dist n) . [p,q] = |.(p - q).|

proof

let p, q be Point of (TOP-REAL n); :: thesis: (Eucl_dist n) . [p,q] = |.(p - q).|
thus (Eucl_dist n) . [p,q] = (Eucl_dist n) . (p,q)
.= |.(p - q).| by Def1 ; :: thesis: verum

end;

then A20: (Eucl_dist n) . p = |.(p1 - p2).| by A5;
A21: s = |.(q1 - q2).| by A9, A12, A19;
A22: (q1 - q2) - (p1 - p2) = ((q1 - q2) - p1) + p2 by RLVECT_1:29
.= (q1 - (q2 + p1)) + p2 by RLVECT_1:27
.= ((q1 - p1) - q2) + p2 by RLVECT_1:27
.= (q1 - p1) - (q2 - p2) by RLVECT_1:29 ;
A23: |.((q1 - p1) - (q2 - p2)).| <= |.(q1 - p1).| + |.(q2 - p2).| by TOPRNS_1:30;
A24: s - ((Eucl_dist n) . p) <= |.((q1 - q2) - (p1 - p2)).| by A20, A21, TOPRNS_1:32;
((Eucl_dist n) . p) - s <= |.((p1 - p2) - (q1 - q2)).| by A20, A21, TOPRNS_1:32;
then ((Eucl_dist n) . p) - s <= |.((q1 - q2) - (p1 - p2)).| by TOPRNS_1:27;
then ((Eucl_dist n) . p) - s <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, XXREAL_0:2;
then ((Eucl_dist n) . p) - s < r by A18, XXREAL_0:2;
then A25: ((Eucl_dist n) . p) - r < s by XREAL_1:11;
s - ((Eucl_dist n) . p) <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, A24, XXREAL_0:2;
then s - ((Eucl_dist n) . p) < r by A18, XXREAL_0:2;
then s < ((Eucl_dist n) . p) + r by XREAL_1:19;
hence s in N by A2, A25, XXREAL_1:4; :: thesis: verum