let P be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2, p being Point of (TOP-REAL 2)
for e being Real st P is_an_arc_of p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e & not p is_Rin P,p1,p2,e holds
p is_OSin P,p1,p2,e
let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for e being Real st P is_an_arc_of p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e & not p is_Rin P,p1,p2,e holds
p is_OSin P,p1,p2,e
let e be Real; :: thesis: ( P is_an_arc_of p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e & not p is_Rin P,p1,p2,e implies p is_OSin P,p1,p2,e )
assume that
A1: P is_an_arc_of p1,p2 and
A2: p1 `1 < e and
A3: p in P and
A4: p `1 = e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e or p is_OSin P,p1,p2,e )
now :: thesis: ( p is_OSin P,p1,p2,e or p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
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 object 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 Element of REAL by A10, BORSUK_1:40;
A13: 0 <= s2 by A10, BORSUK_1:40, XXREAL_1:1;
A14: 0 in REAL by XREAL_0:def 1;
for q being Point of (TOP-REAL 2) st q = f . 0 holds
q `1 <> e by A2, A6;
then A15: 0 in { s where s is Element of REAL : ( 0 <= s & s <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } by A13, A14;
{ s where s is Element of REAL : ( 0 <= 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of REAL : ( 0 <= s & s <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } or x in REAL )
assume x in { s where s is Element of REAL : ( 0 <= s & s <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) } ; :: thesis: x in REAL
then ex s being Element of REAL st
( s = x & 0 <= s & s <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ) ) ;
hence x in REAL ; :: thesis: verum
end;
then reconsider R = { s where s is Element of REAL : ( 0 <= 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 A15;
A16: s2 <= 1 by A10, BORSUK_1:40, XXREAL_1:1;
R c= [.0,1.]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in [.0,1.] )
assume x in R ; :: thesis: x in [.0,1.]
then consider s being Element of REAL such that
A17: ( s = x & 0 <= s ) and
A18: s <= s2 and
for q being Point of (TOP-REAL 2) st q = f . s holds
q `1 <> e ;
s <= 1 by A16, A18, XXREAL_0:2;
hence x in [.0,1.] by A17, XXREAL_1:1; :: thesis: verum
end;
then reconsider R99 = R as Subset of I[01] by BORSUK_1:40;
reconsider s0 = upper_bound R as Element of REAL by XREAL_0:def 1;
A19: for s being Real st s in R holds
s < s2
proof
let s be Real; :: thesis: ( s in R implies s < s2 )
assume s in R ; :: thesis: s < s2
then A20: ex s3 being Element of REAL st
( s3 = s & 0 <= 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 A20, XXREAL_0:1; :: thesis: verum
end;
then for s being Real st s in R holds
s <= s2 ;
then A21: s0 <= s2 by SEQ_4:45;
then A22: s0 <= 1 by A16, XXREAL_0:2;
R99 = R ;
then A23: 0 <= s0 by A15, BORSUK_4:26;
then s0 in dom f by A12, A22, 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) ;
A24: LE p9,p,P,p1,p2 by A1, A5, A6, A7, A11, A16, A23, A21, A22, JORDAN5C:8;
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: pro1 . p7 = proj1 . p7
the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:8;
hence pro1 . p7 = proj1 . p7 by FUNCT_1:49; :: thesis: verum
end;
then A25: pro1 is continuous by JGRAPH_2:29;
reconsider h = pro1 * f as Function of I[01],R^1 ;
A26: dom h = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
for s being ExtReal st s in R holds
s <= s2 by A19;
then s2 is UpperBound of R by XXREAL_2:def 1;
then A27: R is bounded_above by XXREAL_2:def 10;
A28: rng f = P by A9, PRE_TOPC:def 5;
A29: for p8 being Point of (TOP-REAL 2) st LE p9,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds
p8 `1 = e
proof
let p8 be Point of (TOP-REAL 2); :: thesis: ( LE p9,p8,P,p1,p2 & LE p8,p,P,p1,p2 implies p8 `1 = e )
assume that
A30: LE p9,p8,P,p1,p2 and
A31: LE p8,p,P,p1,p2 ; :: thesis: p8 `1 = e
A32: p8 in P by A30, JORDAN5C:def 3;
then consider x8 being object such that
A33: x8 in dom f and
A34: p8 = f . x8 by A28, FUNCT_1:def 3;
reconsider s8 = x8 as Element of REAL by A12, A33, BORSUK_1:40;
A35: s8 <= 1 by A33, BORSUK_1:40, XXREAL_1:1;
then A36: s8 <= s2 by A5, A6, A7, A11, A13, A16, A31, A34, JORDAN5C:def 3;
A37: 0 <= s8 by A33, BORSUK_1:40, XXREAL_1:1;
then A38: s0 <= s8 by A5, A6, A7, A22, A30, A34, A35, JORDAN5C:def 3;
now :: thesis: not p8 `1 <> e
reconsider s8n = s8 as Point of RealSpace by METRIC_1:def 13;
reconsider s8m = s8 as Point of (Closed-Interval-MSpace (0,1)) by A33, BORSUK_1:40, TOPMETR:10;
reconsider ee = |.((p8 `1) - e).| / 2 as Real ;
reconsider w = p8 `1 as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
reconsider B = Ball (w,ee) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
A39: 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 A40: p8 `1 <> e ; :: thesis: contradiction
then (p8 `1) - e <> 0 ;
then |.((p8 `1) - e).| > 0 by COMPLEX1:47;
then A41: w in Ball (w,ee) by GOBOARD6:1, XREAL_1:139;
A42: ( h " B is open & I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) ) by A8, A25, TOPMETR:20, TOPMETR:def 6, TOPMETR:def 7, UNIFORM1:2;
h . s8 = pro1 . (f . s8) by A26, A33, BORSUK_1:40, FUNCT_1:12
.= proj1 . p8 by A32, A34, FUNCT_1:49
.= p8 `1 by PSCOMP_1:def 5 ;
then s8 in h " B by A26, A33, A41, BORSUK_1:40, FUNCT_1:def 7;
then consider r0 being Real such that
A43: r0 > 0 and
A44: Ball (s8m,r0) c= h " B by A42, TOPMETR:15;
reconsider r0 = r0 as Real ;
reconsider r01 = min ((s2 - s8),r0) as Real ;
s8 < s2 by A4, A11, A34, A36, A40, XXREAL_0:1;
then s2 - s8 > 0 by XREAL_1:50;
then A45: r01 > 0 by A43, XXREAL_0:21;
then A46: (r01 - (r01 / 2)) + (r01 / 2) > 0 + (r01 / 2) by XREAL_1:6;
then A47: s8 + (r01 / 2) < s8 + r01 by XREAL_1:6;
reconsider s70 = s8 + (r01 / 2) 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 A48: Ball (s8m,r01) = ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] by TOPMETR:9;
s2 - s8 >= r01 by XXREAL_0:17;
then A49: (s2 - s8) + s8 >= r01 + s8 by XREAL_1:7;
then A50: s70 <= s2 by A47, XXREAL_0:2;
s8 + r01 <= 1 by A16, A49, XXREAL_0:2;
then s8 + (r01 / 2) < 1 by A47, XXREAL_0:2;
then A51: s8 + (r01 / 2) in [.0,1.] by A37, A45, XXREAL_1:1;
Ball (s8m,r01) c= Ball (s8m,r0) by PCOMPS_1:1, XXREAL_0:17;
then A52: ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] c= h " B by A44, A48;
s8 + 0 < s8 + ((r01 / 2) + r01) by A45, XREAL_1:6;
then (s8 - r01) + r01 < (s8 + (r01 / 2)) + r01 ;
then A53: s8 - r01 < s8 + (r01 / 2) by XREAL_1:6;
s8 + (r01 / 2) < s8 + r01 by A46, XREAL_1:6;
then s8 + (r01 / 2) in ].(s8 - r01),(s8 + r01).[ by A53, XXREAL_1:4;
then A54: s8 + (r01 / 2) in ].(s8 - r01),(s8 + r01).[ /\ [.0,1.] by A51, XBOOLE_0:def 4;
then A55: h . (s8 + (r01 / 2)) in B by A52, FUNCT_1:def 7;
A56: s8 + (r01 / 2) in dom h by A52, A54, FUNCT_1:def 7;
A57: 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: ( p7 = f . s70 implies p7 `1 <> e )
assume A58: p7 = f . s70 ; :: thesis: p7 `1 <> e
s70 <= 1 by A16, A50, XXREAL_0:2;
then s70 in [.0,1.] by A37, A45, XXREAL_1:1;
then A59: p7 in rng f by A12, A58, BORSUK_1:40, FUNCT_1:def 3;
A60: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5
.= P by PRE_TOPC:def 5 ;
A61: h . s70 = pro1 . (f . s70) by A56, FUNCT_1:12
.= pr1a . p7 by A58, A59, A60, FUNCT_1:49
.= p7 `1 by PSCOMP_1:def 5 ;
then A62: p7 `1 < (p8 `1) + ee by A39, A55, XXREAL_1:4;
A63: (p8 `1) - ee < p7 `1 by A39, A55, A61, XXREAL_1:4;
now :: thesis: not p7 `1 = e
assume A64: p7 `1 = e ; :: thesis: contradiction
now :: thesis: ( ( (p8 `1) - e >= 0 & contradiction ) or ( (p8 `1) - e < 0 & contradiction ) )
per cases ( (p8 `1) - e >= 0 or (p8 `1) - e < 0 ) ;
case A65: (p8 `1) - e >= 0 ; :: thesis: contradiction
then (p8 `1) - (((p8 `1) - e) / 2) < e by A63, A64, 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: verum
end;
case A67: (p8 `1) - e < 0 ; :: thesis: contradiction
then e < (p8 `1) + ((- ((p8 `1) - e)) / 2) by A62, A64, ABSVALUE:def 1;
then ((p8 `1) / 2) + (e / 2) > (e / 2) + (e / 2) ;
then (p8 `1) / 2 > e / 2 by XREAL_1:7;
then A68: ((p8 `1) / 2) - (e / 2) > (e / 2) - (e / 2) by XREAL_1:14;
((p8 `1) - e) / 2 <= 0 / 2 by A67;
hence contradiction by A68; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence p7 `1 <> e ; :: thesis: verum
end;
s8 < s70 by A45, XREAL_1:29, XREAL_1:139;
then consider s7 being Real such that
A69: s8 < s7 and
A70: ( 0 <= s7 & s7 <= s2 & ( for p7 being Point of (TOP-REAL 2) st p7 = f . s7 holds
p7 `1 <> e ) ) by A37, A50, A57;
reconsider s7 = s7 as Element of REAL by XREAL_0:def 1;
s7 in R by A70;
then s7 <= s0 by A27, SEQ_4:def 1;
hence contradiction by A38, A69, XXREAL_0:2; :: thesis: verum
end;
hence p8 `1 = e ; :: thesis: verum
end;
assume not p is_OSin P,p1,p2,e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
then consider p4 being Point of (TOP-REAL 2) such that
A71: LE p4,p9,P,p1,p2 and
A72: p4 <> p9 and
A73: ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p9,P,p1,p2 holds
p5 `1 <= e or for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p9,P,p1,p2 holds
p6 `1 >= e ) by A1, A3, A4, A24, A29;
A74: p9 in P by A71, JORDAN5C:def 3;
now :: thesis: ( ( ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p9,P,p1,p2 holds
p5 `1 <= e ) & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) or ( ( for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p9,P,p1,p2 holds
p6 `1 >= e ) & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) )
per cases ( for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p9,P,p1,p2 holds
p5 `1 <= e or for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p9,P,p1,p2 holds
p6 `1 >= e ) by A73;
case A75: for p5 being Point of (TOP-REAL 2) st LE p4,p5,P,p1,p2 & LE p5,p9,P,p1,p2 holds
p5 `1 <= e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
A76: now :: thesis: ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 < e )
p4 in P by A71, JORDAN5C:def 3;
then p4 in rng f by A9, PRE_TOPC:def 5;
then consider xs4 being object such that
A77: xs4 in dom f and
A78: p4 = f . xs4 by FUNCT_1:def 3;
reconsider s4 = xs4 as Real by A77;
A79: 0 <= s4 by A77, BORSUK_1:40, XXREAL_1:1;
A80: s4 <= 1 by A77, BORSUK_1:40, XXREAL_1:1;
assume A81: for p51 being Point of (TOP-REAL 2) holds
( not LE p4,p51,P,p1,p2 or not LE p51,p9,P,p1,p2 or not p51 `1 < e ) ; :: thesis: contradiction
A82: for p51 being Point of (TOP-REAL 2) st LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 holds
p51 `1 = e
proof
let p51 be Point of (TOP-REAL 2); :: thesis: ( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 implies p51 `1 = e )
assume ( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 ) ; :: thesis: p51 `1 = e
then ( p51 `1 >= e & p51 `1 <= e ) by A75, A81;
hence p51 `1 = e by XXREAL_0:1; :: thesis: verum
end;
A83: now :: thesis: not s4 < s0
assume s4 < s0 ; :: thesis: contradiction
then A84: s0 - s4 > 0 by XREAL_1:50;
then A85: s4 < s4 + ((s0 - s4) / 2) by XREAL_1:29, XREAL_1:139;
(s0 - s4) / 2 > 0 by A84, XREAL_1:139;
then consider r being Real such that
A86: r in R and
A87: s0 - ((s0 - s4) / 2) < r by A27, SEQ_4:def 1;
reconsider rss = r as Real ;
A88: ex s7 being Element of REAL st
( s7 = r & 0 <= s7 & s7 <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A86;
then A89: r <= 1 by A16, XXREAL_0:2;
then r in [.0,1.] by A79, A85, A87, 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 < r by A85, A87, XXREAL_0:2;
then A90: LE p4,pss,P,p1,p2 by A1, A5, A6, A7, A78, A79, A80, A89, JORDAN5C:8;
r <= s0 by A27, A86, SEQ_4:def 1;
then LE pss,p9,P,p1,p2 by A1, A5, A6, A7, A22, A79, A85, A87, A89, JORDAN5C:8;
then pss `1 = e by A82, A90;
hence contradiction by A88; :: thesis: verum
end;
s4 <= s0 by A5, A6, A7, A23, A22, A71, A78, A80, JORDAN5C:def 3;
hence contradiction by A72, A78, A83, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: ( ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 < e ) implies p is_Lin P,p1,p2,e )
assume ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 < e ) ; :: thesis: p is_Lin P,p1,p2,e
then consider p51 being Point of (TOP-REAL 2) such that
A91: LE p4,p51,P,p1,p2 and
A92: LE p51,p9,P,p1,p2 and
A93: p51 `1 < e ;
A94: for p5 being Point of (TOP-REAL 2) st LE p51,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds
p5 `1 <= e
proof
let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p51,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
assume that
A95: LE p51,p5,P,p1,p2 and
A96: LE p5,p,P,p1,p2 ; :: thesis: p5 `1 <= e
A97: LE p4,p5,P,p1,p2 by A91, A95, JORDAN5C:13;
A98: p5 in P by A95, JORDAN5C:def 3;
then A99: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;
now :: thesis: ( ( LE p5,p9,P,p1,p2 & p5 `1 <= e ) or ( LE p9,p5,P,p1,p2 & p5 `1 <= e ) )
per cases ( LE p5,p9,P,p1,p2 or LE p9,p5,P,p1,p2 ) by A1, A74, A98, A99, JORDAN5C:14;
case LE p5,p9,P,p1,p2 ; :: thesis: p5 `1 <= e
hence p5 `1 <= e by A75, A97; :: thesis: verum
end;
case LE p9,p5,P,p1,p2 ; :: thesis: p5 `1 <= e
hence p5 `1 <= e by A29, A96; :: thesis: verum
end;
end;
end;
hence p5 `1 <= e ; :: thesis: verum
end;
LE p51,p,P,p1,p2 by A24, A92, JORDAN5C:13;
hence p is_Lin P,p1,p2,e by A1, A3, A4, A93, A94; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A76; :: thesis: verum
end;
case A100: for p6 being Point of (TOP-REAL 2) st LE p4,p6,P,p1,p2 & LE p6,p9,P,p1,p2 holds
p6 `1 >= e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
A101: now :: thesis: ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 > e )
p4 in P by A71, JORDAN5C:def 3;
then p4 in rng f by A9, PRE_TOPC:def 5;
then consider xs4 being object such that
A102: xs4 in dom f and
A103: p4 = f . xs4 by FUNCT_1:def 3;
reconsider s4 = xs4 as Real by A102;
A104: 0 <= s4 by A102, BORSUK_1:40, XXREAL_1:1;
A105: s4 <= 1 by A102, BORSUK_1:40, XXREAL_1:1;
assume A106: for p51 being Point of (TOP-REAL 2) holds
( not LE p4,p51,P,p1,p2 or not LE p51,p9,P,p1,p2 or not p51 `1 > e ) ; :: thesis: contradiction
A107: for p51 being Point of (TOP-REAL 2) st LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 holds
p51 `1 = e
proof
let p51 be Point of (TOP-REAL 2); :: thesis: ( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 implies p51 `1 = e )
assume ( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 ) ; :: thesis: p51 `1 = e
then ( p51 `1 <= e & p51 `1 >= e ) by A100, A106;
hence p51 `1 = e by XXREAL_0:1; :: thesis: verum
end;
A108: now :: thesis: not s4 < s0
assume s4 < s0 ; :: thesis: contradiction
then A109: s0 - s4 > 0 by XREAL_1:50;
then A110: s4 < s4 + ((s0 - s4) / 2) by XREAL_1:29, XREAL_1:139;
(s0 - s4) / 2 > 0 by A109, XREAL_1:139;
then consider r being Real such that
A111: r in R and
A112: s0 - ((s0 - s4) / 2) < r by A27, SEQ_4:def 1;
reconsider rss = r as Real ;
A113: ex s7 being Element of REAL st
( s7 = r & 0 <= s7 & s7 <= s2 & ( for q being Point of (TOP-REAL 2) st q = f . s7 holds
q `1 <> e ) ) by A111;
then A114: r <= 1 by A16, XXREAL_0:2;
then r in [.0,1.] by A104, A110, A112, 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 < r by A110, A112, XXREAL_0:2;
then A115: LE p4,pss,P,p1,p2 by A1, A5, A6, A7, A103, A104, A105, A114, JORDAN5C:8;
r <= s0 by A27, A111, SEQ_4:def 1;
then LE pss,p9,P,p1,p2 by A1, A5, A6, A7, A22, A104, A110, A112, A114, JORDAN5C:8;
then pss `1 = e by A107, A115;
hence contradiction by A113; :: thesis: verum
end;
s4 <= s0 by A5, A6, A7, A23, A22, A71, A103, A105, JORDAN5C:def 3;
hence contradiction by A72, A103, A108, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: ( ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 > e ) implies p is_Rin P,p1,p2,e )
assume ex p51 being Point of (TOP-REAL 2) st
( LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2 & p51 `1 > e ) ; :: thesis: p is_Rin P,p1,p2,e
then consider p51 being Point of (TOP-REAL 2) such that
A116: LE p4,p51,P,p1,p2 and
A117: LE p51,p9,P,p1,p2 and
A118: p51 `1 > e ;
A119: for p5 being Point of (TOP-REAL 2) st LE p51,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds
p5 `1 >= e
proof
let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p51,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
assume that
A120: LE p51,p5,P,p1,p2 and
A121: LE p5,p,P,p1,p2 ; :: thesis: p5 `1 >= e
A122: LE p4,p5,P,p1,p2 by A116, A120, JORDAN5C:13;
A123: p5 in P by A120, JORDAN5C:def 3;
then A124: ( p5 = p9 implies LE p9,p5,P,p1,p2 ) by JORDAN5C:9;
now :: thesis: ( ( LE p5,p9,P,p1,p2 & p5 `1 >= e ) or ( LE p9,p5,P,p1,p2 & p5 `1 >= e ) )
per cases ( LE p5,p9,P,p1,p2 or LE p9,p5,P,p1,p2 ) by A1, A74, A123, A124, JORDAN5C:14;
case LE p5,p9,P,p1,p2 ; :: thesis: p5 `1 >= e
hence p5 `1 >= e by A100, A122; :: thesis: verum
end;
case LE p9,p5,P,p1,p2 ; :: thesis: p5 `1 >= e
hence p5 `1 >= e by A29, A121; :: thesis: verum
end;
end;
end;
hence p5 `1 >= e ; :: thesis: verum
end;
LE p51,p,P,p1,p2 by A24, A117, JORDAN5C:13;
hence p is_Rin P,p1,p2,e by A1, A3, A4, A118, A119; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A101; :: thesis: verum
end;
end;
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e or p is_OSin P,p1,p2,e ) ; :: thesis: verum