let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being 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 Nat; ( 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 )
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)));
A1:
(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
then A2:
L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n)))
by A1, TOPREAL1:25;
assume A3:
n > 0
; 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
then 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 Th47;
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:20;
then A6:
(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:25;
A7:
W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n)))
by SPRECT_1:31;
then A8:
W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by XREAL_1:226;
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n)))
by A7, XREAL_1:226;
then A9:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1
by EUCLID:52;
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A8, EUCLID:52;
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 A2, A9, JORDAN6:49;
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 A2, 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 Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)
by XBOOLE_0:def 4;
then A10:
(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:31;
A11:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A1, FINSEQ_6:42;
A12:
now not (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)) = 1assume
(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
;
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:43
.=
(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, A11, FINSEQ_5:9;
hence
contradiction
by A8, A10, EUCLID:52;
verum end;
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 A5, FINSEQ_3:25;
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 A12, XXREAL_0:1;
then A13:
(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;
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 >= 0
by XREAL_1:19;
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 A14:
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, A13, FINSEQ_6:186;
let q be Point of (TOP-REAL 2); ( 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 )
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)))))
; q `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
then consider k being Element of NAT such that
A15:
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
A16:
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:2;
k + 2 >= 1 + 1
by NAT_1:11;
then A17:
(k + 2) - 1 >= (1 + 1) - 1
by XREAL_1:9;
len (Upper_Seq (C,n)) >= 3
by JORDAN1E:15;
then
len (Upper_Seq (C,n)) >= 2
by XXREAL_0:2;
then
2 in dom (Upper_Seq (C,n))
by FINSEQ_3:25;
then A18: (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 A15, A5, A13, SPRECT_2:3
.=
(Upper_Seq (C,n)) /. (k + (2 - 1))
by A17, XREAL_0:def 2
;
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 A15, FINSEQ_3:25;
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 A14, NAT_1:13;
then A19:
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 A19, 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))
;
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))
;
q `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2end;