let P, P1 be non empty compact Subset of (TOP-REAL 2); :: thesis: ( 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 A1: ( P is being_simple_closed_curve & P1 is_an_arc_of W-min P, E-max P & P1 c= P ) ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )
then A2: ( Upper_Arc P is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P2 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) ) by JORDAN6:def 8;
A3: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by A1, JORDAN6:def 9;
then A4: E-max P in (Upper_Arc P) /\ (Lower_Arc P) by TARSKI:def 2;
A5: W-min P in (Upper_Arc P) /\ (Lower_Arc P) by A3, TARSKI:def 2;
consider f being Function of I[01] ,((TOP-REAL 2) | P1) such that
A6: ( f is being_homeomorphism & f . 0 = W-min P & f . 1 = E-max P ) by A1, TOPREAL1:def 2;
A7: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def 10 ;
A8: f is one-to-one by A6, TOPS_2:def 5;
A9: f is continuous by A6, TOPS_2:def 5;
dom f = [#] I[01] by A6, TOPS_2:def 5;
then A10: dom f = the carrier of I[01] ;
A11: rng f = [#] ((TOP-REAL 2) | P1) by A6, TOPS_2:def 5
.= P1 by PRE_TOPC:def 10 ;
A12: ( Upper_Arc P c= P & Lower_Arc P c= P ) by A1, JORDAN6:76;
reconsider U2 = Upper_Arc P as Subset of ((TOP-REAL 2) | P) by A1, A7, JORDAN6:76;
U2 = (Upper_Arc P) /\ P by A12, XBOOLE_1:28;
then A13: U2 is closed by A2, JORDAN6:3, JORDAN6:12;
reconsider U3 = Lower_Arc P as Subset of ((TOP-REAL 2) | P) by A1, A7, JORDAN6:76;
U3 = (Lower_Arc P) /\ P by A12, XBOOLE_1:28;
then A14: U3 is closed by A3, JORDAN6:3, JORDAN6:12;

now

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 A15: for r being Real st 0 < r & r < 1 holds
f . r in Lower_Arc P ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

P1 c= Lower_Arc P

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in P1 or y in Lower_Arc P )
assume y in P1 ; :: thesis: y in Lower_Arc P
then consider x being set such that
A16: ( x in dom f & y = f . x ) by A11, FUNCT_1:def 5;
reconsider r = x as Real by A10, A16, BORSUK_1:83;
A17: ( 0 <= r & r <= 1 ) by A16, BORSUK_1:83, XXREAL_1:1;

now

per cases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A17, XXREAL_0:1;

case ( 0 < r & r < 1 ) ; :: thesis: y in Lower_Arc P

hence y in Lower_Arc P by A15, A16; :: thesis: verum

end;

case r = 0 ; :: thesis: y in Lower_Arc P

hence y in Lower_Arc P by A5, A6, A16, XBOOLE_0:def 4; :: thesis: verum

end;

case r = 1 ; :: thesis: y in Lower_Arc P

hence y in Lower_Arc P by A4, A6, A16, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence y in Lower_Arc P ; :: thesis: verum

end;

hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A1, A3, Th18; :: thesis: verum

end;

case A18: ex r being Real st
( 0 < r & r < 1 & not f . r in Lower_Arc P ) ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

now

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 A19: for r being Real st 0 < r & r < 1 holds
f . r in Upper_Arc P ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

P1 c= Upper_Arc P

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in P1 or y in Upper_Arc P )
assume y in P1 ; :: thesis: y in Upper_Arc P
then consider x being set such that
A20: ( x in dom f & y = f . x ) by A11, FUNCT_1:def 5;
reconsider r = x as Real by A10, A20, BORSUK_1:83;
A21: ( 0 <= r & r <= 1 ) by A20, BORSUK_1:83, XXREAL_1:1;

now

per cases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A21, XXREAL_0:1;

case ( 0 < r & r < 1 ) ; :: thesis: y in Upper_Arc P

hence y in Upper_Arc P by A19, A20; :: thesis: verum

end;

case r = 0 ; :: thesis: y in Upper_Arc P

hence y in Upper_Arc P by A5, A6, A20, XBOOLE_0:def 4; :: thesis: verum

end;

case r = 1 ; :: thesis: y in Upper_Arc P

hence y in Upper_Arc P by A4, A6, A20, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence y in Upper_Arc P ; :: thesis: verum

end;

hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A1, A2, JORDAN6:59; :: thesis: verum

end;

case ex r being Real st
( 0 < r & r < 1 & not f . r in Upper_Arc P ) ; :: thesis: contradiction

then consider r2 being Real such that
A22: ( 0 < r2 & r2 < 1 & not f . r2 in Upper_Arc P ) ;
consider r1 being Real such that
A23: ( 0 < r1 & r1 < 1 & not f . r1 in Lower_Arc P ) by A18;
r2 in [.0 ,1.] by A22, XXREAL_1:1;
then f . r2 in rng f by A10, BORSUK_1:83, FUNCT_1:def 5;
then A24: f . r2 in Lower_Arc P by A1, A3, A11, A22, XBOOLE_0:def 3;
r1 in [.0 ,1.] by A23, XXREAL_1:1;
then A25: f . r1 in rng f by A10, BORSUK_1:83, FUNCT_1:def 5;
then A26: f . r1 in Upper_Arc P by A1, A3, A11, A23, XBOOLE_0:def 3;

now

per cases ( r1 <= r2 or r1 > r2 ) ;

case A27: r1 <= r2 ; :: thesis: contradiction

now

per cases ( r1 = r2 or r1 < r2 ) by A27, XXREAL_0:1;

case r1 = r2 ; :: thesis: contradiction

hence contradiction by A1, A3, A11, A22, A23, A25, XBOOLE_0:def 3; :: thesis: verum

end;

case A28: r1 < r2 ; :: thesis: contradiction

A29: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def 10 ;
the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def 10 ;
then rng f c= the carrier of ((TOP-REAL 2) | P) by A1, A29, XBOOLE_1:1;
then reconsider g = f as Function of I[01] ,((TOP-REAL 2) | P) by A10, FUNCT_2:4;
reconsider Q = P as non empty Subset of (Euclid 2) by TOPREAL3:13;
P = P1 \/ P by A1, XBOOLE_1:12;
then (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | P by TOPMETR:5;
then A30: g is continuous by A9, PRE_TOPC:56;
A31: U2 \/ U3 = the carrier of ((Euclid 2) | Q) by A3, TOPMETR:def 2;
(TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) by EUCLID:67;
then consider r0 being Real such that
A32: ( r1 <= r0 & r0 <= r2 & g . r0 in U2 /\ U3 ) by A13, A14, A22, A23, A24, A26, A28, A30, A31, Th17;
r0 < 1 by A22, A32, XXREAL_0:2;
then A33: r0 in dom f by A10, A23, A32, BORSUK_1:83, XXREAL_1:1;
A34: 0 in dom f by A10, BORSUK_1:83, XXREAL_1:1;
A35: 1 in dom f by A10, BORSUK_1:83, XXREAL_1:1;

now

per cases ( g . r0 = W-min P or g . r0 = E-max P ) by A3, A32, TARSKI:def 2;

case g . r0 = W-min P ; :: thesis: contradiction

hence contradiction by A6, A8, A23, A32, A33, A34, FUNCT_1:def 8; :: thesis: verum

end;

case g . r0 = E-max P ; :: thesis: contradiction

hence contradiction by A6, A8, A22, A32, A33, A35, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A36: r1 > r2 ; :: thesis: contradiction

A37: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def 10 ;
the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def 10 ;
then rng f c= the carrier of ((TOP-REAL 2) | P) by A1, A37, XBOOLE_1:1;
then reconsider g = f as Function of I[01] ,((TOP-REAL 2) | P) by A10, FUNCT_2:4;
reconsider Q = P as non empty Subset of (Euclid 2) by TOPREAL3:13;
P = P1 \/ P by A1, XBOOLE_1:12;
then (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | P by TOPMETR:5;
then A38: g is continuous by A9, PRE_TOPC:56;
A39: U2 \/ U3 = the carrier of ((Euclid 2) | Q) by A3, TOPMETR:def 2;
(TOP-REAL 2) | P = TopSpaceMetr ((Euclid 2) | Q) by EUCLID:67;
then consider r0 being Real such that
A40: ( r2 <= r0 & r0 <= r1 & g . r0 in U2 /\ U3 ) by A13, A14, A22, A23, A24, A26, A36, A38, A39, Th17;
r0 < 1 by A23, A40, XXREAL_0:2;
then A41: r0 in dom f by A10, A22, A40, BORSUK_1:83, XXREAL_1:1;
A42: 0 in dom f by A10, BORSUK_1:83, XXREAL_1:1;
A43: 1 in dom f by A10, BORSUK_1:83, XXREAL_1:1;

now

per cases ( g . r0 = W-min P or g . r0 = E-max P ) by A3, A40, TARSKI:def 2;

case g . r0 = W-min P ; :: thesis: contradiction

hence contradiction by A6, A8, A22, A40, A41, A42, FUNCT_1:def 8; :: thesis: verum

end;

case g . r0 = E-max P ; :: thesis: contradiction

hence contradiction by A6, A8, A23, A40, A41, A43, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ; :: thesis: verum

end;

end;

end;

hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) ; :: thesis: verum