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 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 ; :: thesis: ( 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;

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 ; :: thesis: ( 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 :: thesis: ( ( ( 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 ) ) )end;

hence
( P1 = Upper_Arc P or P1 = Lower_Arc P )
; :: thesis: verumf . 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 ) ) ;

end;

f . r in Lower_Arc P or ex r being Real st

( 0 < r & r < 1 & not f . r in Lower_Arc P ) ) ;

case A20:
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 )

f . r in Lower_Arc P ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

P1 c= Lower_Arc P

end;proof

hence
( P1 = Upper_Arc P or P1 = Lower_Arc P )
by A2, A6, Th14; :: thesis: verum
let y be object ; :: 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 object such that

A21: x in dom f and

A22: y = f . x by A18, FUNCT_1:def 3;

reconsider r = x as Real by A21;

A23: r <= 1 by A21, BORSUK_1:40, XXREAL_1:1;

end;assume y in P1 ; :: thesis: y in Lower_Arc P

then consider x being object such that

A21: x in dom f and

A22: y = f . x by A18, FUNCT_1:def 3;

reconsider r = x as Real by A21;

A23: r <= 1 by A21, BORSUK_1:40, XXREAL_1:1;

now :: thesis: ( ( 0 < r & r < 1 & y in Lower_Arc P ) or ( r = 0 & y in Lower_Arc P ) or ( r = 1 & y in Lower_Arc P ) )

hence
y in Lower_Arc P
; :: thesis: verumend;

case A24:
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 )

end;

( 0 < r & r < 1 & not f . r in Lower_Arc P ) ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

now :: thesis: ( ( ( 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 ) )end;

hence
( P1 = Upper_Arc P or P1 = Lower_Arc P )
; :: thesis: verumf . 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 ) ) ;

end;

f . r in Upper_Arc P or ex r being Real st

( 0 < r & r < 1 & not f . r in Upper_Arc P ) ) ;

case A25:
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 )

f . r in Upper_Arc P ; :: thesis: ( P1 = Upper_Arc P or P1 = Lower_Arc P )

P1 c= Upper_Arc P

end;proof

hence
( P1 = Upper_Arc P or P1 = Lower_Arc P )
by A2, A4, JORDAN6:46; :: thesis: verum
let y be object ; :: 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 object such that

A26: x in dom f and

A27: y = f . x by A18, FUNCT_1:def 3;

reconsider r = x as Real by A26;

A28: r <= 1 by A26, BORSUK_1:40, XXREAL_1:1;

end;assume y in P1 ; :: thesis: y in Upper_Arc P

then consider x being object such that

A26: x in dom f and

A27: y = f . x by A18, FUNCT_1:def 3;

reconsider r = x as Real by A26;

A28: r <= 1 by A26, BORSUK_1:40, XXREAL_1:1;

now :: thesis: ( ( 0 < r & r < 1 & y in Upper_Arc P ) or ( r = 0 & y in Upper_Arc P ) or ( r = 1 & y in Upper_Arc P ) )

hence
y in Upper_Arc P
; :: thesis: verumend;

case
ex r being Real st

( 0 < r & r < 1 & not f . r in Upper_Arc P ) ; :: thesis: contradiction

( 0 < r & r < 1 & not f . r in Upper_Arc P ) ; :: thesis: contradiction

then 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;

end;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 :: thesis: ( ( r1 <= r2 & contradiction ) or ( r1 > r2 & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( r1 <= r2 or r1 > r2 )
;

end;

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

end;

now :: thesis: ( ( r1 = r2 & contradiction ) or ( r1 < r2 & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( r1 = r2 or r1 < r2 )
by A38, XXREAL_0:1;

end;

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

reconsider 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;

end;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 :: thesis: ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )

hence
contradiction
; :: thesis: verumend;

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

reconsider 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;

end;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 :: thesis: ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )

hence
contradiction
; :: thesis: verumend;