let P be non empty Subset of (TOP-REAL 2); :: thesis:
let p1, p2, p be Point of (TOP-REAL 2); :: thesis:
let e be Real; :: thesis:
assume that
A1: P is_an_arc_of p1,p2 and
A2: p2 `1 > e and
A3: p in P and
A4: p `1 = e ; :: thesis:

reconsider pr1a = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider pro1 = pr1a | P as Function of ((TOP-REAL 2) | P),R^1 by PRE_TOPC:9;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A5: f is being_homeomorphism and
A6: f . 0 = p1 and
A7: f . 1 = p2 by A1, TOPREAL1:def 1;
A8: f is continuous by A5, TOPS_2:def 5;
A9: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5;
then p in rng f by A3, PRE_TOPC:def 5;
then consider xs being set such that
A10: xs in dom f and
A11: p = f . xs by FUNCT_1:def 3;
A12: dom f = [#] I[01] by A5, TOPS_2:def 5;
then reconsider s2 = xs as Real by A10, BORSUK_1:40;
A13: s2 <= 1 by A10, BORSUK_1:40, XXREAL_1:1;
for q being Point of (TOP-REAL 2) st q = f . 1 holds
q `1 <> e by A2, A7;
then A14: 1 in { s where s is Real : ( 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } by A13;
{ s where s is Real : ( 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } c= REAL

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Real : ( 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } ; :: thesis:
then ex s being Real st
( s = x & 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) ;
hence x in REAL ; :: thesis:

end;

then reconsider R = { s where s is Real : ( 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } as non empty Subset of REAL by A14;
reconsider s0 = lower_bound R as Real ;
A15: for s being real number st s in R holds
s > s2

proof

let s be real number ; :: thesis:
assume s in R ; :: thesis:
then A16: ex s3 being Real st
( s3 = s & 1 >= s3 & s3 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s3 holds
q `1 <> e ) ) ;
then s <> s2 by A4, A11;
hence s > s2 by A16, XXREAL_0:1; :: thesis:

end;

then for s being real number st s in R holds
s >= s2 ;
then A17: s0 >= s2 by SEQ_4:43;
for p7 being Point of ((TOP-REAL 2) | P) holds pro1 . p7 = proj1 . p7

proof

let p7 be Point of ((TOP-REAL 2) | P); :: thesis:
the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:8;
hence pro1 . p7 = proj1 . p7 by FUNCT_1:49; :: thesis:

end;

then A18: pro1 is continuous by JGRAPH_2:29;
reconsider h = pro1 * f as Function of I[01],R^1 ;
A19: dom h = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
for s being ext-real number st s in R holds
s >= s2 by A15;
then s2 is LowerBound of R by XXREAL_2:def 2;
then A20: R is bounded_below by XXREAL_2:def 9;
A21: 0 <= s2 by A10, BORSUK_1:40, XXREAL_1:1;
R c= [.0,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in R ; :: thesis:
then ex s being Real st
( s = x & 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) ;
hence x in [.0,1.] by A21, XXREAL_1:1; :: thesis:

end;

then A22: 1 >= s0 by A14, BORSUK_1:40, BORSUK_4:26;
then s0 in dom f by A12, A21, A17, BORSUK_1:40, XXREAL_1:1;
then f . s0 in rng f by FUNCT_1:def 3;
then f . s0 in P by A9, PRE_TOPC:def 5;
then reconsider p9 = f . s0 as Point of (TOP-REAL 2) ;
A23: LE p,p9,P,p1,p2 by A1, A5, A6, A7, A11, A21, A13, A22, A17, JORDAN5C:8;
A24: rng f = P by A9, PRE_TOPC:def 5;
A25: for p8 being Point of (TOP-REAL 2) st LE p8,p9,P,p1,p2 & LE p,p8,P,p1,p2 holds
p8 `1 = e

proof

let p8 be Point of (TOP-REAL 2); :: thesis:
assume that
A26: LE p8,p9,P,p1,p2 and
A27: LE p,p8,P,p1,p2 ; :: thesis:
A28: p8 in P by A26, JORDAN5C:def 3;
then consider x8 being set such that
A29: x8 in dom f and
A30: p8 = f . x8 by A24, FUNCT_1:def 3;
reconsider s8 = x8 as Real by A12, A29, BORSUK_1:40;
A31: s8 <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
0 <= s8 by A29, BORSUK_1:40, XXREAL_1:1;
then A32: s8 >= s2 by A5, A6, A7, A11, A13, A27, A30, A31, JORDAN5C:def 3;
A33: s0 >= s8 by A5, A6, A7, A21, A22, A17, A26, A30, A31, JORDAN5C:def 3;

now

reconsider s8n = s8 as Point of RealSpace by METRIC_1:def 13;
reconsider s8m = s8 as Point of (Closed-Interval-MSpace (0,1)) by A29, BORSUK_1:40, TOPMETR:10;
reconsider ee = (abs ((p8 `1) - e)) / 2 as Real ;
reconsider w = p8 `1 as Element of RealSpace by METRIC_1:def 13;
reconsider B = Ball (w,ee) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
A34: B = { s7 where s7 is Real : ( (p8 `1) - ee < s7 & s7 < (p8 `1) + ee ) } by JORDAN2B:17
.= ].((p8 `1) - ee),((p8 `1) + ee).[ by RCOMP_1:def 2 ;
assume A35: p8 `1 <> e ; :: thesis:
then (p8 `1) - e <> 0 ;
then abs ((p8 `1) - e) > 0 by COMPLEX1:47;
then A36: w in Ball (w,ee) by GOBOARD6:1, XREAL_1:139;
A37: ( h " B is open & I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) ) by A8, A18, TOPMETR:20, TOPMETR:def 6, TOPMETR:def 7, UNIFORM1:2;
h . s8 = pro1 . (f . s8) by A19, A29, BORSUK_1:40, FUNCT_1:12
.= proj1 . p8 by A28, A30, FUNCT_1:49
.= p8 `1 by PSCOMP_1:def 5 ;
then s8 in h " B by A19, A29, A36, BORSUK_1:40, FUNCT_1:def 7;
then consider r0 being real number such that
A38: r0 > 0 and
A39: Ball (s8m,r0) c= h " B by A37, TOPMETR:15;
reconsider r0 = r0 as Real by XREAL_0:def 1;
reconsider r01 = min ((s8 - s2),r0) as Real ;
( the carrier of (Closed-Interval-MSpace (0,1)) = [.0,1.] & Ball (s8n,r01) = ].(s8 - r01),(s8 + r01).[ ) by FRECHET:7, TOPMETR:10;
then A40: Ball (s8m,r01) = ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] by TOPMETR:9;
s8 > s2 by A4, A11, A30, A32, A35, XXREAL_0:1;
then s8 - s2 > 0 by XREAL_1:50;
then A41: r01 > 0 by A38, XXREAL_0:21;
then A42: (r01 - (r01 / 2)) + (r01 / 2) > 0 + (r01 / 2) by XREAL_1:6;
then A43: s8 - r01 < s8 - (r01 / 2) by XREAL_1:10;
A44: r01 / 2 > 0 by A41, XREAL_1:139;
then A45: s8 + (- (r01 / 2)) < s8 + (r01 / 2) by XREAL_1:8;
s8 + (r01 / 2) < s8 + r01 by A42, XREAL_1:8;
then s8 - (r01 / 2) < s8 + r01 by A45, XXREAL_0:2;
then A46: s8 - (r01 / 2) in ].(s8 - r01),(s8 + r01).[ by A43, XXREAL_1:4;
A47: s8 - (r01 / 2) > s8 - r01 by A42, XREAL_1:10;
Ball (s8m,r01) c= Ball (s8m,r0) by PCOMPS_1:1, XXREAL_0:17;
then A48: ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] c= h " B by A39, A40, XBOOLE_1:1;
reconsider s70 = s8 - (r01 / 2) as Real ;
s8 - s2 >= r01 by XXREAL_0:17;
then - (s8 - s2) <= - r01 by XREAL_1:24;
then A49: (s2 - s8) + s8 <= (- r01) + s8 by XREAL_1:7;
- (- (r01 / 2)) > 0 by A41, XREAL_1:139;
then - (r01 / 2) < 0 ;
then A50: s8 + 0 > s8 + (- (r01 / 2)) by XREAL_1:8;
then A51: 1 >= s70 by A31, XXREAL_0:2;
1 - 0 > s8 - (r01 / 2) by A31, A44, XREAL_1:15;
then s8 - (r01 / 2) in [.0,1.] by A21, A49, A47, XXREAL_1:1;
then A52: s8 - (r01 / 2) in ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] by A46, XBOOLE_0:def 4;
then A53: h . (s8 - (r01 / 2)) in B by A48, FUNCT_1:def 7;
A54: s8 - (r01 / 2) in dom h by A48, A52, FUNCT_1:def 7;
A55: for p7 being Point of (TOP-REAL 2) st p7 = f . s70 holds
p7 `1 <> e

proof

let p7 be Point of (TOP-REAL 2); :: thesis:
assume A56: p7 = f . s70 ; :: thesis:
s70 in [.0,1.] by A21, A49, A43, A51, XXREAL_1:1;
then A57: p7 in rng f by A12, A56, BORSUK_1:40, FUNCT_1:def 3;
A58: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5
.= P by PRE_TOPC:def 5 ;
A59: h . s70 = pro1 . (f . s70) by A54, FUNCT_1:12
.= pr1a . p7 by A56, A57, A58, FUNCT_1:49
.= p7 `1 by PSCOMP_1:def 5 ;
then A60: p7 `1 < (p8 `1) + ee by A34, A53, XXREAL_1:4;
A61: (p8 `1) - ee < p7 `1 by A34, A53, A59, XXREAL_1:4;

now

assume A62: p7 `1 = e ; :: thesis:

now

per cases ) - e >= 0 or (p8 `1) - e < 0 ) ;

case A63: (p8 `1) - e >= 0 ; :: thesis:

then (p8 `1) - (((p8 `1) - e) / 2) < e by A61, A62, ABSVALUE:def 1;
then ((p8 `1) / 2) + (e / 2) < (e / 2) + (e / 2) ;
then (p8 `1) / 2 < e / 2 by XREAL_1:7;
then A64: ((p8 `1) / 2) - (e / 2) < (e / 2) - (e / 2) by XREAL_1:14;
((p8 `1) - e) / 2 >= 0 / 2 by A63;
hence contradiction by A64; :: thesis:

end;

case A65: (p8 `1) - e < 0 ; :: thesis:

then e < (p8 `1) + ((- ((p8 `1) - e)) / 2) by A60, A62, ABSVALUE:def 1;
then ((p8 `1) / 2) + (e / 2) > (e / 2) + (e / 2) ;
then (p8 `1) / 2 > e / 2 by XREAL_1:7;
then A66: ((p8 `1) / 2) - (e / 2) > (e / 2) - (e / 2) by XREAL_1:14;
((p8 `1) - e) / 2 <= 0 / 2 by A65;
hence contradiction by A66; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence p7 `1 <> e ; :: thesis:

end;

s70 >= s2 by A49, A43, XXREAL_0:2;
then consider s7 being Real such that
A67: s8 > s7 and
A68: ( 1 >= s7 & s7 >= s2 & ( for p7 being Point of (TOP-REAL 2) st p7 = f . s7 holds
p7 `1 <> e ) ) by A50, A51, A55;
s7 in R by A68;
then s7 >= s0 by A20, SEQ_4:def 2;
hence contradiction by A33, A67, XXREAL_0:2; :: thesis:

end;

hence p8 `1 = e ; :: thesis:

end;

assume not p is_OSout P,p1,p2,e ; :: thesis:
then consider p4 being Point of (TOP-REAL 2) such that
A69: LE p9,p4,P,p1,p2 and
A70: p4 <> p9 and
A71: ( for p5 being Point of (TOP-REAL 2) st LE p5,p4,P,p1,p2 & LE p9,p5,P,p1,p2 holds
p5 `1 <= e or for p6 being Point of (TOP-REAL 2) st LE p6,p4,P,p1,p2 & LE p9,p6,P,p1,p2 holds
p6 `1 >= e ) by A1, A3, A4, A23, A25, Def6;
A72: p9 in P by A69, JORDAN5C:def 3;

now

per cases by A71;

case A73: for p5 being Point of (TOP-REAL 2) st LE p5,p4,P,p1,p2 & LE p9,p5,P,p1,p2 holds
p5 `1 <= e ; :: thesis:

A74: now

p4 in P by A69, JORDAN5C:def 3;
then p4 in rng f by A9, PRE_TOPC:def 5;
then consider xs4 being set such that
A75: xs4 in dom f and
A76: p4 = f . xs4 by FUNCT_1:def 3;
reconsider s4 = xs4 as Real by A12, A75, BORSUK_1:40;
A77: s4 <= 1 by A75, BORSUK_1:40, XXREAL_1:1;
assume A78: for p51 being Point of (TOP-REAL 2) holds
( not LE p51,p4,P,p1,p2 or not LE p9,p51,P,p1,p2 or not p51 `1 < e ) ; :: thesis:
A79: for p51 being Point of (TOP-REAL 2) st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 holds
p51 `1 = e

proof

let p51 be Point of (TOP-REAL 2); :: thesis:
assume ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 ) ; :: thesis:
then ( p51 `1 >= e & p51 `1 <= e ) by A73, A78;
hence p51 `1 = e by XXREAL_0:1; :: thesis:

end;

A80: now

assume s4 > s0 ; :: thesis:
then - (- (s4 - s0)) > 0 by XREAL_1:50;
then - (s4 - s0) < 0 ;
then A81: (s0 - s4) / 2 < 0 by XREAL_1:141;
then - ((s0 - s4) / 2) > 0 by XREAL_1:58;
then consider r being real number such that
A82: r in R and
A83: r < s0 + (- ((s0 - s4) / 2)) by A20, SEQ_4:def 2;
reconsider rss = r as Real by XREAL_0:def 1;
A84: ex s7 being Real st
( s7 = r & 1 >= s7 & s7 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A82;
then r in [.0,1.] by A21, XXREAL_1:1;
then f . rss in rng f by A12, BORSUK_1:40, FUNCT_1:def 3;
then f . rss in P by A9, PRE_TOPC:def 5;
then reconsider pss = f . rss as Point of (TOP-REAL 2) ;
s4 + 0 > s4 + ((s0 - s4) / 2) by A81, XREAL_1:8;
then A85: s4 > r by A83, XXREAL_0:2;
then A86: 1 > r by A77, XXREAL_0:2;
A87: r >= s0 by A20, A82, SEQ_4:def 2;
then A88: LE p9,pss,P,p1,p2 by A1, A5, A6, A7, A21, A22, A17, A86, JORDAN5C:8;
LE pss,p4,P,p1,p2 by A1, A5, A6, A7, A21, A17, A76, A77, A87, A85, A86, JORDAN5C:8;
then pss `1 = e by A79, A88;
hence contradiction by A84; :: thesis:

end;

0 <= s4 by A75, BORSUK_1:40, XXREAL_1:1;
then s4 >= s0 by A5, A6, A7, A22, A69, A76, A77, JORDAN5C:def 3;
hence contradiction by A70, A76, A80, XXREAL_0:1; :: thesis:

end;

now

assume ex p51 being Point of (TOP-REAL 2) st
( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51 `1 < e ) ; :: thesis:
then consider p51 being Point of (TOP-REAL 2) such that
A89: LE p51,p4,P,p1,p2 and
A90: LE p9,p51,P,p1,p2 and
A91: p51 `1 < e ;
A92: for p5 being Point of (TOP-REAL 2) st LE p5,p51,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 <= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis:
assume that
A93: LE p5,p51,P,p1,p2 and
A94: LE p,p5,P,p1,p2 ; :: thesis:
A95: LE p5,p4,P,p1,p2 by A89, A93, JORDAN5C:13;
A96: p5 in P by A93, JORDAN5C:def 3;
then A97: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;

now

per cases by A1, A72, A96, A97, JORDAN5C:14;

case LE p5,p9,P,p1,p2 ; :: thesis:

hence p5 `1 <= e by A25, A94; :: thesis:

end;

case LE p9,p5,P,p1,p2 ; :: thesis:

hence p5 `1 <= e by A73, A95; :: thesis:

end;

hence p5 `1 <= e ; :: thesis:

end;

LE p,p51,P,p1,p2 by A23, A90, JORDAN5C:13;
hence p is_Lout P,p1,p2,e by A1, A3, A4, A91, A92, Def3; :: thesis:

end;

hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A74; :: thesis:

end;

case A98: for p6 being Point of (TOP-REAL 2) st LE p6,p4,P,p1,p2 & LE p9,p6,P,p1,p2 holds
p6 `1 >= e ; :: thesis:

A99: now

p4 in P by A69, JORDAN5C:def 3;
then p4 in rng f by A9, PRE_TOPC:def 5;
then consider xs4 being set such that
A100: xs4 in dom f and
A101: p4 = f . xs4 by FUNCT_1:def 3;
reconsider s4 = xs4 as Real by A12, A100, BORSUK_1:40;
A102: s4 <= 1 by A100, BORSUK_1:40, XXREAL_1:1;
assume A103: for p51 being Point of (TOP-REAL 2) holds
( not LE p51,p4,P,p1,p2 or not LE p9,p51,P,p1,p2 or not p51 `1 > e ) ; :: thesis:
A104: for p51 being Point of (TOP-REAL 2) st LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 holds
p51 `1 = e

proof

let p51 be Point of (TOP-REAL 2); :: thesis:
assume ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 ) ; :: thesis:
then ( p51 `1 <= e & p51 `1 >= e ) by A98, A103;
hence p51 `1 = e by XXREAL_0:1; :: thesis:

end;

A105: now

assume s4 > s0 ; :: thesis:
then - (- (s4 - s0)) > 0 by XREAL_1:50;
then - (s4 - s0) < 0 ;
then A106: (s0 - s4) / 2 < 0 by XREAL_1:141;
then - ((s0 - s4) / 2) > 0 by XREAL_1:58;
then consider r being real number such that
A107: r in R and
A108: r < s0 + (- ((s0 - s4) / 2)) by A20, SEQ_4:def 2;
reconsider rss = r as Real by XREAL_0:def 1;
A109: ex s7 being Real st
( s7 = r & 1 >= s7 & s7 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A107;
then r in [.0,1.] by A21, XXREAL_1:1;
then f . rss in rng f by A12, BORSUK_1:40, FUNCT_1:def 3;
then f . rss in P by A9, PRE_TOPC:def 5;
then reconsider pss = f . rss as Point of (TOP-REAL 2) ;
s4 + 0 > s4 + ((s0 - s4) / 2) by A106, XREAL_1:8;
then A110: s4 > r by A108, XXREAL_0:2;
then A111: 1 > r by A102, XXREAL_0:2;
A112: r >= s0 by A20, A107, SEQ_4:def 2;
then A113: LE p9,pss,P,p1,p2 by A1, A5, A6, A7, A21, A22, A17, A111, JORDAN5C:8;
LE pss,p4,P,p1,p2 by A1, A5, A6, A7, A21, A17, A101, A102, A112, A110, A111, JORDAN5C:8;
then pss `1 = e by A104, A113;
hence contradiction by A109; :: thesis:

end;

0 <= s4 by A100, BORSUK_1:40, XXREAL_1:1;
then s4 >= s0 by A5, A6, A7, A22, A69, A101, A102, JORDAN5C:def 3;
hence contradiction by A70, A101, A105, XXREAL_0:1; :: thesis:

end;

now

assume ex p51 being Point of (TOP-REAL 2) st
( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51 `1 > e ) ; :: thesis:
then consider p51 being Point of (TOP-REAL 2) such that
A114: LE p51,p4,P,p1,p2 and
A115: LE p9,p51,P,p1,p2 and
A116: p51 `1 > e ;
A117: for p5 being Point of (TOP-REAL 2) st LE p5,p51,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 >= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis:
assume that
A118: LE p5,p51,P,p1,p2 and
A119: LE p,p5,P,p1,p2 ; :: thesis:
A120: LE p5,p4,P,p1,p2 by A114, A118, JORDAN5C:13;
A121: p5 in P by A118, JORDAN5C:def 3;
then A122: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;

now

per cases by A1, A72, A121, A122, JORDAN5C:14;

case LE p9,p5,P,p1,p2 ; :: thesis:

hence p5 `1 >= e by A98, A120; :: thesis:

end;

case LE p5,p9,P,p1,p2 ; :: thesis:

hence p5 `1 >= e by A25, A119; :: thesis:

end;

hence p5 `1 >= e ; :: thesis:

end;

LE p,p51,P,p1,p2 by A23, A115, JORDAN5C:13;
hence p is_Rout P,p1,p2,e by A1, A3, A4, A116, A117, Def4; :: thesis:

end;

hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A99; :: thesis:

end;

hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ; :: thesis:

end;

hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e or p is_OSout P,p1,p2,e ) ; :: thesis: