let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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 ; ( 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
; 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 S1[ 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 S1[k] holds
S1[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;
( S1[k] implies S1[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 )
;
S1[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))
;
((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 )
;
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2then ((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;
verum end; suppose A40:
(
i1 + 1
= i2 &
j1 = j2 )
;
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2A41:
now assume
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 = ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
;
contradictionthen
(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, SPPOL_2:47, 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, SPPOL_2:47;
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, JORDAN3:25;
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;
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;
verum suppose
(
i1 = i2 + 1 &
j1 = j2 )
;
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2then
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;
verum end; suppose
(
i1 = i2 &
j1 = j2 + 1 )
;
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2then ((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;
verum end;
hence
((Rev (Lower_Seq C,n)) /. (k + 1)) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
;
verum
end;
A52:
S1[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))
;
((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;
verum
end;
A53:
for k being non empty Nat holds S1[k]
from NAT_1:sch 10(A52, A8);
let k be Nat; ( 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)) )
; ((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; verum