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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

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

set LS = Lower_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 RLS = Rev (Lower_Seq (C,n));

set FiP = First_Point ((L~ (Rev (Lower_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)));

set LaP = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

A2: L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) by SPPOL_2:22;

A3: len (Rev (Lower_Seq (C,n))) = len (Lower_Seq (C,n)) by FINSEQ_5:def 3;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_Seq (C,n))) /. $1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 );

A4: rng (Rev (Lower_Seq (C,n))) = rng (Lower_Seq (C,n)) by FINSEQ_5:57;

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

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

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

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

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

let k be Nat; :: thesis: ( 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

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

for k being Nat st 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) holds

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

set LS = Lower_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 RLS = Rev (Lower_Seq (C,n));

set FiP = First_Point ((L~ (Rev (Lower_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)));

set LaP = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)));

A2: L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) by SPPOL_2:22;

A3: len (Rev (Lower_Seq (C,n))) = len (Lower_Seq (C,n)) by FINSEQ_5:def 3;

defpred S

A4: rng (Rev (Lower_Seq (C,n))) = rng (Lower_Seq (C,n)) by FINSEQ_5:57;

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

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

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

A8: for k being non zero Nat st S

S

proof

A52:
S
A9:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:21;

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

then A10: (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n))) by A9, JORDAN6:1;

then A11: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by EUCLID:52;

A12: (Rev (Lower_Seq (C,n))) /. (len (Rev (Lower_Seq (C,n)))) = (Lower_Seq (C,n)) /. 1 by A3, FINSEQ_5:65

.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;

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 A13: ( 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_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 A14: 1 <= width (Gauge (C,n)) by JORDAN8:def 1;

then A15: ((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 ;

A16: ( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by JORDAN1F:6, JORDAN1F:8;

then A17: L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))), W-min (L~ (Cage (C,n))) by TOPREAL1:25;

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

A19: (Rev (Lower_Seq (C,n))) /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by FINSEQ_5:65

.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;

L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by A16, JORDAN5B:14, TOPREAL1:25;

then ( L~ (Lower_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) & (L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is closed ) by A10, A11, JORDAN6:49;

then A20: First_Point ((L~ (Rev (Lower_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))) = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A2, A17, JORDAN5C:18;

then A21: (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) in dom (Rev (Lower_Seq (C,n))) by A1, A4, Th48, FINSEQ_4:20;

then A22: 1 <= (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) by FINSEQ_3:25;

A23: k >= 1 by NAT_1:14;

reconsider kk = k as Nat ;

assume that

A24: 1 <= k + 1 and

A25: k + 1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

A26: (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) <= len (Rev (Lower_Seq (C,n))) by A21, FINSEQ_3:25;

then A27: k + 1 <= len (Rev (Lower_Seq (C,n))) by A25, XXREAL_0:2;

Lower_Seq (C,n) is_sequence_on Gauge (C,n) by Th5;

then Rev (Lower_Seq (C,n)) is_sequence_on Gauge (C,n) by JORDAN9:5;

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

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

A29: (Rev (Lower_Seq (C,n))) /. kk = (Gauge (C,n)) * (i1,j1) and

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

A31: (Rev (Lower_Seq (C,n))) /. (kk + 1) = (Gauge (C,n)) * (i2,j2) and

A32: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A23, A27, JORDAN8:3;

A33: 1 <= i1 by A28, MATRIX_0:32;

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

A35: i2 <= len (Gauge (C,n)) by A30, MATRIX_0:32;

A36: i1 <= len (Gauge (C,n)) by A28, MATRIX_0:32;

A37: j2 <= width (Gauge (C,n)) by A30, MATRIX_0:32;

A38: ( 1 <= i2 & 1 <= j2 ) by A30, MATRIX_0:32;

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

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

then A10: (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52;

((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n))) by A9, JORDAN6:1;

then A11: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by EUCLID:52;

A12: (Rev (Lower_Seq (C,n))) /. (len (Rev (Lower_Seq (C,n)))) = (Lower_Seq (C,n)) /. 1 by A3, FINSEQ_5:65

.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;

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

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

assume A13: ( 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_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 A14: 1 <= width (Gauge (C,n)) by JORDAN8:def 1;

then A15: ((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 ;

A16: ( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by JORDAN1F:6, JORDAN1F:8;

then A17: L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))), W-min (L~ (Cage (C,n))) by TOPREAL1:25;

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

A19: (Rev (Lower_Seq (C,n))) /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by FINSEQ_5:65

.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;

L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by A16, JORDAN5B:14, TOPREAL1:25;

then ( L~ (Lower_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) & (L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is closed ) by A10, A11, JORDAN6:49;

then A20: First_Point ((L~ (Rev (Lower_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))) = Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) by A2, A17, JORDAN5C:18;

then A21: (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) in dom (Rev (Lower_Seq (C,n))) by A1, A4, Th48, FINSEQ_4:20;

then A22: 1 <= (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) by FINSEQ_3:25;

A23: k >= 1 by NAT_1:14;

reconsider kk = k as Nat ;

assume that

A24: 1 <= k + 1 and

A25: k + 1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

A26: (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) <= len (Rev (Lower_Seq (C,n))) by A21, FINSEQ_3:25;

then A27: k + 1 <= len (Rev (Lower_Seq (C,n))) by A25, XXREAL_0:2;

Lower_Seq (C,n) is_sequence_on Gauge (C,n) by Th5;

then Rev (Lower_Seq (C,n)) is_sequence_on Gauge (C,n) by JORDAN9:5;

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

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

A29: (Rev (Lower_Seq (C,n))) /. kk = (Gauge (C,n)) * (i1,j1) and

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

A31: (Rev (Lower_Seq (C,n))) /. (kk + 1) = (Gauge (C,n)) * (i2,j2) and

A32: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A23, A27, JORDAN8:3;

A33: 1 <= i1 by A28, MATRIX_0:32;

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

A35: i2 <= len (Gauge (C,n)) by A30, MATRIX_0:32;

A36: i1 <= len (Gauge (C,n)) by A28, MATRIX_0:32;

A37: j2 <= width (Gauge (C,n)) by A30, MATRIX_0:32;

A38: ( 1 <= i2 & 1 <= j2 ) by A30, MATRIX_0:32;

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

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

hence
((Rev (Lower_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 A32;

end;

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

then ((Rev (Lower_Seq (C,n))) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A29, A33, A36, A34, GOBOARD5:2

.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:2 ;

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

end;.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:2 ;

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

suppose A40:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: ((Rev (Lower_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 ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A31, A34, A14, A15, A39, A40, JORDAN1A:18;

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

end;

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

then (Rev (Lower_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 A43: (Rev (Lower_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;

A44: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by A7, EUCLID:52;

( L~ (Rev (Lower_Seq (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) & (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ) by A6, A19, A12, EUCLID:52, TOPREAL1:25;

then A45: L~ (Rev (Lower_Seq (C,n))) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A44, JORDAN6:49;

A46: (Rev (Lower_Seq (C,n))) /. ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) = First_Point ((L~ (Rev (Lower_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 A1, A4, A20, Th48, FINSEQ_5:38;

A47: k + 1 >= 1 + 1 by A23, XREAL_1:7;

len (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) = (((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) -' 1) + 1 by A22, A26, JORDAN4:8

.= (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) by A22, XREAL_1:235 ;

then A48: rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) c= L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) by A25, A47, SPPOL_2:18, XXREAL_0:2;

A49: k + 1 in dom (Rev (Lower_Seq (C,n))) by A24, A27, FINSEQ_3:25;

( Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is closed & Rev (Lower_Seq (C,n)) is being_S-Seq ) by JORDAN6:30;

then A50: (L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Rev (Lower_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 A1, A4, A20, A19, A12, A45, A42, Th48, Th50;

A51: ( mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))) = (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) & (Rev (Lower_Seq (C,n))) | (Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))) = (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) ) by A22, FINSEQ_1:def 15, FINSEQ_6:116;

k + 1 in Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) by A24, A25, FINSEQ_1:1;

then (Rev (Lower_Seq (C,n))) /. (k + 1) in rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) by A51, A49, PARTFUN2:18;

then (Rev (Lower_Seq (C,n))) /. (k + 1) in {(First_Point ((L~ (Rev (Lower_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 A43, A48, A50, XBOOLE_0:def 4;

then (Rev (Lower_Seq (C,n))) /. (k + 1) = First_Point ((L~ (Rev (Lower_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 A25, A21, A49, A46, PARTFUN2:10; :: thesis: verum

end;

i1 < Center (Gauge (C,n))
by A13, A25, A29, A36, A34, A18, A14, A15, JORDAN1A:18, NAT_1:13, NAT_1:14;A42: now :: thesis: not (Rev (Lower_Seq (C,n))) /. 1 in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)

assume
((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
; :: thesis: contradictionassume
(Rev (Lower_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 A19, JORDAN6:31;

hence contradiction by A6, 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 A19, JORDAN6:31;

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

then (Rev (Lower_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 A43: (Rev (Lower_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;

A44: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by A7, EUCLID:52;

( L~ (Rev (Lower_Seq (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) & (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ) by A6, A19, A12, EUCLID:52, TOPREAL1:25;

then A45: L~ (Rev (Lower_Seq (C,n))) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) by A44, JORDAN6:49;

A46: (Rev (Lower_Seq (C,n))) /. ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) = First_Point ((L~ (Rev (Lower_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 A1, A4, A20, Th48, FINSEQ_5:38;

A47: k + 1 >= 1 + 1 by A23, XREAL_1:7;

len (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) = (((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) -' 1) + 1 by A22, A26, JORDAN4:8

.= (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) by A22, XREAL_1:235 ;

then A48: rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) c= L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) by A25, A47, SPPOL_2:18, XXREAL_0:2;

A49: k + 1 in dom (Rev (Lower_Seq (C,n))) by A24, A27, FINSEQ_3:25;

( Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) is closed & Rev (Lower_Seq (C,n)) is being_S-Seq ) by JORDAN6:30;

then A50: (L~ (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) = {(First_Point ((L~ (Rev (Lower_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 A1, A4, A20, A19, A12, A45, A42, Th48, Th50;

A51: ( mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))) = (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) & (Rev (Lower_Seq (C,n))) | (Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))))) = (Rev (Lower_Seq (C,n))) | ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) ) by A22, FINSEQ_1:def 15, FINSEQ_6:116;

k + 1 in Seg ((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))) by A24, A25, FINSEQ_1:1;

then (Rev (Lower_Seq (C,n))) /. (k + 1) in rng (mid ((Rev (Lower_Seq (C,n))),1,((First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n)))))) by A51, A49, PARTFUN2:18;

then (Rev (Lower_Seq (C,n))) /. (k + 1) in {(First_Point ((L~ (Rev (Lower_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 A43, A48, A50, XBOOLE_0:def 4;

then (Rev (Lower_Seq (C,n))) /. (k + 1) = First_Point ((L~ (Rev (Lower_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 A25, A21, A49, A46, PARTFUN2:10; :: thesis: verum

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

then ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by A31, A34, A14, A15, A39, A40, JORDAN1A:18;

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

suppose
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: ((Rev (Lower_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 ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((Rev (Lower_Seq (C,n))) /. k) `1 by A29, A31, A36, A34, A38, A37, JORDAN1A:18;

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

end;then ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 <= ((Rev (Lower_Seq (C,n))) /. k) `1 by A29, A31, A36, A34, A38, A37, JORDAN1A:18;

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

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

then ((Rev (Lower_Seq (C,n))) /. k) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A29, A33, A36, A34, GOBOARD5:2

.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:2 ;

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

end;.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:2 ;

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

proof

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

1 <= 1 and

1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

(Rev (Lower_Seq (C,n))) /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by FINSEQ_5:65

.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;

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

end;1 <= 1 and

1 < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. 1) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

(Rev (Lower_Seq (C,n))) /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by FINSEQ_5:65

.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;

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

let k be Nat; :: thesis: ( 1 <= k & k < (First_Point ((L~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) implies ((Rev (Lower_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~ (Rev (Lower_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)))) .. (Rev (Lower_Seq (C,n))) ) ; :: thesis: ((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2

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