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:1;
now assume A4:
P2 \ P1 <> {}
;
contradictionset p = the
Element of
P2 \ P1;
A5:
the
Element of
P2 \ P1 in P2
by A4, XBOOLE_0:def 5;
A6:
not the
Element of
P2 \ P1 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 1;
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 1;
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:56;
then A17:
dom (f2 ") =
[#] ((TOP-REAL n) | P2)
by TOPS_2:def 5
.=
P2
by PRE_TOPC:def 5
;
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:40, FUNCT_2:7, TOPMETR:17, TOPMETR:20;
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 6;
A23:
dom f1 =
[#] I[01]
by A7, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
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:13;
A27:
g . 1
= (f2 ") . p2
by A9, A18, A25, FUNCT_1:13;
A28:
dom f2 =
[#] I[01]
by A11, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then A29:
0 in dom f2
by XXREAL_1:1;
A30:
1
in dom f2
by A28, XXREAL_1:1;
ba1:
f2 is
onto
by A15, FUNCT_2:def 3;
then A31:
(f2 ") . p1 = (f4 ") . p1
by A14, TOPS_2:def 4;
A32:
(f2 ") . p2 = (f4 ") . p2
by A14, ba1, TOPS_2:def 4;
A33:
g . 0 = 0
by A12, A14, A26, A29, A31, FUNCT_1:32;
A34:
g . 1
= 1
by A13, A14, A27, A30, A32, FUNCT_1:32;
the
Element of
P2 \ P1 in the
carrier of
((TOP-REAL n) | P29)
by A5, PRE_TOPC:8;
then A35:
(f2 ") . the
Element of
P2 \ P1 in the
carrier of
I[01]
by FUNCT_2:5;
A36:
now assume
(f2 ") . the
Element of
P2 \ P1 in rng g
;
contradictionthen consider x being
set such that A37:
x in dom g
and A38:
(f2 ") . the
Element of
P2 \ P1 = g . x
by FUNCT_1:def 3;
A39:
(f2 ") . the
Element of
P2 \ P1 = (f2 ") . (f1 . x)
by A18, A37, A38, FUNCT_1:12;
A40:
x in dom f1
by A18, A37, FUNCT_1:11;
A41:
f1 . x in dom (f2 ")
by A18, A37, FUNCT_1:11;
f2 " is
one-to-one
by A16, TOPS_2:def 5;
then
the
Element of
P2 \ P1 = f1 . x
by A5, A17, A39, A41, FUNCT_1:def 4;
then A42:
the
Element of
P2 \ P1 in rng f1
by A40, FUNCT_1:def 3;
rng f1 =
[#] ((TOP-REAL n) | P1)
by A7, TOPS_2:def 5
.=
P1
by PRE_TOPC:def 5
;
hence
contradiction
by A4, A42, XBOOLE_0:def 5;
verum end; reconsider r =
(f2 ") . the
Element of
P2 \ P1 as
Real by A35, BORSUK_1:40;
A43:
rng f2 =
[#] ((TOP-REAL n) | P2)
by A11, TOPS_2:def 5
.=
P2
by PRE_TOPC:def 5
;
A44:
r <= 1
by A35, BORSUK_1:40, XXREAL_1:1;
A49:
0 < r
by A35, A45, BORSUK_1:40, 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:6;
the
carrier of
((TOP-REAL n) | P1) =
[#] ((TOP-REAL n) | P1)
.=
P1
by PRE_TOPC:def 5
;
then
rng f1 c= dom (f2 ")
by A3, A17, XBOOLE_1:1;
then dom g =
dom f1
by A18, RELAT_1:27
.=
[#] I[01]
by A7, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then
rc in dom g
by A51, A52, XXREAL_1:1;
hence
contradiction
by A36, A50, FUNCT_1:def 3;
verum end;
then
P2 c= P1
by XBOOLE_1:37;
hence
P1 = P2
by A3, XBOOLE_0:def 10; verum