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 & p2 `1 > e & p in P & p `1 = e & not p is_Lout P,p1,p2,e holds
p is_Rout 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 & p2 `1 > e & p in P & p `1 = e & not p is_Lout P,p1,p2,e holds
p is_Rout P,p1,p2,e
let e be Real; :: thesis: ( P is_S-P_arc_joining p1,p2 & p2 `1 > e & p in P & p `1 = e & not p is_Lout P,p1,p2,e implies p is_Rout P,p1,p2,e )
assume that
A1: P is_S-P_arc_joining p1,p2 and
A2: p2 `1 > e and
A3: p in P and
A4: p `1 = e ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )
consider f being FinSequence of (TOP-REAL 2) such that
A5: f is being_S-Seq and
A6: P = L~ f and
A7: p1 = f /. 1 and
A8: p2 = f /. (len f) by A1, TOPREAL4:def 1;
A9: P is_an_arc_of p1,p2 by A1, TOPREAL4:2;
A10: L~ f = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by TOPREAL1:def 4;
then consider Y being set such that
A11: p in Y and
A12: Y in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A3, A6, TARSKI:def 4;
consider i being Nat such that
A13: Y = LSeg (f,i) and
A14: 1 <= i and
A15: i + 1 <= len f by A12;
A16: 1 < i + 1 by A14, NAT_1:13;
A17: 1 < i + 1 by A14, NAT_1:13;
then i + 1 in Seg (len f) by A15, FINSEQ_1:1;
then A18: i + 1 in dom f by FINSEQ_1:def 3;
A19: Y c= L~ f by A10, A12, TARSKI:def 4;
defpred S₁[ Nat] means for p being Point of (TOP-REAL 2) st p = f . ((i + 1) + $1) holds
p `1 <> e;
A20: (len f) - (i + 1) >= 0 by A15, XREAL_1:48;
then A21: (i + 1) + ((len f) -' (i + 1)) = (i + 1) + ((len f) - (i + 1)) by XREAL_0:def 2
.= len f ;
A22: (len f) -' (i + 1) = (len f) - (i + 1) by A20, XREAL_0:def 2;
A23: i < len f by A15, NAT_1:13;
then 1 < len f by A14, XXREAL_0:2;
then len f in Seg (len f) by FINSEQ_1:1;
then len f in dom f by FINSEQ_1:def 3;
then A24: S₁[(len f) -' (i + 1)] by A2, A8, A21, PARTFUN1:def 6;
then A25: ex k being Nat st S₁[k] ;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A25);
then consider k being Nat such that
A26: S₁[k] and
A27: for n being Nat st S₁[n] holds
k <= n ;
k <= (len f) -' (i + 1) by A24, A27;
then A28: k + (i + 1) <= ((len f) - (i + 1)) + (i + 1) by A22, XREAL_1:7;
i + k >= i by NAT_1:11;
then A29: (i + k) + 1 >= i + 1 by XREAL_1:7;
then A30: (i + 1) + k > 1 by A16, XXREAL_0:2;
1 <= (i + 1) + k by A17, NAT_1:12;
then (i + 1) + k in Seg (len f) by A28, FINSEQ_1:1;
then A31: (i + 1) + k in dom f by FINSEQ_1:def 3;
then A32: f /. ((i + 1) + k) = f . ((i + 1) + k) by PARTFUN1:def 6;
then reconsider pk = f . ((i + 1) + k) as Point of (TOP-REAL 2) ;
A33: (k + i) + 1 > 1 by A16, A29, XXREAL_0:2;

now :: thesis: ( ( pk `1 < e & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) or ( pk `1 > e & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) )

per cases ( pk `1 < e or pk `1 > e ) by A26, XXREAL_0:1;

case A34: pk `1 < e ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

now :: thesis: ( ( k = 0 & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) or ( k <> 0 & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) )

per cases ( k = 0 or k <> 0 ) ;

case A35: k = 0 ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

set p44 = f /. (i + 1);
A36: pk = f /. (i + 1) by A18, A35, PARTFUN1:def 6;
A37: f /. (i + 1) in LSeg (p,(f /. (i + 1))) by RLTOPSP1:68;
A38: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A14, A15, TOPREAL1:def 3;
A39: for p5 being Point of (TOP-REAL 2) st LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 <= e

proof

f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
then LSeg (p,(f /. (i + 1))) c= LSeg (f,i) by A11, A13, A38, TOPREAL1:6;
then A40: LSeg (p,(f /. (i + 1))) c= P by A6, A19, A13;
let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 implies p5 `1 <= e )
A41: Segment (P,p1,p2,p,(f /. (i + 1))) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE p,p8,P,p1,p2 & LE p8,f /. (i + 1),P,p1,p2 ) } by JORDAN6:26;
assume ( LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 ) ; :: thesis: p5 `1 <= e
then A42: p5 in Segment (P,p1,p2,p,(f /. (i + 1))) by A41;

now :: thesis: ( ( f /. (i + 1) <> p & p5 `1 <= e ) or ( f /. (i + 1) = p & p5 `1 <= e ) )

per cases ( f /. (i + 1) <> p or f /. (i + 1) = p ) ;

case f /. (i + 1) <> p ; :: thesis: p5 `1 <= e

then LSeg (p,(f /. (i + 1))) is_an_arc_of p,f /. (i + 1) by TOPREAL1:9;
then Segment (P,p1,p2,p,(f /. (i + 1))) = LSeg (p,(f /. (i + 1))) by A9, A5, A6, A7, A8, A11, A13, A14, A23, A37, A40, Th25, SPRECT_4:4;
hence p5 `1 <= e by A4, A34, A36, A42, TOPREAL1:3; :: thesis: verum

end;

case f /. (i + 1) = p ; :: thesis: p5 `1 <= e

hence p5 `1 <= e by A4, A18, A34, A35, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

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

end;

LE p,f /. (i + 1),P,p1,p2 by A5, A6, A7, A8, A11, A13, A14, A23, A37, SPRECT_4:4;
hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A3, A4, A9, A34, A36, A39; :: thesis: verum

end;

case A43: k <> 0 ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

set p44 = f /. (i + 1);

A44: now :: thesis: not (f /. (i + 1)) `1 <> e

assume (f /. (i + 1)) `1 <> e ; :: thesis: contradiction
then for p9 being Point of (TOP-REAL 2) st p9 = f . ((i + 1) + 0) holds
p9 `1 <> e by A18, PARTFUN1:def 6;
hence contradiction by A27, A43; :: thesis: verum

end;

A45: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A14, A15, TOPREAL1:def 3;

A46: now :: thesis: for p51 being Point of (TOP-REAL 2) st LE f /. (i + 1),p51,P,p1,p2 & LE p51,pk,P,p1,p2 holds
p51 `1 <= e

assume ex p51 being Point of (TOP-REAL 2) st
( LE f /. (i + 1),p51,P,p1,p2 & LE p51,pk,P,p1,p2 & not p51 `1 <= e ) ; :: thesis: contradiction
then consider p51 being Point of (TOP-REAL 2) such that
A47: LE f /. (i + 1),p51,P,p1,p2 and
A48: LE p51,pk,P,p1,p2 and
A49: p51 `1 > e ;
p51 in P by A47, JORDAN5C:def 3;
then consider Y3 being set such that
A50: p51 in Y3 and
A51: Y3 in { (LSeg (f,i5)) where i5 is Nat : ( 1 <= i5 & i5 + 1 <= len f ) } by A6, A10, TARSKI:def 4;
consider kk being Nat such that
A52: Y3 = LSeg (f,kk) and
A53: 1 <= kk and
A54: kk + 1 <= len f by A51;
A55: LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A5, A50, A52, A53, A54, JORDAN5C:26;
A56: LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A5, A50, A52, A53, A54, JORDAN5C:25;
A57: kk - 1 >= 0 by A53, XREAL_1:48;
A58: LSeg (f,kk) = LSeg ((f /. kk),(f /. (kk + 1))) by A53, A54, TOPREAL1:def 3;
A59: kk < len f by A54, NAT_1:13;
then A60: kk in dom f by A53, FINSEQ_3:25;
then A61: f /. kk = f . kk by PARTFUN1:def 6;
A62: 1 < kk + 1 by A53, NAT_1:13;
then A63: kk + 1 in dom f by A54, FINSEQ_3:25;
( f is one-to-one & kk < kk + 1 ) by A5, NAT_1:13, TOPREAL1:def 8;
then A64: f . kk <> f . (kk + 1) by A60, A63, FUNCT_1:def 4;

now :: thesis: ( ( (f /. (kk + 1)) `1 > e & contradiction ) or ( (f /. kk) `1 > e & (f /. (kk + 1)) `1 <= e & contradiction ) )

per cases ( (f /. (kk + 1)) `1 > e or ( (f /. kk) `1 > e & (f /. (kk + 1)) `1 <= e ) ) by A49, A50, A52, A58, Th2;

case A65: (f /. (kk + 1)) `1 > e ; :: thesis: contradiction

set k2 = kk -' i;
A66: LE f /. (i + 1),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A47, A55, JORDAN5C:13;

now :: thesis: not kk - i < 0

assume kk - i < 0 ; :: thesis: contradiction
then (kk - i) + i < 0 + i by XREAL_1:6;
then LE f /. (kk + 1),f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A15, A62, JORDAN5C:24, XREAL_1:7;
hence contradiction by A1, A6, A7, A8, A44, A65, A66, JORDAN5C:12, TOPREAL4:2; :: thesis: verum

end;

then A67: (i + 1) + (kk -' i) = (1 + i) + (kk - i) by XREAL_0:def 2
.= kk + 1 ;
A68: LSeg ((f /. kk),(f /. (kk + 1))) c= L~ f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg ((f /. kk),(f /. (kk + 1))) or z in L~ f )
assume A69: 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 Nat : ( 1 <= i7 & i7 + 1 <= len f ) } by A53, A54, A58;
hence z in L~ f by A10, A69, TARSKI:def 4; :: thesis: verum

end;

f is special by A5, TOPREAL1:def 8;
then A70: ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A53, A54, TOPREAL1:def 5;
( f is one-to-one & kk < kk + 1 ) by A5, NAT_1:13, TOPREAL1:def 8;
then A71: f . kk <> f . (kk + 1) by A60, A63, FUNCT_1:def 4;
A72: LE p51,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A31, A48, PARTFUN1:def 6;
A73: LE f /. kk,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A32, A48, A56, JORDAN5C:13;
1 < kk + 1 by A53, NAT_1:13;
then S₁[kk -' i] by A54, A65, A67, FINSEQ_4:15;
then kk -' i >= k by A27;
then A74: LE f /. ((i + 1) + k),f /. ((i + 1) + (kk -' i)), L~ f,f /. 1,f /. (len f) by A5, A33, A54, A67, JORDAN5C:24, XREAL_1:7;
( f /. kk = f . kk & f /. (kk + 1) = f . (kk + 1) ) by A60, A63, PARTFUN1:def 6;
then LSeg ((f /. kk),(f /. (kk + 1))) is_an_arc_of f /. kk,f /. (kk + 1) by A71, TOPREAL1:9;
then A75: Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) = LSeg ((f /. kk),(f /. (kk + 1))) by A9, A6, A7, A8, A67, A74, A73, A68, Th25, 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:26;
then A76: f /. ((i + 1) + k) in Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) by A67, A74, A73;
then (f /. kk) `1 < e by A32, A34, A65, A75, Th3;
then (f /. kk) `1 < (f /. (kk + 1)) `1 by A65, XXREAL_0:2;
then (f /. ((i + 1) + k)) `1 >= p51 `1 by A5, A50, A52, A53, A59, A58, A72, A76, A75, A70, Th7;
hence contradiction by A32, A34, A49, XXREAL_0:2; :: thesis: verum

end;

case A77: ( (f /. kk) `1 > e & (f /. (kk + 1)) `1 <= e ) ; :: thesis: contradiction

set k2 = kk -' (i + 1);
A78: LSeg ((f /. kk),(f /. (kk + 1))) c= L~ f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg ((f /. kk),(f /. (kk + 1))) or z in L~ f )
assume A79: 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 Nat : ( 1 <= i7 & i7 + 1 <= len f ) } by A53, A54, A58;
hence z in L~ f by A10, A79, TARSKI:def 4; :: thesis: verum

end;

LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A5, A50, A52, A53, A54, JORDAN5C:26;
then A80: LE f /. (i + 1),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A47, JORDAN5C:13;
f /. (kk + 1) = f . (kk + 1) by A63, PARTFUN1:def 6;
then LSeg ((f /. kk),(f /. (kk + 1))) is_an_arc_of f /. kk,f /. (kk + 1) by A64, A61, TOPREAL1:9;
then A81: ( 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) ) } & Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) = LSeg ((f /. kk),(f /. (kk + 1))) ) by A9, A5, A6, A7, A8, A53, A54, A78, Th25, JORDAN5C:23, JORDAN6:26;

A82: now :: thesis: not kk - (i + 1) < 0

assume kk - (i + 1) < 0 ; :: thesis: contradiction
then (kk - (i + 1)) + (i + 1) < 0 + (i + 1) by XREAL_1:6;
then kk <= i by NAT_1:13;
then A83: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A5, A23, A53, JORDAN5C:24;
A84: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A14, A15, JORDAN5C:23;
then LE f /. i,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A80, JORDAN5C:13;
then f /. i in LSeg ((f /. kk),(f /. (kk + 1))) by A81, A83;
then (LSeg ((f /. kk),(f /. (kk + 1)))) /\ (LSeg ((f /. i),(f /. (i + 1)))) <> {} by A84, XBOOLE_0:def 4;
then A85: not LSeg ((f /. kk),(f /. (kk + 1))) misses LSeg ((f /. i),(f /. (i + 1))) by XBOOLE_0:def 7;
A86: kk - 1 = kk -' 1 by A57, XREAL_0:def 2;

A87: now :: thesis: not i = (kk -' 1) + 2

assume A88: i = (kk -' 1) + 2 ; :: thesis: contradiction
then kk + 1 < i + 1 by A86, NAT_1:13;
then LE f /. (kk + 1),f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A15, A62, JORDAN5C:24;
then f /. (i + 1) = f /. (kk + 1) by A1, A6, A7, A8, A80, JORDAN5C:12, TOPREAL4:2;
then f . (i + 1) = f /. (kk + 1) by A18, PARTFUN1:def 6;
then A89: f . (i + 1) = f . (kk + 1) by A63, PARTFUN1:def 6;
f is one-to-one by A5, TOPREAL1:def 8;
then i + 1 = kk + 1 by A18, A63, A89, FUNCT_1:def 4;
hence contradiction by A86, A88; :: thesis: verum

end;

A90: f is s.n.c. by A5, TOPREAL1:def 8;
A91: ( LSeg (f,kk) = LSeg ((f /. kk),(f /. (kk + 1))) & LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) by A14, A15, A53, A54, TOPREAL1:def 3;
then i + 1 >= kk by A85, A90, TOPREAL1:def 7;
then A92: (i + 1) - 1 >= kk - 1 by XREAL_1:9;
kk + 1 >= i by A85, A91, A90, TOPREAL1:def 7;
then A93: not not i = (kk -' 1) + 0 & ... & not i = (kk -' 1) + 2 by A86, A92, NAT_1:62;

A94: now :: thesis: ( ( i = kk & f /. (i + 1) in LSeg (f,kk) ) or ( i = kk - 1 & f /. (i + 1) in LSeg (f,kk) ) )

per cases ( i = kk or i = kk - 1 ) by A86, A93, A87;

case i = kk ; :: thesis: f /. (i + 1) in LSeg (f,kk)

hence f /. (i + 1) in LSeg (f,kk) by A45, RLTOPSP1:68; :: thesis: verum

end;

case i = kk - 1 ; :: thesis: f /. (i + 1) in LSeg (f,kk)

hence f /. (i + 1) in LSeg (f,kk) by A58, RLTOPSP1:68; :: thesis: verum

end;

end;

end;

f is special by A5, TOPREAL1:def 8;
then ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A53, A54, TOPREAL1:def 5;
hence contradiction by A5, A6, A7, A8, A44, A47, A49, A50, A52, A53, A59, A77, A94, Th6; :: thesis: verum

end;

then (i + 1) + (kk -' (i + 1)) = (i + 1) + (kk - (i + 1)) by XREAL_0:def 2
.= kk ;
then S₁[kk -' (i + 1)] by A53, A59, A77, FINSEQ_4:15;
then A95: kk -' (i + 1) >= k by A27;
kk -' (i + 1) = kk - (i + 1) by A82, XREAL_0:def 2;
then (kk - (i + 1)) + (i + 1) >= k + (i + 1) by A95, XREAL_1:7;
then A96: LE f /. ((i + 1) + k),f /. kk, L~ f,f /. 1,f /. (len f) by A5, A30, A59, JORDAN5C:24;
LE f /. kk,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A32, A48, A56, JORDAN5C:13;
hence contradiction by A1, A6, A7, A8, A32, A34, A77, A96, JORDAN5C:12, TOPREAL4:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A97: f /. (i + 1) in LSeg (p,(f /. (i + 1))) by RLTOPSP1:68;
A98: for p5 being Point of (TOP-REAL 2) st LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 holds
p5 `1 <= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 implies p5 `1 <= e )
A99: Segment (P,p1,p2,p,(f /. (i + 1))) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE p,p8,P,p1,p2 & LE p8,f /. (i + 1),P,p1,p2 ) } by JORDAN6:26;
assume ( LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 ) ; :: thesis: p5 `1 <= e
then A100: p5 in Segment (P,p1,p2,p,(f /. (i + 1))) by A99;
f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
then LSeg (p,(f /. (i + 1))) c= LSeg (f,i) by A11, A13, A45, TOPREAL1:6;
then A101: LSeg (p,(f /. (i + 1))) c= P by A6, A19, A13;

now :: thesis: ( ( f /. (i + 1) <> p & p5 `1 <= e ) or ( f /. (i + 1) = p & p5 `1 <= e ) )

per cases ( f /. (i + 1) <> p or f /. (i + 1) = p ) ;

case f /. (i + 1) <> p ; :: thesis: p5 `1 <= e

then LSeg (p,(f /. (i + 1))) is_an_arc_of p,f /. (i + 1) by TOPREAL1:9;
then Segment (P,p1,p2,p,(f /. (i + 1))) = LSeg (p,(f /. (i + 1))) by A9, A5, A6, A7, A8, A11, A13, A14, A23, A97, A101, Th25, SPRECT_4:4;
hence p5 `1 <= e by A4, A44, A100, TOPREAL1:3; :: thesis: verum

end;

case f /. (i + 1) = p ; :: thesis: p5 `1 <= e

then Segment (P,p1,p2,p,(f /. (i + 1))) = {(f /. (i + 1))} by A1, A3, Th1, TOPREAL4:2;
hence p5 `1 <= e by A44, A100, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

i + 1 <= (i + 1) + k by NAT_1:11;
then A102: LE f /. (i + 1),pk,P,p1,p2 by A5, A6, A7, A8, A17, A28, A32, JORDAN5C:24;
then A103: f /. (i + 1) in P by JORDAN5C:def 3;
A104: for p5 being Point of (TOP-REAL 2) st LE p5,pk,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 <= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p5,pk,P,p1,p2 & LE p,p5,P,p1,p2 implies p5 `1 <= e )
assume that
A105: LE p5,pk,P,p1,p2 and
A106: LE p,p5,P,p1,p2 ; :: thesis: p5 `1 <= e
A107: p5 in P by A105, JORDAN5C:def 3;

now :: thesis: ( ( LE f /. (i + 1),p5,P,p1,p2 & p5 `1 <= e ) or ( LE p5,f /. (i + 1),P,p1,p2 & p5 `1 <= e ) )

per cases ( LE f /. (i + 1),p5,P,p1,p2 or LE p5,f /. (i + 1),P,p1,p2 ) by A1, A103, A107, Th19, TOPREAL4:2;

case LE f /. (i + 1),p5,P,p1,p2 ; :: thesis: p5 `1 <= e

hence p5 `1 <= e by A46, A105; :: thesis: verum

end;

case LE p5,f /. (i + 1),P,p1,p2 ; :: thesis: p5 `1 <= e

hence p5 `1 <= e by A98, A106; :: thesis: verum

end;

end;

end;

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

end;

LE p,f /. (i + 1),P,p1,p2 by A5, A6, A7, A8, A11, A13, A14, A23, A97, SPRECT_4:4;
then LE p,pk,P,p1,p2 by A102, JORDAN5C:13;
hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A3, A4, A9, A34, A104; :: thesis: verum

end;

end;

end;

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

end;

case A108: pk `1 > e ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

now :: thesis: ( ( k = 0 & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) or ( k <> 0 & ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) ) )

per cases ( k = 0 or k <> 0 ) ;

case A109: k = 0 ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

set p44 = f /. (i + 1);
A110: pk = f /. (i + 1) by A18, A109, PARTFUN1:def 6;
A111: f /. (i + 1) in LSeg (p,(f /. (i + 1))) by RLTOPSP1:68;
A112: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A14, A15, TOPREAL1:def 3;
A113: for p5 being Point of (TOP-REAL 2) st LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 >= e

proof

f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
then LSeg (p,(f /. (i + 1))) c= LSeg (f,i) by A11, A13, A112, TOPREAL1:6;
then A114: LSeg (p,(f /. (i + 1))) c= P by A6, A19, A13;
let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 implies p5 `1 >= e )
A115: Segment (P,p1,p2,p,(f /. (i + 1))) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE p,p8,P,p1,p2 & LE p8,f /. (i + 1),P,p1,p2 ) } by JORDAN6:26;
assume ( LE p5,f /. (i + 1),P,p1,p2 & LE p,p5,P,p1,p2 ) ; :: thesis: p5 `1 >= e
then A116: p5 in Segment (P,p1,p2,p,(f /. (i + 1))) by A115;

now :: thesis: ( ( f /. (i + 1) <> p & p5 `1 >= e ) or ( f /. (i + 1) = p & p5 `1 >= e ) )

per cases ( f /. (i + 1) <> p or f /. (i + 1) = p ) ;

case f /. (i + 1) <> p ; :: thesis: p5 `1 >= e

then LSeg (p,(f /. (i + 1))) is_an_arc_of p,f /. (i + 1) by TOPREAL1:9;
then Segment (P,p1,p2,p,(f /. (i + 1))) = LSeg (p,(f /. (i + 1))) by A9, A5, A6, A7, A8, A11, A13, A14, A23, A111, A114, Th25, SPRECT_4:4;
hence p5 `1 >= e by A4, A108, A110, A116, TOPREAL1:3; :: thesis: verum

end;

case f /. (i + 1) = p ; :: thesis: p5 `1 >= e

hence p5 `1 >= e by A4, A18, A108, A109, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

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

end;

LE p,f /. (i + 1),P,p1,p2 by A5, A6, A7, A8, A11, A13, A14, A23, A111, SPRECT_4:4;
hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A3, A4, A9, A108, A110, A113; :: thesis: verum

end;

case A117: k <> 0 ; :: thesis: ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e )

set p44 = f /. (i + 1);

A118: now :: thesis: not (f /. (i + 1)) `1 <> e

assume (f /. (i + 1)) `1 <> e ; :: thesis: contradiction
then for p9 being Point of (TOP-REAL 2) st p9 = f . ((i + 1) + 0) holds
p9 `1 <> e by A18, PARTFUN1:def 6;
hence contradiction by A27, A117; :: thesis: verum

end;

A119: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A14, A15, TOPREAL1:def 3;

A120: now :: thesis: for p51 being Point of (TOP-REAL 2) st LE f /. (i + 1),p51,P,p1,p2 & LE p51,pk,P,p1,p2 holds
p51 `1 >= e

assume ex p51 being Point of (TOP-REAL 2) st
( LE f /. (i + 1),p51,P,p1,p2 & LE p51,pk,P,p1,p2 & not p51 `1 >= e ) ; :: thesis: contradiction
then consider p51 being Point of (TOP-REAL 2) such that
A121: LE f /. (i + 1),p51,P,p1,p2 and
A122: LE p51,pk,P,p1,p2 and
A123: p51 `1 < e ;
p51 in P by A121, JORDAN5C:def 3;
then consider Y3 being set such that
A124: p51 in Y3 and
A125: Y3 in { (LSeg (f,i5)) where i5 is Nat : ( 1 <= i5 & i5 + 1 <= len f ) } by A6, A10, TARSKI:def 4;
consider kk being Nat such that
A126: Y3 = LSeg (f,kk) and
A127: 1 <= kk and
A128: kk + 1 <= len f by A125;
A129: LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A5, A124, A126, A127, A128, JORDAN5C:26;
A130: LE f /. kk,p51, L~ f,f /. 1,f /. (len f) by A5, A124, A126, A127, A128, JORDAN5C:25;
A131: kk - 1 >= 0 by A127, XREAL_1:48;
A132: LSeg (f,kk) = LSeg ((f /. kk),(f /. (kk + 1))) by A127, A128, TOPREAL1:def 3;
A133: kk < len f by A128, NAT_1:13;
then kk in Seg (len f) by A127, FINSEQ_1:1;
then A134: kk in dom f by FINSEQ_1:def 3;
then A135: f /. kk = f . kk by PARTFUN1:def 6;
A136: 1 < kk + 1 by A127, NAT_1:13;
then A137: kk + 1 in dom f by A128, FINSEQ_3:25;
( f is one-to-one & kk < kk + 1 ) by A5, NAT_1:13, TOPREAL1:def 8;
then A138: f . kk <> f . (kk + 1) by A134, A137, FUNCT_1:def 4;

now :: thesis: ( ( (f /. (kk + 1)) `1 < e & contradiction ) or ( (f /. kk) `1 < e & (f /. (kk + 1)) `1 >= e & contradiction ) )

per cases ( (f /. (kk + 1)) `1 < e or ( (f /. kk) `1 < e & (f /. (kk + 1)) `1 >= e ) ) by A123, A124, A126, A132, Th3;

case A139: (f /. (kk + 1)) `1 < e ; :: thesis: contradiction

set k2 = kk -' i;
A140: LE f /. (i + 1),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A121, A129, JORDAN5C:13;

now :: thesis: not kk - i < 0

assume kk - i < 0 ; :: thesis: contradiction
then (kk - i) + i < 0 + i by XREAL_1:6;
then LE f /. (kk + 1),f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A15, A136, JORDAN5C:24, XREAL_1:7;
hence contradiction by A1, A6, A7, A8, A118, A139, A140, JORDAN5C:12, TOPREAL4:2; :: thesis: verum

end;

then A141: (i + 1) + (kk -' i) = (1 + i) + (kk - i) by XREAL_0:def 2
.= kk + 1 ;
A142: LSeg ((f /. kk),(f /. (kk + 1))) c= L~ f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg ((f /. kk),(f /. (kk + 1))) or z in L~ f )
assume A143: 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 Nat : ( 1 <= i7 & i7 + 1 <= len f ) } by A127, A128, A132;
hence z in L~ f by A10, A143, TARSKI:def 4; :: thesis: verum

end;

f is special by A5, TOPREAL1:def 8;
then A144: ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A127, A128, TOPREAL1:def 5;
( f is one-to-one & kk < kk + 1 ) by A5, NAT_1:13, TOPREAL1:def 8;
then A145: f . kk <> f . (kk + 1) by A134, A137, FUNCT_1:def 4;
A146: LE p51,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A31, A122, PARTFUN1:def 6;
A147: LE f /. kk,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A32, A122, A130, JORDAN5C:13;
1 < kk + 1 by A127, NAT_1:13;
then S₁[kk -' i] by A128, A139, A141, FINSEQ_4:15;
then kk -' i >= k by A27;
then A148: LE f /. ((i + 1) + k),f /. ((i + 1) + (kk -' i)), L~ f,f /. 1,f /. (len f) by A5, A33, A128, A141, JORDAN5C:24, XREAL_1:7;
( f /. kk = f . kk & f /. (kk + 1) = f . (kk + 1) ) by A134, A137, PARTFUN1:def 6;
then LSeg ((f /. kk),(f /. (kk + 1))) is_an_arc_of f /. kk,f /. (kk + 1) by A145, TOPREAL1:9;
then A149: Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) = LSeg ((f /. kk),(f /. (kk + 1))) by A9, A6, A7, A8, A141, A148, A147, A142, Th25, 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:26;
then A150: f /. ((i + 1) + k) in Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) by A141, A148, A147;
then (f /. kk) `1 > e by A32, A108, A139, A149, Th2;
then (f /. kk) `1 > (f /. (kk + 1)) `1 by A139, XXREAL_0:2;
then (f /. ((i + 1) + k)) `1 <= p51 `1 by A5, A124, A126, A127, A133, A132, A146, A150, A149, A144, Th6;
hence contradiction by A32, A108, A123, XXREAL_0:2; :: thesis: verum

end;

case A151: ( (f /. kk) `1 < e & (f /. (kk + 1)) `1 >= e ) ; :: thesis: contradiction

set k2 = kk -' (i + 1);
A152: LSeg ((f /. kk),(f /. (kk + 1))) c= L~ f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg ((f /. kk),(f /. (kk + 1))) or z in L~ f )
assume A153: 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 Nat : ( 1 <= i7 & i7 + 1 <= len f ) } by A127, A128, A132;
hence z in L~ f by A10, A153, TARSKI:def 4; :: thesis: verum

end;

LE p51,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A5, A124, A126, A127, A128, JORDAN5C:26;
then A154: LE f /. (i + 1),f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A121, JORDAN5C:13;
f /. (kk + 1) = f . (kk + 1) by A137, PARTFUN1:def 6;
then LSeg ((f /. kk),(f /. (kk + 1))) is_an_arc_of f /. kk,f /. (kk + 1) by A138, A135, TOPREAL1:9;
then A155: ( 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) ) } & Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) = LSeg ((f /. kk),(f /. (kk + 1))) ) by A9, A5, A6, A7, A8, A127, A128, A152, Th25, JORDAN5C:23, JORDAN6:26;

A156: now :: thesis: not kk - (i + 1) < 0

assume kk - (i + 1) < 0 ; :: thesis: contradiction
then (kk - (i + 1)) + (i + 1) < 0 + (i + 1) by XREAL_1:6;
then kk <= i by NAT_1:13;
then A157: LE f /. kk,f /. i, L~ f,f /. 1,f /. (len f) by A5, A23, A127, JORDAN5C:24;
A158: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A14, A15, JORDAN5C:23;
then LE f /. i,f /. (kk + 1), L~ f,f /. 1,f /. (len f) by A154, JORDAN5C:13;
then f /. i in LSeg ((f /. kk),(f /. (kk + 1))) by A155, A157;
then (LSeg ((f /. kk),(f /. (kk + 1)))) /\ (LSeg ((f /. i),(f /. (i + 1)))) <> {} by A158, XBOOLE_0:def 4;
then A159: not LSeg ((f /. kk),(f /. (kk + 1))) misses LSeg ((f /. i),(f /. (i + 1))) by XBOOLE_0:def 7;
A160: kk - 1 = kk -' 1 by A131, XREAL_0:def 2;

A161: now :: thesis: not i = (kk -' 1) + 2

assume A162: i = (kk -' 1) + 2 ; :: thesis: contradiction
then kk + 1 < i + 1 by A160, NAT_1:13;
then LE f /. (kk + 1),f /. (i + 1), L~ f,f /. 1,f /. (len f) by A5, A15, A136, JORDAN5C:24;
then f /. (i + 1) = f /. (kk + 1) by A1, A6, A7, A8, A154, JORDAN5C:12, TOPREAL4:2;
then f . (i + 1) = f /. (kk + 1) by A18, PARTFUN1:def 6;
then A163: f . (i + 1) = f . (kk + 1) by A137, PARTFUN1:def 6;
f is one-to-one by A5, TOPREAL1:def 8;
then i + 1 = kk + 1 by A18, A137, A163, FUNCT_1:def 4;
hence contradiction by A160, A162; :: thesis: verum

end;

A164: f is s.n.c. by A5, TOPREAL1:def 8;
A165: ( LSeg (f,kk) = LSeg ((f /. kk),(f /. (kk + 1))) & LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) by A14, A15, A127, A128, TOPREAL1:def 3;
then i + 1 >= kk by A159, A164, TOPREAL1:def 7;
then A166: (i + 1) - 1 >= kk - 1 by XREAL_1:9;
kk + 1 >= i by A159, A165, A164, TOPREAL1:def 7;
then A167: not not i = (kk -' 1) + 0 & ... & not i = (kk -' 1) + 2 by A160, A166, NAT_1:62;

A168: now :: thesis: ( ( i = kk & f /. (i + 1) in LSeg (f,kk) ) or ( i = kk - 1 & f /. (i + 1) in LSeg (f,kk) ) )

per cases ( i = kk or i = kk - 1 ) by A160, A167, A161;

case i = kk ; :: thesis: f /. (i + 1) in LSeg (f,kk)

hence f /. (i + 1) in LSeg (f,kk) by A119, RLTOPSP1:68; :: thesis: verum

end;

case i = kk - 1 ; :: thesis: f /. (i + 1) in LSeg (f,kk)

hence f /. (i + 1) in LSeg (f,kk) by A132, RLTOPSP1:68; :: thesis: verum

end;

end;

end;

f is special by A5, TOPREAL1:def 8;
then ( (f /. kk) `1 = (f /. (kk + 1)) `1 or (f /. kk) `2 = (f /. (kk + 1)) `2 ) by A127, A128, TOPREAL1:def 5;
hence contradiction by A5, A6, A7, A8, A118, A121, A123, A124, A126, A127, A133, A151, A168, Th7; :: thesis: verum

end;

then (i + 1) + (kk -' (i + 1)) = (i + 1) + (kk - (i + 1)) by XREAL_0:def 2
.= kk ;
then S₁[kk -' (i + 1)] by A127, A133, A151, FINSEQ_4:15;
then A169: kk -' (i + 1) >= k by A27;
kk -' (i + 1) = kk - (i + 1) by A156, XREAL_0:def 2;
then (kk - (i + 1)) + (i + 1) >= k + (i + 1) by A169, XREAL_1:7;
then A170: LE f /. ((i + 1) + k),f /. kk, L~ f,f /. 1,f /. (len f) by A5, A30, A133, JORDAN5C:24;
LE f /. kk,f /. ((i + 1) + k), L~ f,f /. 1,f /. (len f) by A6, A7, A8, A32, A122, A130, JORDAN5C:13;
hence contradiction by A1, A6, A7, A8, A32, A108, A151, A170, JORDAN5C:12, TOPREAL4:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A171: f /. (i + 1) in LSeg (p,(f /. (i + 1))) by RLTOPSP1:68;
A172: for p5 being Point of (TOP-REAL 2) st LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 holds
p5 `1 >= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 implies p5 `1 >= e )
A173: Segment (P,p1,p2,p,(f /. (i + 1))) = { p8 where p8 is Point of (TOP-REAL 2) : ( LE p,p8,P,p1,p2 & LE p8,f /. (i + 1),P,p1,p2 ) } by JORDAN6:26;
assume ( LE p,p5,P,p1,p2 & LE p5,f /. (i + 1),P,p1,p2 ) ; :: thesis: p5 `1 >= e
then A174: p5 in Segment (P,p1,p2,p,(f /. (i + 1))) by A173;
f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
then LSeg (p,(f /. (i + 1))) c= LSeg (f,i) by A11, A13, A119, TOPREAL1:6;
then A175: LSeg (p,(f /. (i + 1))) c= P by A6, A19, A13;

now :: thesis: ( ( f /. (i + 1) <> p & p5 `1 >= e ) or ( f /. (i + 1) = p & p5 `1 >= e ) )

per cases ( f /. (i + 1) <> p or f /. (i + 1) = p ) ;

case f /. (i + 1) <> p ; :: thesis: p5 `1 >= e

then LSeg (p,(f /. (i + 1))) is_an_arc_of p,f /. (i + 1) by TOPREAL1:9;
then Segment (P,p1,p2,p,(f /. (i + 1))) = LSeg (p,(f /. (i + 1))) by A9, A5, A6, A7, A8, A11, A13, A14, A23, A171, A175, Th25, SPRECT_4:4;
hence p5 `1 >= e by A4, A118, A174, TOPREAL1:3; :: thesis: verum

end;

case f /. (i + 1) = p ; :: thesis: p5 `1 >= e

then Segment (P,p1,p2,p,(f /. (i + 1))) = {(f /. (i + 1))} by A1, A3, Th1, TOPREAL4:2;
hence p5 `1 >= e by A118, A174, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

i + 1 <= (i + 1) + k by NAT_1:11;
then A176: LE f /. (i + 1),pk,P,p1,p2 by A5, A6, A7, A8, A17, A28, A32, JORDAN5C:24;
then A177: f /. (i + 1) in P by JORDAN5C:def 3;
A178: for p5 being Point of (TOP-REAL 2) st LE p5,pk,P,p1,p2 & LE p,p5,P,p1,p2 holds
p5 `1 >= e

proof

let p5 be Point of (TOP-REAL 2); :: thesis: ( LE p5,pk,P,p1,p2 & LE p,p5,P,p1,p2 implies p5 `1 >= e )
assume that
A179: LE p5,pk,P,p1,p2 and
A180: LE p,p5,P,p1,p2 ; :: thesis: p5 `1 >= e
A181: p5 in P by A179, JORDAN5C:def 3;

now :: thesis: ( ( LE f /. (i + 1),p5,P,p1,p2 & p5 `1 >= e ) or ( LE p5,f /. (i + 1),P,p1,p2 & p5 `1 >= e ) )

per cases ( LE f /. (i + 1),p5,P,p1,p2 or LE p5,f /. (i + 1),P,p1,p2 ) by A1, A177, A181, Th19, TOPREAL4:2;

case LE f /. (i + 1),p5,P,p1,p2 ; :: thesis: p5 `1 >= e

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

end;

case LE p5,f /. (i + 1),P,p1,p2 ; :: thesis: p5 `1 >= e

hence p5 `1 >= e by A172, A180; :: thesis: verum

end;

end;

end;

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

end;

LE p,f /. (i + 1),P,p1,p2 by A5, A6, A7, A8, A11, A13, A14, A23, A171, SPRECT_4:4;
then LE p,pk,P,p1,p2 by A176, JORDAN5C:13;
hence ( p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e ) by A3, A4, A9, A108, A178; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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