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 A1: ( P is_an_arc_of p1,p2 & p1 `1 < e & p2 `1 > e & p in P & p `1 = e ) ; :: thesis:

now

assume A2: not p is_OSout P,p1,p2,e ; :: thesis:
LE p1,p,P,p1,p2 by A1, JORDAN5C:10;
then A3: ( p1 in P & p in P & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by JORDAN5C:def 3;
consider f being Function of I[01] ,((TOP-REAL 2) | P) such that
A4: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 2;
A5: f is continuous by A4, TOPS_2:def 5;
A6: ( dom f = [#] I[01] & rng f = [#] ((TOP-REAL 2) | P) ) by A4, TOPS_2:def 5;
then A7: rng f = P by PRE_TOPC:def 10;
p in rng f by A3, A6, PRE_TOPC:def 10;
then consider xs being set such that
A8: ( xs in dom f & p = f . xs ) by FUNCT_1:def 5;
reconsider s2 = xs as Real by A6, A8, BORSUK_1:83;
A9: ( 0 <= s2 & s2 <= 1 ) by A8, BORSUK_1:83, XXREAL_1:1;
reconsider pr1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider pro1 = pr1 | P as Function of ((TOP-REAL 2) | P),R^1 by PRE_TOPC:30;
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:29;
hence pro1 . p7 = proj1 . p7 by FUNCT_1:72; :: thesis:

end;

then A10: pro1 is continuous by JGRAPH_2:39;
reconsider h = pro1 * f as Function of I[01] ,R^1 ;
A11: h is continuous by A5, A10;
A12: dom h = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
for q being Point of (TOP-REAL 2) st q = f . 1 holds
q `1 <> e by A1, A4;
then A13: 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 A9;
{ 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

proof

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 consider s being Real such that
A14: ( s = x & 1 >= s & s >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) ;
thus x in REAL by A14; :: 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 A13;
reconsider s0 = lower_bound R as Real ;
R c= [.0 ,1.]

proof

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

end;

then A16: 1 >= s0 by A13, BORSUK_1:83, BORSUK_4:51;
A17: 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 consider s3 being Real such that
A18: ( s3 = s & 1 >= s3 & s3 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s3 holds
q `1 <> e ) ) ;
s <> s2 by A1, A8, A18;
hence s > s2 by A18, XXREAL_0:1; :: thesis:

end;

then for s being real number st s in R holds
s >= s2 ;
then A19: s0 >= s2 by SEQ_4:60;
then s0 in dom f by A6, A9, A16, BORSUK_1:83, XXREAL_1:1;
then f . s0 in rng f by FUNCT_1:def 5;
then f . s0 in P by A6, PRE_TOPC:def 10;
then reconsider p9 = f . s0 as Point of (TOP-REAL 2) ;
for s being real number st s in R holds
s >= s2 by A17;
then A20: R is bounded_below by SEQ_4:def 2;
A21: LE p,p9,P,p1,p2 by A1, A4, A8, A9, A16, A19, JORDAN5C:8;
A22: 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 A23: ( LE p8,p9,P,p1,p2 & LE p,p8,P,p1,p2 ) ; :: thesis:
then A24: p8 in P by JORDAN5C:def 3;
then consider x8 being set such that
A25: ( x8 in dom f & p8 = f . x8 ) by A7, FUNCT_1:def 5;
reconsider s8 = x8 as Real by A6, A25, BORSUK_1:83;
A26: ( 0 <= s8 & s8 <= 1 & f . s8 = p8 ) by A25, BORSUK_1:83, XXREAL_1:1;
then A27: s0 >= s8 by A4, A9, A16, A19, A23, JORDAN5C:def 3;
A28: s8 >= s2 by A4, A8, A9, A23, A26, JORDAN5C:def 3;

now

assume A29: p8 `1 <> e ; :: thesis:
then A30: s8 > s2 by A1, A8, A25, A28, XXREAL_0:1;
reconsider ee = (abs ((p8 `1 ) - e)) / 2 as Real ;
(p8 `1 ) - e <> 0 by A29;
then abs ((p8 `1 ) - e) > 0 by COMPLEX1:133;
then A31: ee > 0 by XREAL_1:141;
reconsider w = p8 `1 as Element of RealSpace by METRIC_1:def 14;
reconsider B = Ball w,ee as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
A32: w in Ball w,ee by A31, GOBOARD6:4;
A33: B = { s7 where s7 is Real : ( (p8 `1 ) - ee < s7 & s7 < (p8 `1 ) + ee ) } by A31, JORDAN2B:21
.= ].((p8 `1 ) - ee),((p8 `1 ) + ee).[ by RCOMP_1:def 2 ;
A34: h " B is open by A11, TOPMETR:def 7, UNIFORM1:3;
A35: the carrier of (Closed-Interval-MSpace 0 ,1) = [.0 ,1.] by TOPMETR:14;
reconsider s8m = s8 as Point of (Closed-Interval-MSpace 0 ,1) by A25, BORSUK_1:83, TOPMETR:14;
reconsider s8n = s8 as Point of RealSpace by METRIC_1:def 14;
A36: I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1) by TOPMETR:27, TOPMETR:def 8;
h . s8 = pro1 . (f . s8) by A12, A25, BORSUK_1:83, FUNCT_1:22
.= proj1 . p8 by A24, A25, FUNCT_1:72
.= p8 `1 by PSCOMP_1:def 28 ;
then s8 in h " B by A12, A25, A32, BORSUK_1:83, FUNCT_1:def 13;
then consider r0 being real number such that
A37: ( r0 > 0 & Ball s8m,r0 c= h " B ) by A34, A36, TOPMETR:22;
reconsider r0 = r0 as Real by XREAL_0:def 1;
reconsider r01 = min (s8 - s2),r0 as Real ;
s8 - s2 > 0 by A30, XREAL_1:52;
then A38: r01 > 0 by A37, XXREAL_0:21;
then Ball s8n,r01 = ].(s8 - r01),(s8 + r01).[ by FRECHET:7;
then A39: Ball s8m,r01 = ].(s8 - r01),(s8 + r01).[ /\ [.0 ,1.] by A35, TOPMETR:13;
s8 - s2 >= r01 by XXREAL_0:17;
then - (s8 - s2) <= - r01 by XREAL_1:26;
then A40: (s2 - s8) + s8 <= (- r01) + s8 by XREAL_1:9;
A41: Ball s8m,r01 c= Ball s8m,r0 by PCOMPS_1:1, XXREAL_0:17;
A42: ].(s8 - r01),(s8 + r01).[ /\ [.0 ,1.] c= h " B by A37, A39, A41, XBOOLE_1:1;
A43: (r01 - (r01 / 2)) + (r01 / 2) > 0 + (r01 / 2) by A38, XREAL_1:8;
then A44: s8 - (r01 / 2) > s8 - r01 by XREAL_1:12;
A45: r01 / 2 > 0 by A38, XREAL_1:141;
- (- (r01 / 2)) > 0 by A38, XREAL_1:141;
then A46: - (r01 / 2) < 0 ;
A47: s8 + (r01 / 2) < s8 + r01 by A43, XREAL_1:10;
s8 + (- (r01 / 2)) < s8 + (r01 / 2) by A45, XREAL_1:10;
then A48: ( s8 - r01 < s8 - (r01 / 2) & s8 - (r01 / 2) < s8 + r01 ) by A43, A47, XREAL_1:12, XXREAL_0:2;
then A49: s8 - (r01 / 2) in ].(s8 - r01),(s8 + r01).[ by XXREAL_1:4;
1 - 0 > s8 - (r01 / 2) by A26, A45, XREAL_1:17;
then s8 - (r01 / 2) in [.0 ,1.] by A9, A40, A44, XXREAL_1:1;
then s8 - (r01 / 2) in ].(s8 - r01),(s8 + r01).[ /\ [.0 ,1.] by A49, XBOOLE_0:def 4;
then A50: ( s8 - (r01 / 2) in dom h & h . (s8 - (r01 / 2)) in B ) by A42, FUNCT_1:def 13;
reconsider s70 = s8 - (r01 / 2) as Real ;
s8 + 0 > s8 + (- (r01 / 2)) by A46, XREAL_1:10;
then A51: ( s8 > s70 & 1 >= s70 & s70 >= s2 ) by A26, A40, A48, XXREAL_0:2;
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 A52: p7 = f . s70 ; :: thesis:
s70 in [.0 ,1.] by A9, A51, XXREAL_1:1;
then A53: p7 in rng f by A6, A52, BORSUK_1:83, FUNCT_1:def 5;
A54: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
h . s70 = pro1 . (f . s70) by A50, FUNCT_1:22
.= pr1 . p7 by A52, A53, A54, FUNCT_1:72
.= p7 `1 by PSCOMP_1:def 28 ;
then A55: ( (p8 `1 ) - ee < p7 `1 & p7 `1 < (p8 `1 ) + ee ) by A33, A50, XXREAL_1:4;

now

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

now

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

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

then ( (p8 `1 ) - (((p8 `1 ) - e) / 2) < e & e < (p8 `1 ) + (((p8 `1 ) - e) / 2) ) by A55, A56, ABSVALUE:def 1;
then ((p8 `1 ) / 2) + (e / 2) < (e / 2) + (e / 2) ;
then (p8 `1 ) / 2 < e / 2 by XREAL_1:9;
then A58: ((p8 `1 ) / 2) - (e / 2) < (e / 2) - (e / 2) by XREAL_1:16;
((p8 `1 ) - e) / 2 >= 0 / 2 by A57;
hence contradiction by A58; :: thesis:

end;

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

then ( (p8 `1 ) - ((- ((p8 `1 ) - e)) / 2) < e & e < (p8 `1 ) + ((- ((p8 `1 ) - e)) / 2) ) by A55, A56, ABSVALUE:def 1;
then ((p8 `1 ) / 2) + (e / 2) > (e / 2) + (e / 2) ;
then (p8 `1 ) / 2 > e / 2 by XREAL_1:9;
then A60: ((p8 `1 ) / 2) - (e / 2) > (e / 2) - (e / 2) by XREAL_1:16;
((p8 `1 ) - e) / 2 <= 0 / 2 by A59;
hence contradiction by A60; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

end;

then consider s7 being Real such that
A61: ( s8 > s7 & 1 >= s7 & s7 >= s2 & ( for p7 being Point of (TOP-REAL 2) st p7 = f . s7 holds
p7 `1 <> e ) ) by A51;
s7 in R by A61;
then s7 >= s0 by A20, SEQ_4:def 5;
hence contradiction by A27, A61, XXREAL_0:2; :: thesis:

end;

hence p8 `1 = e ; :: thesis:

end;

then consider p4 being Point of (TOP-REAL 2) such that
A62: ( LE p9,p4,P,p1,p2 & p4 <> p9 & ( 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, A2, A21, Def6;
A63: p9 in P by A62, JORDAN5C:def 3;

now

per cases by A62;

case A64: 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:

A65: 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
A66: ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51 `1 < e ) ;
A67: LE p,p51,P,p1,p2 by A21, A66, JORDAN5C:13;
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 A68: ( LE p5,p51,P,p1,p2 & LE p,p5,P,p1,p2 ) ; :: thesis:
then A69: LE p5,p4,P,p1,p2 by A66, JORDAN5C:13;
A70: p5 in P by A68, JORDAN5C:def 3;
then A71: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;

now

per cases by A1, A63, A70, A71, JORDAN5C:14;

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

hence p5 `1 <= e by A22, A68; :: thesis:

end;

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

hence p5 `1 <= e by A64, A69; :: thesis:

end;

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

end;

hence p is_Lout P,p1,p2,e by A1, A66, A67, Def3; :: thesis:

end;

now

assume A72: 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:
A73: 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 A74: ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 ) ; :: thesis:
then A75: p51 `1 >= e by A72;
p51 `1 <= e by A64, A74;
hence p51 `1 = e by A75, XXREAL_0:1; :: thesis:

end;

p4 in P by A62, JORDAN5C:def 3;
then p4 in rng f by A6, PRE_TOPC:def 10;
then consider xs4 being set such that
A76: ( xs4 in dom f & p4 = f . xs4 ) by FUNCT_1:def 5;
reconsider s4 = xs4 as Real by A6, A76, BORSUK_1:83;
A77: ( 0 <= s4 & s4 <= 1 ) by A76, BORSUK_1:83, XXREAL_1:1;
then A78: s4 >= s0 by A4, A16, A62, A76, JORDAN5C:def 3;

now

assume s4 > s0 ; :: thesis:
then - (- (s4 - s0)) > 0 by XREAL_1:52;
then - (s4 - s0) < 0 ;
then A79: (s0 - s4) / 2 < 0 by XREAL_1:143;
then A80: - ((s0 - s4) / 2) > 0 by XREAL_1:60;
A81: s4 + 0 > s4 + ((s0 - s4) / 2) by A79, XREAL_1:10;
consider r being real number such that
A82: ( r in R & r < s0 + (- ((s0 - s4) / 2)) ) by A20, A80, SEQ_4:def 5;
A83: r >= s0 by A20, A82, SEQ_4:def 5;
A84: s4 > r by A81, A82, XXREAL_0:2;
then A85: 1 > r by A77, XXREAL_0:2;
consider s7 being Real such that
A86: ( s7 = r & 1 >= s7 & s7 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A82;
A87: r in [.0 ,1.] by A9, A86, XXREAL_1:1;
reconsider rss = r as Real by XREAL_0:def 1;
f . rss in rng f by A6, A87, BORSUK_1:83, FUNCT_1:def 5;
then f . rss in P by A6, PRE_TOPC:def 10;
then reconsider pss = f . rss as Point of (TOP-REAL 2) ;
( LE pss,p4,P,p1,p2 & LE p9,pss,P,p1,p2 ) by A1, A4, A9, A16, A19, A76, A77, A83, A84, A85, JORDAN5C:8;
then pss `1 = e by A73;
hence contradiction by A86; :: thesis:

end;

hence contradiction by A62, A76, A78, XXREAL_0:1; :: thesis:

end;

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

end;

case A88: 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:

A89: 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
A90: ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 & p51 `1 > e ) ;
A91: LE p,p51,P,p1,p2 by A21, A90, JORDAN5C:13;
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 A92: ( LE p5,p51,P,p1,p2 & LE p,p5,P,p1,p2 ) ; :: thesis:
then A93: LE p5,p4,P,p1,p2 by A90, JORDAN5C:13;
A94: p5 in P by A92, JORDAN5C:def 3;
then A95: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;

now

per cases by A1, A63, A94, A95, JORDAN5C:14;

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

hence p5 `1 >= e by A88, A93; :: thesis:

end;

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

hence p5 `1 >= e by A22, A92; :: thesis:

end;

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

end;

hence p is_Rout P,p1,p2,e by A1, A90, A91, Def4; :: thesis:

end;

now

assume A96: 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:
A97: 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 A98: ( LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2 ) ; :: thesis:
then A99: p51 `1 <= e by A96;
p51 `1 >= e by A88, A98;
hence p51 `1 = e by A99, XXREAL_0:1; :: thesis:

end;

p4 in P by A62, JORDAN5C:def 3;
then p4 in rng f by A6, PRE_TOPC:def 10;
then consider xs4 being set such that
A100: ( xs4 in dom f & p4 = f . xs4 ) by FUNCT_1:def 5;
reconsider s4 = xs4 as Real by A6, A100, BORSUK_1:83;
A101: ( 0 <= s4 & s4 <= 1 ) by A100, BORSUK_1:83, XXREAL_1:1;
then A102: s4 >= s0 by A4, A16, A62, A100, JORDAN5C:def 3;

now

assume s4 > s0 ; :: thesis:
then - (- (s4 - s0)) > 0 by XREAL_1:52;
then - (s4 - s0) < 0 ;
then A103: (s0 - s4) / 2 < 0 by XREAL_1:143;
then A104: - ((s0 - s4) / 2) > 0 by XREAL_1:60;
A105: s4 + 0 > s4 + ((s0 - s4) / 2) by A103, XREAL_1:10;
consider r being real number such that
A106: ( r in R & r < s0 + (- ((s0 - s4) / 2)) ) by A20, A104, SEQ_4:def 5;
A107: r >= s0 by A20, A106, SEQ_4:def 5;
A108: s4 > r by A105, A106, XXREAL_0:2;
then A109: 1 > r by A101, XXREAL_0:2;
consider s7 being Real such that
A110: ( s7 = r & 1 >= s7 & s7 >= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A106;
A111: r in [.0 ,1.] by A9, A110, XXREAL_1:1;
reconsider rss = r as Real by XREAL_0:def 1;
f . rss in rng f by A6, A111, BORSUK_1:83, FUNCT_1:def 5;
then f . rss in P by A6, PRE_TOPC:def 10;
then reconsider pss = f . rss as Point of (TOP-REAL 2) ;
( LE pss,p4,P,p1,p2 & LE p9,pss,P,p1,p2 ) by A1, A4, A9, A16, A19, A100, A101, A107, A108, A109, JORDAN5C:8;
then pss `1 = e by A97;
hence contradiction by A110; :: thesis:

end;

hence contradiction by A62, A100, A102, XXREAL_0:1; :: thesis:

end;

hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A89; :: 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: