set f = Eucl_dist n;
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; JORDAN_A:def 2 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; 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
; (Eucl_dist n) .: V c= N
let s be object ; TARSKI:def 3 ( not s in (Eucl_dist n) .: V or s in N )
assume A7:
s in (Eucl_dist n) .: V
; 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).|
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; verum