let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat st n > 0 holds

for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

let n be Nat; :: thesis: ( n > 0 implies for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )

assume A1: n > 0 ; :: thesis: for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

set US = Upper_Seq (C,n);

set sr = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2;

set Ebo = E-bound (L~ (Cage (C,n)));

set Wbo = W-bound (L~ (Cage (C,n)));

set Emax = E-max (L~ (Cage (C,n)));

set Wmin = W-min (L~ (Cage (C,n)));

set FiP = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. $1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 );

A2: W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n))) by SPRECT_1:31;

then A3: W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by XREAL_1:226;

A4: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n))) by A2, XREAL_1:226;

A5: for k being non zero Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[1]
_{1}[k]
from NAT_1:sch 10(A44, A5);

let k be Nat; :: thesis: ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )

assume ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ) ; :: thesis: ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

hence ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A45; :: thesis: verum

for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

let n be Nat; :: thesis: ( n > 0 implies for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )

assume A1: n > 0 ; :: thesis: for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds

((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

set US = Upper_Seq (C,n);

set sr = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2;

set Ebo = E-bound (L~ (Cage (C,n)));

set Wbo = W-bound (L~ (Cage (C,n)));

set Emax = E-max (L~ (Cage (C,n)));

set Wmin = W-min (L~ (Cage (C,n)));

set FiP = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

defpred S

A2: W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n))) by SPRECT_1:31;

then A3: W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by XREAL_1:226;

A4: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n))) by A2, XREAL_1:226;

A5: for k being non zero Nat st S

S

proof

A44:
S
set GC1 = (Gauge (C,n)) * ((Center (Gauge (C,n))),1);

let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ) ; :: thesis: S_{1}[k + 1]

4 <= len (Gauge (C,n)) by JORDAN8:10;

then 1 <= len (Gauge (C,n)) by XXREAL_0:2;

then A7: 1 <= width (Gauge (C,n)) by JORDAN8:def 1;

then A8: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Th35

.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by Th33 ;

A9: k >= 1 by NAT_1:14;

A10: (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by JORDAN1F:7;

A11: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A1, Th47;

then A12: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by FINSEQ_4:20;

then A13: 1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) by FINSEQ_3:25;

A14: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;

A15: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;

reconsider kk = k as Nat ;

assume that

A16: 1 <= k + 1 and

A17: k + 1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

A18: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n)) by A12, FINSEQ_3:25;

then A19: k + 1 <= len (Upper_Seq (C,n)) by A17, XXREAL_0:2;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

then consider i1, j1, i2, j2 being Nat such that

A20: [i1,j1] in Indices (Gauge (C,n)) and

A21: (Upper_Seq (C,n)) /. kk = (Gauge (C,n)) * (i1,j1) and

A22: [i2,j2] in Indices (Gauge (C,n)) and

A23: (Upper_Seq (C,n)) /. (kk + 1) = (Gauge (C,n)) * (i2,j2) and

A24: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9, A19, JORDAN8:3;

A25: 1 <= i1 by A20, MATRIX_0:32;

A26: ( 1 <= j1 & j1 <= width (Gauge (C,n)) ) by A20, MATRIX_0:32;

A27: j2 <= width (Gauge (C,n)) by A22, MATRIX_0:32;

A28: ( 1 <= i2 & 1 <= j2 ) by A22, MATRIX_0:32;

A29: i2 <= len (Gauge (C,n)) by A22, MATRIX_0:32;

A30: i1 <= len (Gauge (C,n)) by A20, MATRIX_0:32;

A31: ( Center (Gauge (C,n)) <= len (Gauge (C,n)) & i1 + 1 >= 1 ) by JORDAN1B:13, NAT_1:11;

end;let k be non zero Nat; :: thesis: ( S

assume A6: ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ) ; :: thesis: S

4 <= len (Gauge (C,n)) by JORDAN8:10;

then 1 <= len (Gauge (C,n)) by XXREAL_0:2;

then A7: 1 <= width (Gauge (C,n)) by JORDAN8:def 1;

then A8: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, Th35

.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by Th33 ;

A9: k >= 1 by NAT_1:14;

A10: (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by JORDAN1F:7;

A11: First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A1, Th47;

then A12: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by FINSEQ_4:20;

then A13: 1 <= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) by FINSEQ_3:25;

A14: 1 <= Center (Gauge (C,n)) by JORDAN1B:11;

A15: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;

reconsider kk = k as Nat ;

assume that

A16: 1 <= k + 1 and

A17: k + 1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

A18: (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n)) by A12, FINSEQ_3:25;

then A19: k + 1 <= len (Upper_Seq (C,n)) by A17, XXREAL_0:2;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

then consider i1, j1, i2, j2 being Nat such that

A20: [i1,j1] in Indices (Gauge (C,n)) and

A21: (Upper_Seq (C,n)) /. kk = (Gauge (C,n)) * (i1,j1) and

A22: [i2,j2] in Indices (Gauge (C,n)) and

A23: (Upper_Seq (C,n)) /. (kk + 1) = (Gauge (C,n)) * (i2,j2) and

A24: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9, A19, JORDAN8:3;

A25: 1 <= i1 by A20, MATRIX_0:32;

A26: ( 1 <= j1 & j1 <= width (Gauge (C,n)) ) by A20, MATRIX_0:32;

A27: j2 <= width (Gauge (C,n)) by A22, MATRIX_0:32;

A28: ( 1 <= i2 & 1 <= j2 ) by A22, MATRIX_0:32;

A29: i2 <= len (Gauge (C,n)) by A22, MATRIX_0:32;

A30: i1 <= len (Gauge (C,n)) by A20, MATRIX_0:32;

A31: ( Center (Gauge (C,n)) <= len (Gauge (C,n)) & i1 + 1 >= 1 ) by JORDAN1B:13, NAT_1:11;

now :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2end;

hence
((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
; :: thesis: verumper cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A24;

end;

suppose
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

then ((Upper_Seq (C,n)) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A21, A25, A30, A26, GOBOARD5:2

.= ((Upper_Seq (C,n)) /. (k + 1)) `1 by A23, A29, A28, A27, GOBOARD5:2 ;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14; :: thesis: verum

end;.= ((Upper_Seq (C,n)) /. (k + 1)) `1 by A23, A29, A28, A27, GOBOARD5:2 ;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14; :: thesis: verum

suppose A32:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

then i1 + 1 <= Center (Gauge (C,n)) by NAT_1:13;

then ((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A23, A26, A7, A8, A31, A32, JORDAN1A:18;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A33, XXREAL_0:1; :: thesis: verum

end;

A33: now :: thesis: not ((Upper_Seq (C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

i1 < Center (Gauge (C,n))
by A6, A17, A21, A30, A26, A14, A7, A8, JORDAN1A:18, NAT_1:13, NAT_1:14;A34:
k + 1 >= 1 + 1
by A9, XREAL_1:7;

len (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) = (((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) -' 1) + 1 by A13, A18, JORDAN4:8

.= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) by A13, XREAL_1:235 ;

then A35: rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) c= L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) by A17, A34, SPPOL_2:18, XXREAL_0:2;

A36: (Upper_Seq (C,n)) /. ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A11, FINSEQ_5:38;

A39: ( Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is closed & L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) ) by A15, A10, JORDAN6:30, TOPREAL1:25;

First_Point ((L~ (Upper_Seq (C,n))),((Upper_Seq (C,n)) /. 1),((Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A1, A15, A10, Th47;

then A40: (L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))} by A15, A10, A39, A38, A37, Th50, JORDAN6:49;

A41: ( mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))) = (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) & (Upper_Seq (C,n)) | (Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))) = (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) ) by A13, FINSEQ_1:def 15, FINSEQ_6:116;

assume ((Upper_Seq (C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ; :: thesis: contradiction

then (Upper_Seq (C,n)) /. (k + 1) in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then A42: (Upper_Seq (C,n)) /. (k + 1) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

A43: k + 1 in dom (Upper_Seq (C,n)) by A16, A19, FINSEQ_3:25;

k + 1 in Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) by A16, A17, FINSEQ_1:1;

then (Upper_Seq (C,n)) /. (k + 1) in rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) by A41, A43, PARTFUN2:18;

then (Upper_Seq (C,n)) /. (k + 1) in {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))} by A42, A35, A40, XBOOLE_0:def 4;

then (Upper_Seq (C,n)) /. (k + 1) = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by TARSKI:def 1;

hence contradiction by A17, A12, A43, A36, PARTFUN2:10; :: thesis: verum

end;len (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) = (((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) -' 1) + 1 by A13, A18, JORDAN4:8

.= (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) by A13, XREAL_1:235 ;

then A35: rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) c= L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) by A17, A34, SPPOL_2:18, XXREAL_0:2;

A36: (Upper_Seq (C,n)) /. ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A11, FINSEQ_5:38;

A37: now :: thesis: not (Upper_Seq (C,n)) /. 1 in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)

A38:
( (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 & ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 )
by A3, A4, EUCLID:52;assume
(Upper_Seq (C,n)) /. 1 in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)
; :: thesis: contradiction

then (W-min (L~ (Cage (C,n)))) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A15, JORDAN6:31;

hence contradiction by A3, EUCLID:52; :: thesis: verum

end;then (W-min (L~ (Cage (C,n)))) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A15, JORDAN6:31;

hence contradiction by A3, EUCLID:52; :: thesis: verum

A39: ( Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is closed & L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) ) by A15, A10, JORDAN6:30, TOPREAL1:25;

First_Point ((L~ (Upper_Seq (C,n))),((Upper_Seq (C,n)) /. 1),((Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n)) by A1, A15, A10, Th47;

then A40: (L~ (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))} by A15, A10, A39, A38, A37, Th50, JORDAN6:49;

A41: ( mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))) = (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) & (Upper_Seq (C,n)) | (Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)))) = (Upper_Seq (C,n)) | ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) ) by A13, FINSEQ_1:def 15, FINSEQ_6:116;

assume ((Upper_Seq (C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ; :: thesis: contradiction

then (Upper_Seq (C,n)) /. (k + 1) in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 } ;

then A42: (Upper_Seq (C,n)) /. (k + 1) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by JORDAN6:def 6;

A43: k + 1 in dom (Upper_Seq (C,n)) by A16, A19, FINSEQ_3:25;

k + 1 in Seg ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) by A16, A17, FINSEQ_1:1;

then (Upper_Seq (C,n)) /. (k + 1) in rng (mid ((Upper_Seq (C,n)),1,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) by A41, A43, PARTFUN2:18;

then (Upper_Seq (C,n)) /. (k + 1) in {(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))))} by A42, A35, A40, XBOOLE_0:def 4;

then (Upper_Seq (C,n)) /. (k + 1) = First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by TARSKI:def 1;

hence contradiction by A17, A12, A43, A36, PARTFUN2:10; :: thesis: verum

then i1 + 1 <= Center (Gauge (C,n)) by NAT_1:13;

then ((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A23, A26, A7, A8, A31, A32, JORDAN1A:18;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A33, XXREAL_0:1; :: thesis: verum

suppose
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

then
i2 < i1
by NAT_1:13;

then ((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((Upper_Seq (C,n)) /. k) `1 by A21, A23, A30, A26, A28, A27, JORDAN1A:18;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14, XXREAL_0:2; :: thesis: verum

end;then ((Upper_Seq (C,n)) /. (k + 1)) `1 <= ((Upper_Seq (C,n)) /. k) `1 by A21, A23, A30, A26, A28, A27, JORDAN1A:18;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14, XXREAL_0:2; :: thesis: verum

suppose
( i1 = i2 & j1 = j2 + 1 )
; :: thesis: ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

then ((Upper_Seq (C,n)) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A21, A25, A30, A26, GOBOARD5:2

.= ((Upper_Seq (C,n)) /. (k + 1)) `1 by A23, A29, A28, A27, GOBOARD5:2 ;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14; :: thesis: verum

end;.= ((Upper_Seq (C,n)) /. (k + 1)) `1 by A23, A29, A28, A27, GOBOARD5:2 ;

hence ((Upper_Seq (C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A6, A17, NAT_1:13, NAT_1:14; :: thesis: verum

proof

A45:
for k being non zero Nat holds S
assume that

1 <= 1 and

1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;

hence ((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A3, EUCLID:52; :: thesis: verum

end;1 <= 1 and

1 < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;

hence ((Upper_Seq (C,n)) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A3, EUCLID:52; :: thesis: verum

let k be Nat; :: thesis: ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) implies ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 )

assume ( 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) ) ; :: thesis: ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

hence ((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A45; :: thesis: verum