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;
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 ) ) )
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 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 )
P1 c= Lower_Arc P
proof
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;
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 ) )
end;
hence y in Lower_Arc P ; :: thesis: verum
end;
hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A2, A6, Th14; :: thesis: verum
end;
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 )
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 ) )
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 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 )
P1 c= Upper_Arc P
proof
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;
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 ) )
end;
hence y in Upper_Arc P ; :: thesis: verum
end;
hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by A2, A4, JORDAN6:46; :: 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
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 ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case A38: r1 <= r2 ; :: thesis: contradiction
now :: thesis: ( ( r1 = r2 & contradiction ) or ( r1 < r2 & contradiction ) )
per cases ( r1 = r2 or r1 < r2 ) by A38, XXREAL_0:1;
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;
now :: thesis: ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
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;
now :: thesis: ( ( g . r0 = W-min P & contradiction ) or ( g . r0 = E-max P & contradiction ) )
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