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<sub>1</sub>[ 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₁[k] holds
S₁[k + 1]

proof

set GC1 = (Gauge (C,n)) * ((Center (Gauge (C,n))),1);
let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[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<sub>1</sub>[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;

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

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

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;

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

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

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, FINSEQ_6:186
.= (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)

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;

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;
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 16, 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;

i1 < Center (Gauge (C,n)) by A6, A17, A21, A30, A26, A14, A7, A8, JORDAN1A:18, NAT_1:13, NAT_1:14;
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;

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;

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;

end;

end;

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

end;

A44: S₁[1]

proof

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;

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