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 q being Point of (TOP-REAL 2) st q in rng (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) holds
q `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 q being Point of (TOP-REAL 2) st q in rng (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) holds
q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 )
assume A1:
n > 0
; :: thesis: for q being Point of (TOP-REAL 2) st q in rng (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) holds
q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
let q be Point of (TOP-REAL 2); :: thesis: ( q in rng (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) implies q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 )
set Wmin = W-min (L~ (Cage C,n));
set Emax = E-max (L~ (Cage C,n));
set Wbo = W-bound (L~ (Cage C,n));
set Ebo = E-bound (L~ (Cage C,n));
set sr = ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2;
set US = Upper_Seq 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));
assume
q in rng (mid (Upper_Seq 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))) .. (Upper_Seq C,n)))
; :: thesis: q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
then consider k being Element of NAT such that
A2:
k in dom (mid (Upper_Seq 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))) .. (Upper_Seq C,n)))
and
A3:
q = (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) /. k
by PARTFUN2:4;
A4:
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, Th55;
then A5:
(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:30;
then A6:
( 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) <= len (Upper_Seq C,n) )
by FINSEQ_3:27;
A7:
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n))
by JORDAN1F:5;
then A8:
W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n)
by FINSEQ_6:46;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n))
by JORDAN1F:7;
then A9:
L~ (Upper_Seq C,n) is_an_arc_of W-min (L~ (Cage C,n)), E-max (L~ (Cage C,n))
by A7, TOPREAL1:31;
W-bound (L~ (Cage C,n)) < E-bound (L~ (Cage C,n))
by SPRECT_1:33;
then A10:
( W-bound (L~ (Cage C,n)) < ((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-bound (L~ (Cage C,n)) )
by XREAL_1:228;
then
( (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 EUCLID:56;
then
( L~ (Upper_Seq C,n) meets Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2) & (L~ (Upper_Seq C,n)) /\ (Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2)) is closed )
by A9, JORDAN6:64;
then
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 (L~ (Upper_Seq C,n)) /\ (Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))
by A9, JORDAN5C:def 1;
then
( 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 L~ (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)) in Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2) )
by XBOOLE_0:def 4;
then 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))) `1 = ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
by JORDAN6:34;
now assume
(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
;
:: thesis: contradictionthen (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) /. 1) .. (Upper_Seq C,n)
by FINSEQ_6:47
.=
(W-min (L~ (Cage C,n))) .. (Upper_Seq C,n)
by JORDAN1F:5
;
then
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)) = W-min (L~ (Cage C,n))
by A4, A8, FINSEQ_5:10;
hence
contradiction
by A10, A11, EUCLID:56;
:: thesis: verum end;
then
(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
by A6, XXREAL_0:1;
then A12:
(1 + 1) + 0 <= (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 NAT_1:13;
k + 2 >= 1 + 1
by NAT_1:11;
then A13:
(k + 2) - 1 >= (1 + 1) - 1
by XREAL_1:11;
len (Upper_Seq C,n) >= 3
by JORDAN1E:19;
then
len (Upper_Seq C,n) >= 2
by XXREAL_0:2;
then
2 in dom (Upper_Seq C,n)
by FINSEQ_3:27;
then A14: (mid (Upper_Seq 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))) .. (Upper_Seq C,n))) /. k =
(Upper_Seq C,n) /. ((k + 2) -' 1)
by A2, A5, A12, SPRECT_2:7
.=
(Upper_Seq C,n) /. (k + (2 - 1))
by A13, XREAL_0:def 2
;
A15:
k <= len (mid (Upper_Seq 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))) .. (Upper_Seq C,n)))
by A2, FINSEQ_3:27;
((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)) - 2 >= 0
by A12, XREAL_1:21;
then
((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)) -' 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))) .. (Upper_Seq C,n)) - 2
by XREAL_0:def 2;
then
len (mid (Upper_Seq 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))) .. (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)) - 2) + 1
by A6, A12, JORDAN4:20;
then
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)) - 2) + 1) + 1
by A15, NAT_1:13;
then A16:
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)
by NAT_1:13;
per cases
( 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) or 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) )
by A16, XXREAL_0:1;
suppose
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: q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2end; suppose
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: q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2end;