let n be Element of NAT ; for P1, P2 being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let P1, P2 be Subset of (TOP-REAL n); for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let p1, p2 be Point of (TOP-REAL n); ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 implies P1 = P2 )
assume that
A1:
P1 is_an_arc_of p1,p2
and
A2:
P2 is_an_arc_of p1,p2
and
A3:
P1 c= P2
; P1 = P2
reconsider P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL n) by A1, A2, TOPREAL1:4;
now assume A4:
P2 \ P1 <> {}
;
contradictionconsider p being
Element of
P2 \ P1;
A5:
p in P2
by A4, XBOOLE_0:def 5;
A6:
not
p in P1
by A4, XBOOLE_0:def 5;
consider f1 being
Function of
I[01],
((TOP-REAL n) | P19) such that A7:
f1 is
being_homeomorphism
and A8:
f1 . 0 = p1
and A9:
f1 . 1
= p2
by A1, TOPREAL1:def 2;
A10:
f1 is
continuous
by A7, TOPS_2:def 5;
consider f2 being
Function of
I[01],
((TOP-REAL n) | P29) such that A11:
f2 is
being_homeomorphism
and A12:
f2 . 0 = p1
and A13:
f2 . 1
= p2
by A2, TOPREAL1:def 2;
reconsider f4 =
f2 as
Function ;
A14:
f2 is
one-to-one
by A11, TOPS_2:def 5;
A15:
rng f2 = [#] ((TOP-REAL n) | P2)
by A11, TOPS_2:def 5;
A16:
f2 " is
being_homeomorphism
by A11, TOPS_2:70;
then A17:
dom (f2 ") =
[#] ((TOP-REAL n) | P2)
by TOPS_2:def 5
.=
P2
by PRE_TOPC:def 10
;
f2 " is
continuous
by A11, TOPS_2:def 5;
then consider h being
Function of
I[01],
I[01] such that A18:
h = (f2 ") * f1
and A19:
h is
continuous
by A3, A10, Th58;
reconsider h1 =
h as
Function of
(Closed-Interval-TSpace (0,1)),
R^1 by BORSUK_1:83, FUNCT_2:9, TOPMETR:24, TOPMETR:27;
for
F1 being
Subset of
R^1 st
F1 is
closed holds
h1 " F1 is
closed
then reconsider g =
h1 as
continuous Function of
(Closed-Interval-TSpace (0,1)),
R^1 by PRE_TOPC:def 12;
A23:
dom f1 =
[#] I[01]
by A7, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:83
;
then A24:
0 in dom f1
by XXREAL_1:1;
A25:
1
in dom f1
by A23, XXREAL_1:1;
A26:
g . 0 = (f2 ") . p1
by A8, A18, A24, FUNCT_1:23;
A27:
g . 1
= (f2 ") . p2
by A9, A18, A25, FUNCT_1:23;
A28:
dom f2 =
[#] I[01]
by A11, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:83
;
then A29:
0 in dom f2
by XXREAL_1:1;
A30:
1
in dom f2
by A28, XXREAL_1:1;
A31:
(f2 ") . p1 = (f4 ") . p1
by A14, A15, TOPS_2:def 4;
A32:
(f2 ") . p2 = (f4 ") . p2
by A14, A15, TOPS_2:def 4;
A33:
g . 0 = 0
by A12, A14, A26, A29, A31, FUNCT_1:54;
A34:
g . 1
= 1
by A13, A14, A27, A30, A32, FUNCT_1:54;
p in the
carrier of
((TOP-REAL n) | P29)
by A5, PRE_TOPC:29;
then A35:
(f2 ") . p in the
carrier of
I[01]
by FUNCT_2:7;
A36:
now assume
(f2 ") . p in rng g
;
contradictionthen consider x being
set such that A37:
x in dom g
and A38:
(f2 ") . p = g . x
by FUNCT_1:def 5;
A39:
(f2 ") . p = (f2 ") . (f1 . x)
by A18, A37, A38, FUNCT_1:22;
A40:
x in dom f1
by A18, A37, FUNCT_1:21;
A41:
f1 . x in dom (f2 ")
by A18, A37, FUNCT_1:21;
f2 " is
one-to-one
by A16, TOPS_2:def 5;
then
p = f1 . x
by A5, A17, A39, A41, FUNCT_1:def 8;
then A42:
p in rng f1
by A40, FUNCT_1:def 5;
rng f1 =
[#] ((TOP-REAL n) | P1)
by A7, TOPS_2:def 5
.=
P1
by PRE_TOPC:def 10
;
hence
contradiction
by A4, A42, XBOOLE_0:def 5;
verum end; reconsider r =
(f2 ") . p as
Real by A35, BORSUK_1:83;
A43:
rng f2 =
[#] ((TOP-REAL n) | P2)
by A11, TOPS_2:def 5
.=
P2
by PRE_TOPC:def 10
;
A44:
r <= 1
by A35, BORSUK_1:83, XXREAL_1:1;
A49:
0 < r
by A35, A45, BORSUK_1:83, XXREAL_1:1;
r < 1
by A44, A47, XXREAL_0:1;
then consider rc being
Real such that A50:
g . rc = r
and A51:
0 < rc
and A52:
rc < 1
by A33, A34, A49, TOPREAL5:12;
the
carrier of
((TOP-REAL n) | P1) =
[#] ((TOP-REAL n) | P1)
.=
P1
by PRE_TOPC:def 10
;
then
rng f1 c= dom (f2 ")
by A3, A17, XBOOLE_1:1;
then dom g =
dom f1
by A18, RELAT_1:46
.=
[#] I[01]
by A7, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:83
;
then
rc in dom g
by A51, A52, XXREAL_1:1;
hence
contradiction
by A36, A50, FUNCT_1:def 5;
verum end;
then
P2 c= P1
by XBOOLE_1:37;
hence
P1 = P2
by A3, XBOOLE_0:def 10; verum