let P, P1 be non empty compact Subset of (TOP-REAL 2); ( P is being_simple_closed_curve & P1 is_an_arc_of W-min P, E-max P & P1 c= P & not P1 = Upper_Arc P implies P1 = Lower_Arc P )
assume that
A1:
P is being_simple_closed_curve
and
A2:
P1 is_an_arc_of W-min P, E-max P
and
A3:
P1 c= P
; ( P1 = Upper_Arc P or P1 = Lower_Arc P )
A4:
Upper_Arc P is_an_arc_of W-min P, E-max P
by A1, JORDAN6:def 8;
A5: the carrier of ((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P
by PRE_TOPC:def 5
;
then reconsider U2 = Upper_Arc P as Subset of ((TOP-REAL 2) | P) by A1, JORDAN6:61;
reconsider U3 = Lower_Arc P as Subset of ((TOP-REAL 2) | P) by A1, A5, JORDAN6:61;
A6:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A1, JORDAN6:def 9;
U2 = (Upper_Arc P) /\ P
by A1, JORDAN6:61, XBOOLE_1:28;
then A7:
U2 is closed
by A4, JORDAN6:2, JORDAN6:11;
A8:
(Upper_Arc P) \/ (Lower_Arc P) = P
by A1, JORDAN6:def 9;
U3 = (Lower_Arc P) /\ P
by A1, JORDAN6:61, XBOOLE_1:28;
then A9:
U3 is closed
by A6, JORDAN6:2, JORDAN6:11;
A10:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by A1, JORDAN6:def 9;
then A11:
E-max P in (Upper_Arc P) /\ (Lower_Arc P)
by TARSKI:def 2;
A12:
W-min P in (Upper_Arc P) /\ (Lower_Arc P)
by A10, TARSKI:def 2;
consider f being Function of I[01],((TOP-REAL 2) | P1) such that
A13:
f is being_homeomorphism
and
A14:
f . 0 = W-min P
and
A15:
f . 1 = E-max P
by A2, TOPREAL1:def 1;
A16:
f is one-to-one
by A13, TOPS_2:def 5;
A17:
dom f = [#] I[01]
by A13, TOPS_2:def 5;
A18: rng f =
[#] ((TOP-REAL 2) | P1)
by A13, TOPS_2:def 5
.=
P1
by PRE_TOPC:def 5
;
A19:
f is continuous
by A13, TOPS_2:def 5;
now ( ( ( for r being Real st 0 < r & r < 1 holds
f . r in Lower_Arc P ) & ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ) or ( ex r being Real st
( 0 < r & r < 1 & not f . r in Lower_Arc P ) & ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ) )per cases
( for r being Real st 0 < r & r < 1 holds
f . r in Lower_Arc P or ex r being Real st
( 0 < r & r < 1 & not f . r in Lower_Arc P ) )
;
case A24:
ex
r being
Real st
(
0 < r &
r < 1 & not
f . r in Lower_Arc P )
;
( P1 = Upper_Arc P or P1 = Lower_Arc P )now ( ( ( for r being Real st 0 < r & r < 1 holds
f . r in Upper_Arc P ) & ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ) or ( ex r being Real st
( 0 < r & r < 1 & not f . r in Upper_Arc P ) & contradiction ) )per cases
( for r being Real st 0 < r & r < 1 holds
f . r in Upper_Arc P or ex r being Real st
( 0 < r & r < 1 & not f . r in Upper_Arc P ) )
;
case
ex
r being
Real st
(
0 < r &
r < 1 & not
f . r in Upper_Arc P )
;
contradictionthen consider r2 being
Real such that A29:
0 < r2
and A30:
r2 < 1
and A31:
not
f . r2 in Upper_Arc P
;
r2 in [.0,1.]
by A29, A30, XXREAL_1:1;
then
f . r2 in rng f
by A17, BORSUK_1:40, FUNCT_1:def 3;
then A32:
f . r2 in Lower_Arc P
by A3, A8, A18, A31, XBOOLE_0:def 3;
consider r1 being
Real such that A33:
0 < r1
and A34:
r1 < 1
and A35:
not
f . r1 in Lower_Arc P
by A24;
r1 in [.0,1.]
by A33, A34, XXREAL_1:1;
then A36:
f . r1 in rng f
by A17, BORSUK_1:40, FUNCT_1:def 3;
then A37:
f . r1 in Upper_Arc P
by A3, A8, A18, A35, XBOOLE_0:def 3;
now ( ( r1 <= r2 & contradiction ) or ( r1 > r2 & contradiction ) )per cases
( r1 <= r2 or r1 > r2 )
;
case A38:
r1 <= r2
;
contradictionnow ( ( r1 = r2 & contradiction ) or ( r1 < r2 & contradiction ) )per cases
( r1 = r2 or r1 < r2 )
by A38, XXREAL_0:1;
case
r1 = r2
;
contradictionend; case A39:
r1 < r2
;
contradictionreconsider Q =
P as non
empty Subset of
(Euclid 2) by TOPREAL3:8;
A40: the
carrier of
((TOP-REAL 2) | P1) =
[#] ((TOP-REAL 2) | P1)
.=
P1
by PRE_TOPC:def 5
;
the
carrier of
((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P
by PRE_TOPC:def 5
;
then
rng f c= the
carrier of
((TOP-REAL 2) | P)
by A3, A40;
then reconsider g =
f as
Function of
I[01],
((TOP-REAL 2) | P) by A17, FUNCT_2:2;
P = P1 \/ P
by A3, XBOOLE_1:12;
then A41:
(TOP-REAL 2) | P1 is
SubSpace of
(TOP-REAL 2) | P
by TOPMETR:4;
(
U2 \/ U3 = the
carrier of
((Euclid 2) | Q) &
(TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) )
by A8, EUCLID:63, TOPMETR:def 2;
then consider r0 being
Real such that A42:
r1 <= r0
and A43:
r0 <= r2
and A44:
g . r0 in U2 /\ U3
by A19, A7, A9, A30, A33, A32, A37, A39, A41, Th13, PRE_TOPC:26;
r0 < 1
by A30, A43, XXREAL_0:2;
then A45:
r0 in dom f
by A17, A33, A42, BORSUK_1:40, XXREAL_1:1;
A46:
1
in dom f
by A17, BORSUK_1:40, XXREAL_1:1;
A47:
0 in dom f
by A17, BORSUK_1:40, XXREAL_1:1;
now ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )end; hence
contradiction
;
verum end; hence
contradiction
;
verum case A48:
r1 > r2
;
contradictionreconsider Q =
P as non
empty Subset of
(Euclid 2) by TOPREAL3:8;
A49: the
carrier of
((TOP-REAL 2) | P1) =
[#] ((TOP-REAL 2) | P1)
.=
P1
by PRE_TOPC:def 5
;
the
carrier of
((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P
by PRE_TOPC:def 5
;
then
rng f c= the
carrier of
((TOP-REAL 2) | P)
by A3, A49;
then reconsider g =
f as
Function of
I[01],
((TOP-REAL 2) | P) by A17, FUNCT_2:2;
P = P1 \/ P
by A3, XBOOLE_1:12;
then A50:
(TOP-REAL 2) | P1 is
SubSpace of
(TOP-REAL 2) | P
by TOPMETR:4;
(
U2 \/ U3 = the
carrier of
((Euclid 2) | Q) &
(TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) )
by A8, EUCLID:63, TOPMETR:def 2;
then consider r0 being
Real such that A51:
r2 <= r0
and A52:
r0 <= r1
and A53:
g . r0 in U2 /\ U3
by A19, A7, A9, A29, A34, A32, A37, A48, A50, Th13, PRE_TOPC:26;
r0 < 1
by A34, A52, XXREAL_0:2;
then A54:
r0 in dom f
by A17, A29, A51, BORSUK_1:40, XXREAL_1:1;
A55:
1
in dom f
by A17, BORSUK_1:40, XXREAL_1:1;
A56:
0 in dom f
by A17, BORSUK_1:40, XXREAL_1:1;
now ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )end; hence
contradiction
;
verum end; hence
contradiction
;
verum end; hence
(
P1 = Upper_Arc P or
P1 = Lower_Arc P )
;
verum
hence
( P1 = Upper_Arc P or P1 = Lower_Arc P )
; verum