let P, P1 be non empty compact Subset of (); :: 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 ;
A5: the carrier of (() | P) = [#] (() | P)
.= P by PRE_TOPC:def 5 ;
then reconsider U2 = Upper_Arc P as Subset of (() | P) by ;
reconsider U3 = Lower_Arc P as Subset of (() | P) by ;
A6: Lower_Arc P is_an_arc_of E-max P, W-min P by ;
U2 = () /\ P by ;
then A7: U2 is closed by ;
A8: (Upper_Arc P) \/ () = P by ;
U3 = () /\ P by ;
then A9: U3 is closed by ;
A10: (Upper_Arc P) /\ () = {(),()} by ;
then A11: E-max P in () /\ () by TARSKI:def 2;
A12: W-min P in () /\ () by ;
consider f being Function of I[01],(() | P1) such that
A13: f is being_homeomorphism and
A14: f . 0 = W-min P and
A15: f . 1 = E-max P by ;
A16: f is one-to-one by ;
A17: dom f = [#] I[01] by ;
A18: rng f = [#] (() | P1) by
.= P1 by PRE_TOPC:def 5 ;
A19: f is continuous by ;
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:
then consider x being object such that
A21: x in dom f and
A22: y = f . x by ;
reconsider r = x as Real by A21;
A23: r <= 1 by ;
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 ) )
per cases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by ;
end;
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:
then consider x being object such that
A26: x in dom f and
A27: y = f . x by ;
reconsider r = x as Real by A26;
A28: r <= 1 by ;
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 ) )
per cases ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by ;
end;
end;
hence y in Upper_Arc P ; :: thesis: verum
end;
hence ( P1 = Upper_Arc P or P1 = Lower_Arc P ) by ; :: 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 ;
then f . r2 in rng f by ;
then A32: f . r2 in Lower_Arc P by ;
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 ;
then A36: f . r1 in rng f by ;
then A37: f . r1 in Upper_Arc P by ;
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 ;
case A39: r1 < r2 ; :: thesis: contradiction
reconsider Q = P as non empty Subset of () by TOPREAL3:8;
A40: the carrier of (() | P1) = [#] (() | P1)
.= P1 by PRE_TOPC:def 5 ;
the carrier of (() | P) = [#] (() | P)
.= P by PRE_TOPC:def 5 ;
then rng f c= the carrier of (() | P) by ;
then reconsider g = f as Function of I[01],(() | P) by ;
P = P1 \/ P by ;
then A41: (TOP-REAL 2) | P1 is SubSpace of () | P by TOPMETR:4;
( U2 \/ U3 = the carrier of (() | Q) & () | P = TopSpaceMetr (() | Q) ) by ;
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 ;
then A45: r0 in dom f by ;
A46: 1 in dom f by ;
A47: 0 in dom f by ;
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 () by TOPREAL3:8;
A49: the carrier of (() | P1) = [#] (() | P1)
.= P1 by PRE_TOPC:def 5 ;
the carrier of (() | P) = [#] (() | P)
.= P by PRE_TOPC:def 5 ;
then rng f c= the carrier of (() | P) by ;
then reconsider g = f as Function of I[01],(() | P) by ;
P = P1 \/ P by ;
then A50: (TOP-REAL 2) | P1 is SubSpace of () | P by TOPMETR:4;
( U2 \/ U3 = the carrier of (() | Q) & () | P = TopSpaceMetr (() | Q) ) by ;
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 ;
then A54: r0 in dom f by ;
A55: 1 in dom f by ;
A56: 0 in dom f by ;
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