let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of 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 Element of 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<sub>1</sub>[ 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:60;
A5: W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n))) by SPRECT_1:33;
then A6: W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by XREAL_1:228;
A7: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n))) by A5, XREAL_1:228;
A8: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

A9: W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n))) by SPRECT_1:23;
then W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN6:2;
then A10: (W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by EUCLID:56;
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n))) by A9, JORDAN6:2;
then A11: ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1 by EUCLID:56;
A12: (Rev (Lower_Seq (C,n))) /. (len (Rev (Lower_Seq (C,n)))) = (Lower_Seq (C,n)) /. 1 by A3, FINSEQ_5:68
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
set GC1 = (Gauge (C,n)) * ((Center (Gauge (C,n))),1);
let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[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<sub>1</sub>[k + 1]
4 <= len (Gauge (C,n)) by JORDAN8:13;
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, Th43
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by Th41 ;
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:31;
A18: 1 <= Center (Gauge (C,n)) by JORDAN1B:12;
A19: (Rev (Lower_Seq (C,n))) /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by FINSEQ_5:68
.= 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:31;
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:64;
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, Th56, FINSEQ_4:30;
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:27;
A23: k >= 1 by NAT_1:14;
reconsider kk = k as Element of NAT by ORDINAL1:def 13;
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:27;
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:7;
then consider i1, j1, i2, j2 being Element of 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:6;
A33: 1 <= i1 by A28, MATRIX_1:39;
A34: ( 1 <= j1 & j1 <= width (Gauge (C,n)) ) by A28, MATRIX_1:39;
A35: i2 <= len (Gauge (C,n)) by A30, MATRIX_1:39;
A36: i1 <= len (Gauge (C,n)) by A28, MATRIX_1:39;
A37: j2 <= width (Gauge (C,n)) by A30, MATRIX_1:39;
A38: ( 1 <= i2 & 1 <= j2 ) by A30, MATRIX_1:39;
A39: ( Center (Gauge (C,n)) <= len (Gauge (C,n)) & i1 + 1 >= 1 ) by JORDAN1B:14, NAT_1:11;

now

per 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;

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:3
.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:3 ;
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;

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

A41: now

A42: now

assume (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:34;
hence contradiction by A6, EUCLID:56; :: thesis: verum

end;

assume ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 ; :: thesis: contradiction
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:56;
( 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:56, TOPREAL1:31;
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:64;
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, Th56, FINSEQ_5:41;
A47: k + 1 >= 1 + 1 by A23, XREAL_1:9;
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:20
.= (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:237 ;
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:27;
( 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:33;
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, Th56, Th58;
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:122;
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:3;
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:36;
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:17; :: thesis: verum

end;

i1 < Center (Gauge (C,n)) by A13, A25, A29, A36, A34, A18, A14, A15, JORDAN1A:39, NAT_1:13, NAT_1:14;
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:39;
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;

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:39;
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;

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:3
.= ((Rev (Lower_Seq (C,n))) /. (k + 1)) `1 by A31, A35, A38, A37, GOBOARD5:3 ;
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;

end;

end;

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

end;

A52: S₁[1]

proof

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:68
.= 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:56; :: thesis: verum

end;

A53: for k being non empty Nat holds S₁[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