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_S-P_arc_joining p1,p2 & p1 `1 < e & p2 `1 > e & p in P & p `1 = e & not p is_Lin P,p1,p2,e holds
p is_Rin P,p1,p2,e
let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for e being Real st P is_S-P_arc_joining p1,p2 & p1 `1 < e & p2 `1 > e & p in P & p `1 = e & not p is_Lin P,p1,p2,e holds
p is_Rin P,p1,p2,e
let e be Real; :: thesis: ( P is_S-P_arc_joining p1,p2 & p1 `1 < e & p2 `1 > e & p in P & p `1 = e & not p is_Lin P,p1,p2,e implies p is_Rin P,p1,p2,e )
assume A1: ( P is_S-P_arc_joining p1,p2 & p1 `1 < e & p2 `1 > e & p in P & p `1 = e ) ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
then A2: P is_an_arc_of p1,p2 by TOPREAL4:3;
consider f being FinSequence of (TOP-REAL 2) such that
A3: ( f is being_S-Seq & P = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A1, TOPREAL4:def 1;
( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) by A3, TOPREAL1:def 10;
then A4: len f > 1 by XXREAL_0:2;
A5: L~ f = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TOPREAL1:def 6;
then consider Y being set such that
A6: ( p in Y & Y in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) by A1, A3, TARSKI:def 4;
A7: Y c= L~ f
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in L~ f )
assume x in Y ; :: thesis: x in L~ f
hence x in L~ f by A5, A6, TARSKI:def 4; :: thesis: verum
end;
consider i being Element of NAT such that
A8: ( Y = LSeg f,i & 1 <= i & i + 1 <= len f ) by A6;
A9: i < len f by A8, NAT_1:13;
then A10: i in dom f by A8, FINSEQ_3:27;
A11: 1 < len f by A8, A9, XXREAL_0:2;
A12: 1 < i + 1 by A8, NAT_1:13;
defpred S1[ Nat] means for p being Point of (TOP-REAL 2) st p = f . (i -' $1) holds
p `1 <> e;
1 in dom f by A11, FINSEQ_3:27;
then f /. 1 = f . 1 by PARTFUN1:def 8;
then A13: S1[i -' 1] by A1, A3, A8, NAT_D:58;
then A14: ex k being Nat st S1[k] ;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A14);
 then consider k being Nat such that
A15: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) ;
i -' k <= i by NAT_D:35;
then A16: i -' k < len f by A9, XXREAL_0:2;
A17: i - 1 >= 0 by A8, XREAL_1:50;
k <= i -' 1 by A13, A15;
then k <= i - 1 by A17, XREAL_0:def 2;
then k + 1 <= (i - 1) + 1 by XREAL_1:9;
then A18: (1 + k) - k <= i - k by XREAL_1:11;
then A19: i -' k >= 1 by XREAL_0:def 2;
then A20: i -' k in dom f by A16, FINSEQ_3:27;
then A21: f /. (i -' k) = f . (i -' k) by PARTFUN1:def 8;
then reconsider pk = f . (i -' k) as Point of (TOP-REAL 2) ;
A22: i -' k = i - k by A18, XREAL_0:def 2;
A23: pk `1 <> e by A15;
now
per cases ( pk `1 < e or pk `1 > e ) by A23, XXREAL_0:1;
case A24: pk `1 < e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
now
per cases ( k = 0 or k <> 0 ) ;
case A25: k = 0 ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
set p44 = f /. i;
A26: pk = f . i by A25, NAT_D:40
.= f /. i by A10, PARTFUN1:def 8 ;
A27: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5;
reconsider g = mid f,i,(len f) as FinSequence of (TOP-REAL 2) ;
A28: len g = ((len f) -' i) + 1 by A4, A8, A9, JORDAN3:27;
A29: (len f) - i > 0 by A9, XREAL_1:52;
then (len f) -' i = (len f) - i by XREAL_0:def 2;
then A30: ((len f) -' i) + 1 > 0 + 1 by A29, XREAL_1:10;
then A31: 1 + 1 <= len g by A28, NAT_1:13;
1 + (1 + i) <= 1 + (len f) by A8, XREAL_1:9;
then A32: ((1 + 1) + i) - i <= ((len f) + 1) - i by XREAL_1:11;
then A33: ( 1 <= i & i <= len f & len f <= len f & 1 <= 1 & 1 <= ((len f) + 1) - i ) by A8, NAT_1:13, XXREAL_0:2;
1 in dom g by A28, A30, FINSEQ_3:27;
then A34: g /. 1 = g . 1 by PARTFUN1:def 8
.= f . ((1 - 1) + i) by A33, JORDAN3:31
.= f /. i by A10, PARTFUN1:def 8 ;
reconsider ia = i + 1 as Element of NAT ;
ia in Seg (len f) by A8, A12, FINSEQ_1:3;
then A35: i + 1 in dom f by FINSEQ_1:def 3;
1 + 1 in Seg (len g) by A31, FINSEQ_1:3;
then 1 + 1 in dom g by FINSEQ_1:def 3;
then A36: g /. (1 + 1) = g . (1 + 1) by PARTFUN1:def 8
.= f . (((1 + 1) - 1) + i) by A8, A9, A32, JORDAN3:31
.= f /. (i + 1) by A35, PARTFUN1:def 8 ;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5
.= LSeg g,1 by A31, A34, A36, TOPREAL1:def 5 ;
then ( p in Y & Y in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A6, A8, A31;
then p in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then A37: p in L~ (mid f,i,(len f)) by TOPREAL1:def 6;
then A38: LE f /. i,p,P,p1,p2 by A3, A8, A9, SPRECT_4:4;
for p5 being Point of (TOP-REAL 2) st LE f /. i,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 f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
assume A39: ( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 <= e
Segment P,p1,p2,(f /. i),p = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) } by JORDAN6:29;
then A40: p5 in Segment P,p1,p2,(f /. i),p by A39;
f /. i in LSeg (f /. i),(f /. (i + 1)) by RLTOPSP1:69;
then LSeg (f /. i),p c= LSeg f,i by A6, A8, A27, TOPREAL1:12;
then A41: LSeg (f /. i),p c= P by A3, A7, A8, XBOOLE_1:1;
now
per cases ( f /. i <> p or f /. i = p ) ;
case f /. i <> p ; :: thesis: p5 `1 <= e
then LSeg (f /. i),p is_an_arc_of f /. i,p by TOPREAL1:15;
then Segment P,p1,p2,(f /. i),p = LSeg (f /. i),p by A2, A3, A8, A9, A37, A41, Th28, SPRECT_4:4;
hence p5 `1 <= e by A1, A24, A26, A40, TOPREAL1:9; :: thesis: verum
end;
case f /. i = p ; :: thesis: p5 `1 <= e
hence p5 `1 <= e by A1, A24, A26; :: thesis: verum
end;
end;
end;
hence p5 `1 <= e ; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A1, A2, A24, A26, A38, Def1; :: thesis: verum
end;
case k <> 0 ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
then A42: k > 0 ;
then A43: k >= 0 + 1 by NAT_1:13;
set p44 = f /. i;
A44: i > i -' k by A19, A43, NAT_D:51;
then A45: i > 1 by A19, XXREAL_0:2;
A46: now
assume A47: (f /. i) `1 <> e ; :: thesis: contradiction
f . i = f /. i by A10, PARTFUN1:def 8;
then for p9 being Point of (TOP-REAL 2) st p9 = f . (i -' 0 ) holds
p9 `1 <> e by A47, NAT_D:40;
hence contradiction by A15, A42; :: thesis: verum
end;
A48: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5;
reconsider g = mid f,i,(len f) as FinSequence of (TOP-REAL 2) ;
A49: len g = ((len f) -' i) + 1 by A4, A8, A9, JORDAN3:27;
A50: (len f) - i > 0 by A9, XREAL_1:52;
then (len f) -' i = (len f) - i by XREAL_0:def 2;
then A51: ((len f) -' i) + 1 > 0 + 1 by A50, XREAL_1:10;
then A52: 1 + 1 <= len g by A49, NAT_1:13;
1 + (1 + i) <= 1 + (len f) by A8, XREAL_1:9;
then A53: ((1 + 1) + i) - i <= ((len f) + 1) - i by XREAL_1:11;
then A54: ( 1 <= i & i <= len f & len f <= len f & 1 <= 1 & 1 <= ((len f) + 1) - i ) by A8, NAT_1:13, XXREAL_0:2;
1 in dom g by A49, A51, FINSEQ_3:27;
then A55: g /. 1 = g . 1 by PARTFUN1:def 8
.= f . ((1 - 1) + i) by A54, JORDAN3:31
.= f /. i by A10, PARTFUN1:def 8 ;
reconsider ia = i + 1 as Element of NAT ;
ia in Seg (len f) by A8, A12, FINSEQ_1:3;
then A56: i + 1 in dom f by FINSEQ_1:def 3;
1 + 1 in Seg (len g) by A52, FINSEQ_1:3;
then 1 + 1 in dom g by FINSEQ_1:def 3;
then A57: g /. (1 + 1) = g . (1 + 1) by PARTFUN1:def 8
.= f . (((1 + 1) - 1) + i) by A8, A9, A53, JORDAN3:31
.= f /. (i + 1) by A56, PARTFUN1:def 8 ;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5
.= LSeg g,1 by A52, A55, A57, TOPREAL1:def 5 ;
then ( p in Y & Y in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A6, A8, A52;
then p in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then A58: p in L~ (mid f,i,(len f)) by TOPREAL1:def 6;
then A59: LE f /. i,p,P,p1,p2 by A3, A8, A9, SPRECT_4:4;
A60: for p5 being Point of (TOP-REAL 2) st LE f /. i,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 f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
assume A61: ( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 <= e
Segment P,p1,p2,(f /. i),p = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) } by JORDAN6:29;
then A62: p5 in Segment P,p1,p2,(f /. i),p by A61;
f /. i in LSeg (f /. i),(f /. (i + 1)) by RLTOPSP1:69;
then LSeg (f /. i),p c= LSeg f,i by A6, A8, A48, TOPREAL1:12;
then A63: LSeg (f /. i),p c= P by A3, A7, A8, XBOOLE_1:1;
now
per cases ( f /. i <> p or f /. i = p ) ;
case f /. i <> p ; :: thesis: p5 `1 <= e
then LSeg (f /. i),p is_an_arc_of f /. i,p by TOPREAL1:15;
then Segment P,p1,p2,(f /. i),p = LSeg (f /. i),p by A2, A3, A8, A9, A58, A63, Th28, SPRECT_4:4;
hence p5 `1 <= e by A1, A46, A62, TOPREAL1:9; :: thesis: verum
end;
case f /. i = p ; :: thesis: p5 `1 <= e
then Segment P,p1,p2,(f /. i),p = {(f /. i)} by A1, Th1, TOPREAL4:3;
hence p5 `1 <= e by A46, A62, TARSKI:def 1; :: thesis: verum
end;
end;
end;
hence p5 `1 <= e ; :: thesis: verum
end;
reconsider g = mid f,1,i as FinSequence of (TOP-REAL 2) ;
A64: len g = (i -' 1) + 1 by A8, A9, A11, JORDAN3:27;
i - 1 > 0 by A45, XREAL_1:52;
then A65: i -' 1 = i - 1 by XREAL_0:def 2;
A66: i -' k < i by A19, A43, NAT_D:51;
A67: (i -' k) + 1 <= len g by A44, A64, A65, NAT_1:13;
A68: 1 <= i -' k by A18, XREAL_0:def 2;
A69: ( 1 <= 1 & 1 <= i & i <= len f & 1 <= i -' k & i -' k <= (i + 1) - 1 ) by A8, A19, A43, NAT_1:13, NAT_D:51;
A70: (i -' k) + 1 <= i by A44, NAT_1:13;
i -' k in Seg (len g) by A19, A64, A65, A66, FINSEQ_1:3;
then i -' k in dom g by FINSEQ_1:def 3;
then A71: g /. (i -' k) = g . (i -' k) by PARTFUN1:def 8
.= f . (((i -' k) - 1) + 1) by A69, JORDAN3:31
.= f /. (i -' k) by A20, PARTFUN1:def 8 ;
LSeg g,(i -' k) = LSeg (g /. (i -' k)),(g /. ((i -' k) + 1)) by A19, A67, TOPREAL1:def 5;
then ( pk in LSeg g,(i -' k) & LSeg g,(i -' k) in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A21, A64, A65, A68, A70, A71, RLTOPSP1:69;
then pk in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then pk in L~ (mid f,1,i) by TOPREAL1:def 6;
then A72: LE pk,f /. i,P,p1,p2 by A3, A9, A45, SPRECT_3:33;
then A73: LE pk,p,P,p1,p2 by A59, JORDAN5C:13;
A74: f /. i in P by A72, JORDAN5C:def 3;
A75: now
assume ex p51 being Point of (TOP-REAL 2) st
( LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 & not p51 `1 <= e ) ; :: thesis: contradiction
then consider p51 being Point of (TOP-REAL 2) such that
A76: ( LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 & p51 `1 > e ) ;
p51 in P by A76, JORDAN5C:def 3;
then consider Y3 being set such that
A77: ( p51 in Y3 & Y3 in { (LSeg f,i5) where i5 is Element of NAT : ( 1 <= i5 & i5 + 1 <= len f ) } ) by A3, A5, TARSKI:def 4;
consider kk being Element of NAT such that
A78: ( Y3 = LSeg f,kk & 1 <= kk & kk + 1 <= len f ) by A77;
A79: kk < len f by A78, NAT_1:13;
then kk in Seg (len f) by A78, FINSEQ_1:3;
then A80: kk in dom f by FINSEQ_1:def 3;
1 < kk + 1 by A78, NAT_1:13;
then kk + 1 in Seg (len f) by A78, FINSEQ_1:3;
then A81: kk + 1 in dom f by FINSEQ_1:def 3;
A82: LSeg f,kk = LSeg (f /. kk),(f /. (kk + 1)) by A78, TOPREAL1:def 5;
A83: LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A77, A78, JORDAN5C:26;
now
per cases ( (f /. kk) `1 > e or ( (f /. (kk + 1)) `1 > e & (f /. kk) `1 <= e ) ) by A76, A77, A78, A82, Th2;
case A84: (f /. kk) `1 > e ; :: thesis: contradiction
set k2 = i -' kk;
LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A3, A77, A78, JORDAN5C:25;
then A85: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A3, A76, JORDAN5C:13;
now
assume i - kk <= 0 ; :: thesis: contradiction
then (i - kk) + kk <= 0 + kk by XREAL_1:9;
then LE f /. i,f /. kk, L~ f,f /. 1,f /. (len f) by A3, A45, A79, JORDAN5C:24;
hence contradiction by A1, A3, A46, A84, A85, JORDAN5C:12, TOPREAL4:3; :: thesis: verum
end;
then A86: i -' kk = i - kk by XREAL_0:def 2;
then i - (i -' kk) > 0 by A78;
then A87: i -' (i -' kk) > 0 by XREAL_0:def 2;
A88: i - (i -' kk) = i -' (i -' kk) by A86, XREAL_0:def 2;
i -' (i -' kk) >= 0 + 1 by A87, NAT_1:13;
then S1[i -' kk] by A9, A84, A86, A88, FINSEQ_4:24, NAT_D:50;
then i -' kk >= k by A15;
then i - (i -' kk) <= i - k by XREAL_1:12;
then A89: LE f /. (i -' (i -' kk)),f /. (i -' k), L~ f,f /. 1,f /. (len f) by A3, A16, A22, A78, A86, A88, JORDAN5C:24;
A90: LE f /. (i -' k),p51, L~ f,f /. 1,f /. (len f) by A3, A20, A76, PARTFUN1:def 8;
A91: LE f /. (i -' k),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A21, A76, A83, JORDAN5C:13;
Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } by JORDAN6:29;
then A92: f /. (i -' k) in Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) by A86, A88, A89, A91;
A93: LSeg (f /. kk),(f /. (kk + 1)) c= L~ f
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (f /. kk),(f /. (kk + 1)) or z in L~ f )
assume A94: z in LSeg (f /. kk),(f /. (kk + 1)) ; :: thesis: z in L~ f
LSeg (f /. kk),(f /. (kk + 1)) in { (LSeg f,i7) where i7 is Element of NAT : ( 1 <= i7 & i7 + 1 <= len f ) } by A78, A82;
hence z in L~ f by A5, A94, TARSKI:def 4; :: thesis: verum
end;
A95: f is special by A3, TOPREAL1:def 10;
A96: f is one-to-one by A3, TOPREAL1:def 10;
kk < kk + 1 by NAT_1:13;
then A97: f . kk <> f . (kk + 1) by A80, A81, A96, FUNCT_1:def 8;
A98: f /. kk = f . kk by A80, PARTFUN1:def 8;
f /. (kk + 1) = f . (kk + 1) by A81, PARTFUN1:def 8;
then LSeg (f /. kk),(f /. (kk + 1)) is_an_arc_of f /. kk,f /. (kk + 1) by A97, A98, TOPREAL1:15;
then A99: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = LSeg (f /. kk),(f /. (kk + 1)) by A2, A3, A86, A88, A89, A91, A93, Th28, JORDAN5C:13;
A100: ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A78, A95, TOPREAL1:def 7;
(f /. (kk + 1)) `1 < e by A21, A24, A84, A92, A99, Th3;
then (f /. kk) `1 > (f /. (kk + 1)) `1 by A84, XXREAL_0:2;
then (f /. (i -' k)) `1 >= p51 `1 by A3, A77, A78, A79, A82, A90, A92, A99, A100, Th6;
hence contradiction by A21, A24, A76, XXREAL_0:2; :: thesis: verum
end;
case A101: ( (f /. (kk + 1)) `1 > e & (f /. kk) `1 <= e ) ; :: thesis: contradiction
then A102: (f /. kk) `1 < (f /. (kk + 1)) `1 by XXREAL_0:2;
set k2 = (i -' kk) -' 1;
A103: LSeg (f /. kk),(f /. (kk + 1)) c= L~ f
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (f /. kk),(f /. (kk + 1)) or z in L~ f )
assume A104: z in LSeg (f /. kk),(f /. (kk + 1)) ; :: thesis: z in L~ f
LSeg (f /. kk),(f /. (kk + 1)) in { (LSeg f,i7) where i7 is Element of NAT : ( 1 <= i7 & i7 + 1 <= len f ) } by A78, A82;
hence z in L~ f by A5, A104, TARSKI:def 4; :: thesis: verum
end;
A105: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } by JORDAN6:29;
A106: f is one-to-one by A3, TOPREAL1:def 10;
kk < kk + 1 by NAT_1:13;
then A107: f . kk <> f . (kk + 1) by A80, A81, A106, FUNCT_1:def 8;
A108: f /. kk = f . kk by A80, PARTFUN1:def 8;
f /. (kk + 1) = f . (kk + 1) by A81, PARTFUN1:def 8;
then LSeg (f /. kk),(f /. (kk + 1)) is_an_arc_of f /. kk,f /. (kk + 1) by A107, A108, TOPREAL1:15;
then A109: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = LSeg (f /. kk),(f /. (kk + 1)) by A2, A3, A78, A103, Th28, JORDAN5C:23;
LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A3, A77, A78, JORDAN5C:25;
then A110: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A3, A76, JORDAN5C:13;
A111: now
assume (i - kk) - 1 <= 0 ; :: thesis: contradiction
then (i - (kk + 1)) + (kk + 1) <= 0 + (kk + 1) by XREAL_1:9;
then LE f /. i,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A45, A78, JORDAN5C:24;
then A112: f /. i in LSeg (f /. kk),(f /. (kk + 1)) by A105, A109, A110;
A113: LSeg f,kk = LSeg (f /. kk),(f /. (kk + 1)) by A78, TOPREAL1:def 5;
f is special by A3, TOPREAL1:def 10;
then ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A78, TOPREAL1:def 7;
hence contradiction by A3, A46, A76, A77, A78, A79, A102, A112, A113, Th7; :: thesis: verum
end;
then ((i - kk) - 1) + 1 >= 0 + 1 by XREAL_1:9;
then i -' kk = i - kk by XREAL_0:def 2;
then A114: i - ((i -' kk) -' 1) = i - ((i - kk) - 1) by A111, XREAL_0:def 2
.= kk + 1 ;
then A115: i -' ((i -' kk) -' 1) > 0 by XREAL_0:def 2;
A116: i - ((i -' kk) -' 1) = i -' ((i -' kk) -' 1) by A114, XREAL_0:def 2;
A117: i -' ((i -' kk) -' 1) >= 0 + 1 by A115, NAT_1:13;
then S1[(i -' kk) -' 1] by A9, A101, A114, A116, FINSEQ_4:24, NAT_D:50;
then (i -' kk) -' 1 >= k by A15;
then i - ((i -' kk) -' 1) <= i - k by XREAL_1:12;
then A118: LE f /. (kk + 1),f /. (i -' k), L~ f,f /. 1,f /. (len f) by A3, A16, A22, A114, A116, A117, JORDAN5C:24;
LE f /. (i -' k),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A21, A76, A83, JORDAN5C:13;
hence contradiction by A1, A3, A21, A24, A101, A118, JORDAN5C:12, TOPREAL4:3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
for p5 being Point of (TOP-REAL 2) st LE pk,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 pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
assume A119: ( LE pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 <= e
then A120: p5 in P by JORDAN5C:def 3;
now
per cases ( LE p5,f /. i,P,p1,p2 or LE f /. i,p5,P,p1,p2 ) by A1, A74, A120, Th19, TOPREAL4:3;
case LE p5,f /. i,P,p1,p2 ; :: thesis: p5 `1 <= e
hence p5 `1 <= e by A75, A119; :: thesis: verum
end;
case LE f /. i,p5,P,p1,p2 ; :: thesis: p5 `1 <= e
hence p5 `1 <= e by A60, A119; :: thesis: verum
end;
end;
end;
hence p5 `1 <= e ; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A1, A2, A24, A73, Def1; :: thesis: verum
end;
end;
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ; :: thesis: verum
end;
case A121: pk `1 > e ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
now
per cases ( k = 0 or k <> 0 ) ;
case A122: k = 0 ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
set p44 = f /. i;
A123: pk = f . i by A122, NAT_D:40
.= f /. i by A10, PARTFUN1:def 8 ;
A124: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5;
reconsider g = mid f,i,(len f) as FinSequence of (TOP-REAL 2) ;
A125: len g = ((len f) -' i) + 1 by A4, A8, A9, JORDAN3:27;
A126: (len f) - i > 0 by A9, XREAL_1:52;
then (len f) -' i = (len f) - i by XREAL_0:def 2;
then A127: ((len f) -' i) + 1 > 0 + 1 by A126, XREAL_1:10;
then A128: 1 + 1 <= len g by A125, NAT_1:13;
1 + (1 + i) <= 1 + (len f) by A8, XREAL_1:9;
then A129: ((1 + 1) + i) - i <= ((len f) + 1) - i by XREAL_1:11;
then A130: ( 1 <= i & i <= len f & len f <= len f & 1 <= 1 & 1 <= ((len f) + 1) - i ) by A8, NAT_1:13, XXREAL_0:2;
1 in Seg (len g) by A125, A127, FINSEQ_1:3;
then 1 in dom g by FINSEQ_1:def 3;
then A131: g /. 1 = g . 1 by PARTFUN1:def 8
.= f . ((1 - 1) + i) by A130, JORDAN3:31
.= f /. i by A10, PARTFUN1:def 8 ;
reconsider ia = i + 1 as Element of NAT ;
ia in Seg (len f) by A8, A12, FINSEQ_1:3;
then A132: i + 1 in dom f by FINSEQ_1:def 3;
1 + 1 in Seg (len g) by A128, FINSEQ_1:3;
then 1 + 1 in dom g by FINSEQ_1:def 3;
then A133: g /. (1 + 1) = g . (1 + 1) by PARTFUN1:def 8
.= f . (((1 + 1) - 1) + i) by A8, A9, A129, JORDAN3:31
.= f /. (i + 1) by A132, PARTFUN1:def 8 ;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5
.= LSeg g,1 by A128, A131, A133, TOPREAL1:def 5 ;
then ( p in Y & Y in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A6, A8, A128;
then p in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then A134: p in L~ (mid f,i,(len f)) by TOPREAL1:def 6;
then A135: LE f /. i,p,P,p1,p2 by A3, A8, A9, SPRECT_4:4;
for p5 being Point of (TOP-REAL 2) st LE f /. i,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 f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
assume A136: ( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 >= e
Segment P,p1,p2,(f /. i),p = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) } by JORDAN6:29;
then A137: p5 in Segment P,p1,p2,(f /. i),p by A136;
f /. i in LSeg (f /. i),(f /. (i + 1)) by RLTOPSP1:69;
then LSeg (f /. i),p c= LSeg f,i by A6, A8, A124, TOPREAL1:12;
then A138: LSeg (f /. i),p c= P by A3, A7, A8, XBOOLE_1:1;
now
per cases ( f /. i <> p or f /. i = p ) ;
case f /. i <> p ; :: thesis: p5 `1 >= e
then LSeg (f /. i),p is_an_arc_of f /. i,p by TOPREAL1:15;
then Segment P,p1,p2,(f /. i),p = LSeg (f /. i),p by A2, A3, A8, A9, A134, A138, Th28, SPRECT_4:4;
hence p5 `1 >= e by A1, A121, A123, A137, TOPREAL1:9; :: thesis: verum
end;
case f /. i = p ; :: thesis: p5 `1 >= e
hence p5 `1 >= e by A1, A121, A123; :: thesis: verum
end;
end;
end;
hence p5 `1 >= e ; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A1, A2, A121, A123, A135, Def2; :: thesis: verum
end;
case k <> 0 ; :: thesis: ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
then A139: k > 0 ;
then A140: k >= 0 + 1 by NAT_1:13;
set p44 = f /. i;
A141: i > i -' k by A19, A140, NAT_D:51;
then A142: i > 1 by A19, XXREAL_0:2;
A143: now
assume A144: (f /. i) `1 <> e ; :: thesis: contradiction
f . i = f /. i by A10, PARTFUN1:def 8;
then for p9 being Point of (TOP-REAL 2) st p9 = f . (i -' 0 ) holds
p9 `1 <> e by A144, NAT_D:40;
hence contradiction by A15, A139; :: thesis: verum
end;
A145: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5;
reconsider g = mid f,i,(len f) as FinSequence of (TOP-REAL 2) ;
A146: len g = ((len f) -' i) + 1 by A4, A8, A9, JORDAN3:27;
A147: (len f) - i > 0 by A9, XREAL_1:52;
then (len f) -' i = (len f) - i by XREAL_0:def 2;
then A148: ((len f) -' i) + 1 > 0 + 1 by A147, XREAL_1:10;
then A149: 1 + 1 <= len g by A146, NAT_1:13;
1 + (1 + i) <= 1 + (len f) by A8, XREAL_1:9;
then A150: ((1 + 1) + i) - i <= ((len f) + 1) - i by XREAL_1:11;
then A151: ( 1 <= i & i <= len f & len f <= len f & 1 <= 1 & 1 <= ((len f) + 1) - i ) by A8, NAT_1:13, XXREAL_0:2;
1 in Seg (len g) by A146, A148, FINSEQ_1:3;
then 1 in dom g by FINSEQ_1:def 3;
then A152: g /. 1 = g . 1 by PARTFUN1:def 8
.= f . ((1 - 1) + i) by A151, JORDAN3:31
.= f /. i by A10, PARTFUN1:def 8 ;
reconsider ia = i + 1 as Element of NAT ;
ia in Seg (len f) by A8, A12, FINSEQ_1:3;
then A153: i + 1 in dom f by FINSEQ_1:def 3;
1 + 1 in Seg (len g) by A149, FINSEQ_1:3;
then 1 + 1 in dom g by FINSEQ_1:def 3;
then A154: g /. (1 + 1) = g . (1 + 1) by PARTFUN1:def 8
.= f . (((1 + 1) - 1) + i) by A8, A9, A150, JORDAN3:31
.= f /. (i + 1) by A153, PARTFUN1:def 8 ;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A8, TOPREAL1:def 5
.= LSeg g,1 by A149, A152, A154, TOPREAL1:def 5 ;
then ( p in Y & Y in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A6, A8, A149;
then p in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then A155: p in L~ (mid f,i,(len f)) by TOPREAL1:def 6;
then A156: LE f /. i,p,P,p1,p2 by A3, A8, A9, SPRECT_4:4;
A157: for p5 being Point of (TOP-REAL 2) st LE f /. i,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 f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
assume A158: ( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 >= e
Segment P,p1,p2,(f /. i),p = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) } by JORDAN6:29;
then A159: p5 in Segment P,p1,p2,(f /. i),p by A158;
f /. i in LSeg (f /. i),(f /. (i + 1)) by RLTOPSP1:69;
then LSeg (f /. i),p c= LSeg f,i by A6, A8, A145, TOPREAL1:12;
then A160: LSeg (f /. i),p c= P by A3, A7, A8, XBOOLE_1:1;
now
per cases ( f /. i <> p or f /. i = p ) ;
case f /. i <> p ; :: thesis: p5 `1 >= e
then LSeg (f /. i),p is_an_arc_of f /. i,p by TOPREAL1:15;
then Segment P,p1,p2,(f /. i),p = LSeg (f /. i),p by A2, A3, A8, A9, A155, A160, Th28, SPRECT_4:4;
hence p5 `1 >= e by A1, A143, A159, TOPREAL1:9; :: thesis: verum
end;
case f /. i = p ; :: thesis: p5 `1 >= e
then Segment P,p1,p2,(f /. i),p = {(f /. i)} by A1, Th1, TOPREAL4:3;
hence p5 `1 >= e by A143, A159, TARSKI:def 1; :: thesis: verum
end;
end;
end;
hence p5 `1 >= e ; :: thesis: verum
end;
reconsider g = mid f,1,i as FinSequence of (TOP-REAL 2) ;
A161: len g = (i -' 1) + 1 by A8, A9, A11, JORDAN3:27;
i - 1 > 0 by A142, XREAL_1:52;
then A162: i -' 1 = i - 1 by XREAL_0:def 2;
A163: i -' k < i by A19, A140, NAT_D:51;
A164: (i -' k) + 1 <= len g by A141, A161, A162, NAT_1:13;
A165: 1 <= i -' k by A18, XREAL_0:def 2;
A166: ( 1 <= 1 & 1 <= i & i <= len f & 1 <= i -' k & i -' k <= (i + 1) - 1 ) by A8, A19, A140, NAT_1:13, NAT_D:51;
A167: (i -' k) + 1 <= i by A141, NAT_1:13;
i -' k in Seg (len g) by A19, A161, A162, A163, FINSEQ_1:3;
then i -' k in dom g by FINSEQ_1:def 3;
then A168: g /. (i -' k) = g . (i -' k) by PARTFUN1:def 8
.= f . (((i -' k) - 1) + 1) by A166, JORDAN3:31
.= f /. (i -' k) by A20, PARTFUN1:def 8 ;
LSeg g,(i -' k) = LSeg (g /. (i -' k)),(g /. ((i -' k) + 1)) by A19, A164, TOPREAL1:def 5;
then ( pk in LSeg g,(i -' k) & LSeg g,(i -' k) in { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } ) by A21, A161, A162, A165, A167, A168, RLTOPSP1:69;
then pk in union { (LSeg g,i2) where i2 is Element of NAT : ( 1 <= i2 & i2 + 1 <= len g ) } by TARSKI:def 4;
then pk in L~ (mid f,1,i) by TOPREAL1:def 6;
then A169: LE pk,f /. i,P,p1,p2 by A3, A9, A142, SPRECT_3:33;
then A170: LE pk,p,P,p1,p2 by A156, JORDAN5C:13;
A171: f /. i in P by A169, JORDAN5C:def 3;
A172: now
assume ex p51 being Point of (TOP-REAL 2) st
( LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 & not p51 `1 >= e ) ; :: thesis: contradiction
then consider p51 being Point of (TOP-REAL 2) such that
A173: ( LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 & p51 `1 < e ) ;
p51 in P by A173, JORDAN5C:def 3;
then consider Y3 being set such that
A174: ( p51 in Y3 & Y3 in { (LSeg f,i5) where i5 is Element of NAT : ( 1 <= i5 & i5 + 1 <= len f ) } ) by A3, A5, TARSKI:def 4;
consider kk being Element of NAT such that
A175: ( Y3 = LSeg f,kk & 1 <= kk & kk + 1 <= len f ) by A174;
A176: kk < len f by A175, NAT_1:13;
then kk in Seg (len f) by A175, FINSEQ_1:3;
then A177: kk in dom f by FINSEQ_1:def 3;
1 < kk + 1 by A175, NAT_1:13;
then kk + 1 in Seg (len f) by A175, FINSEQ_1:3;
then A178: kk + 1 in dom f by FINSEQ_1:def 3;
A179: LSeg f,kk = LSeg (f /. kk),(f /. (kk + 1)) by A175, TOPREAL1:def 5;
A180: LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A174, A175, JORDAN5C:26;
now
per cases ( (f /. kk) `1 < e or ( (f /. (kk + 1)) `1 < e & (f /. kk) `1 >= e ) ) by A173, A174, A175, A179, Th3;
case A181: (f /. kk) `1 < e ; :: thesis: contradiction
set k2 = i -' kk;
LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A3, A174, A175, JORDAN5C:25;
then A182: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A3, A173, JORDAN5C:13;
now
assume i - kk <= 0 ; :: thesis: contradiction
then (i - kk) + kk <= 0 + kk by XREAL_1:9;
then LE f /. i,f /. kk, L~ f,f /. 1,f /. (len f) by A3, A142, A176, JORDAN5C:24;
hence contradiction by A1, A3, A143, A181, A182, JORDAN5C:12, TOPREAL4:3; :: thesis: verum
end;
then A183: i - (i -' kk) = i - (i - kk) by XREAL_0:def 2
.= kk ;
then A184: i - (i -' kk) = i -' (i -' kk) by XREAL_0:def 2;
then S1[i -' kk] by A9, A175, A181, A183, FINSEQ_4:24, NAT_D:50;
then i -' kk >= k by A15;
then i - (i -' kk) <= i - k by XREAL_1:12;
then A185: LE f /. (i -' (i -' kk)),f /. (i -' k), L~ f,f /. 1,f /. (len f) by A3, A16, A22, A175, A183, A184, JORDAN5C:24;
A186: LE f /. (i -' k),p51, L~ f,f /. 1,f /. (len f) by A3, A20, A173, PARTFUN1:def 8;
A187: LE f /. (i -' k),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A21, A173, A180, JORDAN5C:13;
Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } by JORDAN6:29;
then A188: f /. (i -' k) in Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) by A183, A184, A185, A187;
A189: LSeg (f /. kk),(f /. (kk + 1)) c= L~ f
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (f /. kk),(f /. (kk + 1)) or z in L~ f )
assume A190: z in LSeg (f /. kk),(f /. (kk + 1)) ; :: thesis: z in L~ f
LSeg (f /. kk),(f /. (kk + 1)) in { (LSeg f,i7) where i7 is Element of NAT : ( 1 <= i7 & i7 + 1 <= len f ) } by A175, A179;
hence z in L~ f by A5, A190, TARSKI:def 4; :: thesis: verum
end;
A191: f is special by A3, TOPREAL1:def 10;
A192: f is one-to-one by A3, TOPREAL1:def 10;
kk < kk + 1 by NAT_1:13;
then A193: f . kk <> f . (kk + 1) by A177, A178, A192, FUNCT_1:def 8;
A194: f /. kk = f . kk by A177, PARTFUN1:def 8;
f /. (kk + 1) = f . (kk + 1) by A178, PARTFUN1:def 8;
then LSeg (f /. kk),(f /. (kk + 1)) is_an_arc_of f /. kk,f /. (kk + 1) by A193, A194, TOPREAL1:15;
then A195: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = LSeg (f /. kk),(f /. (kk + 1)) by A2, A3, A183, A184, A185, A187, A189, Th28, JORDAN5C:13;
A196: ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A175, A191, TOPREAL1:def 7;
(f /. (kk + 1)) `1 > e by A21, A121, A181, A188, A195, Th2;
then (f /. kk) `1 < (f /. (kk + 1)) `1 by A181, XXREAL_0:2;
then (f /. (i -' k)) `1 <= p51 `1 by A3, A174, A175, A176, A179, A186, A188, A195, A196, Th7;
hence contradiction by A21, A121, A173, XXREAL_0:2; :: thesis: verum
end;
case A197: ( (f /. (kk + 1)) `1 < e & (f /. kk) `1 >= e ) ; :: thesis: contradiction
then A198: (f /. kk) `1 > (f /. (kk + 1)) `1 by XXREAL_0:2;
set k2 = (i -' kk) -' 1;
A199: LSeg (f /. kk),(f /. (kk + 1)) c= L~ f
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (f /. kk),(f /. (kk + 1)) or z in L~ f )
assume A200: z in LSeg (f /. kk),(f /. (kk + 1)) ; :: thesis: z in L~ f
LSeg (f /. kk),(f /. (kk + 1)) in { (LSeg f,i7) where i7 is Element of NAT : ( 1 <= i7 & i7 + 1 <= len f ) } by A175, A179;
hence z in L~ f by A5, A200, TARSKI:def 4; :: thesis: verum
end;
A201: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } by JORDAN6:29;
A202: f is one-to-one by A3, TOPREAL1:def 10;
kk < kk + 1 by NAT_1:13;
then A203: f . kk <> f . (kk + 1) by A177, A178, A202, FUNCT_1:def 8;
A204: f /. kk = f . kk by A177, PARTFUN1:def 8;
f /. (kk + 1) = f . (kk + 1) by A178, PARTFUN1:def 8;
then LSeg (f /. kk),(f /. (kk + 1)) is_an_arc_of f /. kk,f /. (kk + 1) by A203, A204, TOPREAL1:15;
then A205: Segment (L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1)) = LSeg (f /. kk),(f /. (kk + 1)) by A2, A3, A175, A199, Th28, JORDAN5C:23;
LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A3, A174, A175, JORDAN5C:25;
then A206: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A3, A173, JORDAN5C:13;
A207: now
assume (i - kk) - 1 <= 0 ; :: thesis: contradiction
then (i - (kk + 1)) + (kk + 1) <= 0 + (kk + 1) by XREAL_1:9;
then LE f /. i,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A142, A175, JORDAN5C:24;
then A208: f /. i in LSeg (f /. kk),(f /. (kk + 1)) by A201, A205, A206;
A209: LSeg f,kk = LSeg (f /. kk),(f /. (kk + 1)) by A175, TOPREAL1:def 5;
f is special by A3, TOPREAL1:def 10;
then ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A175, TOPREAL1:def 7;
hence contradiction by A3, A143, A173, A174, A175, A176, A198, A208, A209, Th6; :: thesis: verum
end;
then ((i - kk) - 1) + 1 >= 0 + 1 by XREAL_1:9;
then i -' kk = i - kk by XREAL_0:def 2;
then A210: i - ((i -' kk) -' 1) = i - ((i - kk) - 1) by A207, XREAL_0:def 2
.= kk + 1 ;
then A211: i -' ((i -' kk) -' 1) > 0 by XREAL_0:def 2;
A212: i - ((i -' kk) -' 1) = i -' ((i -' kk) -' 1) by A210, XREAL_0:def 2;
A213: i -' ((i -' kk) -' 1) >= 0 + 1 by A211, NAT_1:13;
then S1[(i -' kk) -' 1] by A9, A197, A210, A212, FINSEQ_4:24, NAT_D:50;
then (i -' kk) -' 1 >= k by A15;
then i - ((i -' kk) -' 1) <= i - k by XREAL_1:12;
then A214: LE f /. (kk + 1),f /. (i -' k), L~ f,f /. 1,f /. (len f) by A3, A16, A22, A210, A212, A213, JORDAN5C:24;
LE f /. (i -' k),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A3, A21, A173, A180, JORDAN5C:13;
hence contradiction by A1, A3, A21, A121, A197, A214, JORDAN5C:12, TOPREAL4:3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
for p5 being Point of (TOP-REAL 2) st LE pk,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 pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
assume A215: ( LE pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 ) ; :: thesis: p5 `1 >= e
then A216: p5 in P by JORDAN5C:def 3;
now
per cases ( LE p5,f /. i,P,p1,p2 or LE f /. i,p5,P,p1,p2 ) by A1, A171, A216, Th19, TOPREAL4:3;
case LE p5,f /. i,P,p1,p2 ; :: thesis: p5 `1 >= e
hence p5 `1 >= e by A172, A215; :: thesis: verum
end;
case LE f /. i,p5,P,p1,p2 ; :: thesis: p5 `1 >= e
hence p5 `1 >= e by A157, A215; :: thesis: verum
end;
end;
end;
hence p5 `1 >= e ; :: thesis: verum
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) by A1, A2, A121, A170, Def2; :: thesis: verum
end;
end;
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ; :: thesis: verum
end;
end;
end;
hence ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ; :: thesis: verum