let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat st n > 0 holds
(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)))) `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)))) `2
let n be Nat; ( n > 0 implies (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)))) `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)))) `2 )
set sr = ((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 Nbo = N-bound (L~ (Cage (C,n)));
set Ebo = E-bound (L~ (Cage (C,n)));
set Sbo = S-bound (L~ (Cage (C,n)));
set Wbo = W-bound (L~ (Cage (C,n)));
set SW = SW-corner (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)));
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)));
set g = (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))))) ^ <*|[(E-bound (L~ (Cage (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)))) `2)]|*>;
set h = (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>;
A1:
(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
A2:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:21;
then
W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN6:1;
then A3:
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by EUCLID:52;
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n)))
by A2, JORDAN6:1;
then A4:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1
by EUCLID:52;
set GCw = (Gauge (C,n)) * ((Center (Gauge (C,n))),(width (Gauge (C,n))));
A5:
1 <= Center (Gauge (C,n))
by JORDAN1B:11;
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
then A6:
((Gauge (C,n)) * ((Center (Gauge (C,n))),(width (Gauge (C,n))))) `2 = N-bound (L~ (Cage (C,n)))
by A5, JORDAN1A:70, JORDAN1B:13;
A7:
(SW-corner (L~ (Cage (C,n)))) `2 <= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:30;
A8:
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
set RevL = (Rev (Lower_Seq (C,n))) -: (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))));
A9:
( <*|[(E-bound (L~ (Cage (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)))) `2)]|*> is one-to-one & <*|[(E-bound (L~ (Cage (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)))) `2)]|*> is special )
by FINSEQ_3:93;
A10:
rng ((Rev (Lower_Seq (C,n))) -: (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))))) c= rng (Rev (Lower_Seq (C,n)))
by FINSEQ_5:48;
A11:
( (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 A12:
L~ (Lower_Seq (C,n)) is_an_arc_of E-max (L~ (Cage (C,n))), W-min (L~ (Cage (C,n)))
by TOPREAL1:25;
A13:
4 <= len (Gauge (C,n))
by JORDAN8:10;
then A14:
len (Gauge (C,n)) >= 3
by XXREAL_0:2;
A15:
W-bound (L~ (Cage (C,n))) < E-bound (L~ (Cage (C,n)))
by SPRECT_1:31;
then A16:
W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by XREAL_1:226;
L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n)))
by A11, JORDAN5B:14, TOPREAL1:25;
then A17:
( 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 A3, A4, JORDAN6:49;
then A18:
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))) in (L~ (Lower_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))
by A12, JORDAN5C:def 2;
then A19:
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))) in L~ (Lower_Seq (C,n))
by XBOOLE_0:def 4;
then
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))) in (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
by XBOOLE_0:def 3;
then A20:
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))) in L~ (Cage (C,n))
by JORDAN1E:13;
assume A21:
n > 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)))) `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)))) `2
then A22:
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 A23:
(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 A24:
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;
1 <= len (Gauge (C,n))
by A13, XXREAL_0:2;
then
1 <= width (Gauge (C,n))
by JORDAN8:def 1;
then ((Gauge (C,n)) * ((Center (Gauge (C,n))),(width (Gauge (C,n))))) `1 =
((W-bound C) + (E-bound C)) / 2
by A21, Th35
.=
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by Th33
;
then
(Gauge (C,n)) * ((Center (Gauge (C,n))),(width (Gauge (C,n)))) = |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|
by A6, EUCLID:53;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in rng (Lower_Seq (C,n))
by A5, A14, Th43, JORDAN1B:15;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in rng (Rev (Lower_Seq (C,n)))
by FINSEQ_5:57;
then A25:
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in rng ((Rev (Lower_Seq (C,n))) -: (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 A10;
(SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| <> SW-corner (L~ (Cage (C,n)))
by A8, SPRECT_1:32;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in {(SW-corner (L~ (Cage (C,n))))}
by TARSKI:def 1;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in rng <*(SW-corner (L~ (Cage (C,n))))*>
by FINSEQ_1:38;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in (rng <*(SW-corner (L~ (Cage (C,n))))*>) \/ (rng ((Rev (Lower_Seq (C,n))) -: (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 A25, XBOOLE_0:def 3;
then
not |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| in rng (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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 FINSEQ_1:31;
then
rng (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) misses {|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|}
by ZFMISC_1:50;
then
(rng (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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))))))) /\ {|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|} = {}
;
then
(rng (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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))))))) /\ (rng <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) = {}
by FINSEQ_1:38;
then A26:
rng (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) misses rng <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>
;
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))) in rng (Lower_Seq (C,n))
by A21, Th48;
then A27:
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))) in rng (Rev (Lower_Seq (C,n)))
by FINSEQ_5:57;
then A28:
not (Rev (Lower_Seq (C,n))) -: (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)))) is empty
by FINSEQ_5:47;
A29:
len ((Rev (Lower_Seq (C,n))) -: (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))))) = (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)))) .. (Rev (Lower_Seq (C,n)))
by A27, FINSEQ_5:42;
A30:
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
then A31:
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;
A32:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n)))
by A15, XREAL_1:226;
then A33:
((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 A16, 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 A31, A33, JORDAN6:49;
then A34:
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 A31, JORDAN5C:def 1;
then A35:
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))
by XBOOLE_0:def 4;
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))) \/ (L~ (Lower_Seq (C,n)))
by XBOOLE_0:def 3;
then A36:
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~ (Cage (C,n))
by JORDAN1E:13;
now for m being Nat st m in dom <*|[(E-bound (L~ (Cage (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)))) `2)]|*> holds
( W-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*|[(E-bound (L~ (Cage (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)))) `2)]|*> implies ( W-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )assume
m in dom <*|[(E-bound (L~ (Cage (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)))) `2)]|*>
;
( W-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A37:
<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m = |[(E-bound (L~ (Cage (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)))) `2)]|
by FINSEQ_4:16;
then
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
hence
(
W-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 &
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) )
by SPRECT_1:21;
( S-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 & (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `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)))) `2
by A37, EUCLID:52;
hence
(
S-bound (L~ (Cage (C,n))) <= (<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 &
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
by A36, PSCOMP_1:24;
verum end;
then A38:
<*|[(E-bound (L~ (Cage (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)))) `2)]|*> is_in_the_area_of Cage (C,n)
by SPRECT_2:def 1;
A39:
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 A34, XBOOLE_0:def 4;
then A40:
(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;
now not (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)))))) /\ {|[(E-bound (L~ (Cage (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)))) `2)]|} <> {} assume
(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)))))) /\ {|[(E-bound (L~ (Cage (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)))) `2)]|} <> {}
;
contradictionthen consider x being
object such that A41:
x 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)))))) /\ {|[(E-bound (L~ (Cage (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)))) `2)]|}
by XBOOLE_0:def 1;
(
x 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))))) &
x in {|[(E-bound (L~ (Cage (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)))) `2)]|} )
by A41, XBOOLE_0:def 4;
then
|[(E-bound (L~ (Cage (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)))) `2)]| 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)))))
by TARSKI:def 1;
then
|[(E-bound (L~ (Cage (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)))) `2)]| `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, Th53;
hence
contradiction
by A32, EUCLID:52;
verum end;
then
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))))) misses {|[(E-bound (L~ (Cage (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)))) `2)]|}
;
then A42:
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))))) misses rng <*|[(E-bound (L~ (Cage (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)))) `2)]|*>
by FINSEQ_1:38;
A43:
(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 A23, FINSEQ_3:25;
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))) in Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)
by A18, XBOOLE_0:def 4;
then A44:
(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)))) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN6:31;
A45:
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)))) `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)))) `2 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)))) `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)))) `2
;
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)))
= 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 A40, A44, TOPREAL3:6;
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))) /\ (L~ (Lower_Seq (C,n)))
by A35, A19, XBOOLE_0:def 4;
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 {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
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))) or
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)))
= E-max (L~ (Cage (C,n))) )
by TARSKI:def 2;
hence
contradiction
by A16, A32, A40, EUCLID:52;
verum end;
len (Upper_Seq (C,n)) >= 3
by JORDAN1E:15;
then A46:
len (Upper_Seq (C,n)) > 2
by XXREAL_0:2;
then A47:
2 in dom (Upper_Seq (C,n))
by FINSEQ_3:25;
then A48: ((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))))) /. (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))))))) `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
by A23, SPRECT_2:9
.=
(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)))) `2
by A22, FINSEQ_5:38
.=
|[(E-bound (L~ (Cage (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)))) `2)]| `2
by EUCLID:52
.=
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. 1) `2
by FINSEQ_4:16
;
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))
proof
assume
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))
;
contradiction
then
(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)))
by A22, FINSEQ_5:38;
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)))) `1 = W-bound (L~ (Cage (C,n)))
by Th31;
then
W-bound (L~ (Cage (C,n))) = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A39, JORDAN6:31;
hence
contradiction
by SPRECT_1:31;
verum
end;
then
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)))) is being_S-Seq
by A46, A24, A43, JORDAN3:6;
then reconsider g = (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))))) ^ <*|[(E-bound (L~ (Cage (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)))) `2)]|*> as one-to-one special FinSequence of (TOP-REAL 2) by A42, A48, A9, FINSEQ_3:91, GOBOARD2:8;
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)))) is_in_the_area_of Cage (C,n)
by A47, A23, JORDAN1E:17, SPRECT_2:22;
then A49:
g is_in_the_area_of Cage (C,n)
by A38, SPRECT_2:24;
A50: (g /. (len g)) `1 =
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. (len <*|[(E-bound (L~ (Cage (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)))) `2)]|*>)) `1
by SPRECT_3:1
.=
(<*|[(E-bound (L~ (Cage (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)))) `2)]|*> /. 1) `1
by FINSEQ_1:39
.=
|[(E-bound (L~ (Cage (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)))) `2)]| `1
by FINSEQ_4:16
.=
E-bound (L~ (Cage (C,n)))
by EUCLID:52
;
A51:
1 <= 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 A47, A23, SPRECT_2:5;
then
1 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)))))
by FINSEQ_3:25;
then (g /. 1) `1 =
((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))))) /. 1) `1
by FINSEQ_4:68
.=
((Upper_Seq (C,n)) /. 2) `1
by A47, A23, SPRECT_2:8
.=
W-bound (L~ (Cage (C,n)))
by Th31
;
then A52:
g is_a_h.c._for Cage (C,n)
by A49, A50, SPRECT_2:def 2;
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)))) `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)))) `2
; contradiction
then A53:
(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)))) `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)))) `2
by A45, XXREAL_0:1;
A54:
rng (Lower_Seq (C,n)) c= rng (Cage (C,n))
by Th39;
now contradictionper cases
( SW-corner (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n))) or SW-corner (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n))) )
;
suppose A55:
SW-corner (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
;
contradiction
not
SW-corner (L~ (Cage (C,n))) in rng (Lower_Seq (C,n))
proof
(SW-corner (L~ (Cage (C,n)))) `1 = (W-min (L~ (Cage (C,n)))) `1
by PSCOMP_1:29;
then A56:
(SW-corner (L~ (Cage (C,n)))) `2 <> (W-min (L~ (Cage (C,n)))) `2
by A55, TOPREAL3:6;
assume
SW-corner (L~ (Cage (C,n))) in rng (Lower_Seq (C,n))
;
contradiction
then A57:
SW-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
by A54;
len (Cage (C,n)) > 4
by GOBOARD7:34;
then A58:
rng (Cage (C,n)) c= L~ (Cage (C,n))
by SPPOL_2:18, XXREAL_0:2;
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
SW-corner (L~ (Cage (C,n))) in W-most (L~ (Cage (C,n)))
by A57, A58, SPRECT_2:12;
then
(W-min (L~ (Cage (C,n)))) `2 <= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:31;
hence
contradiction
by A7, A56, XXREAL_0:1;
verum
end; then
not
SW-corner (L~ (Cage (C,n))) in rng (Rev (Lower_Seq (C,n)))
by FINSEQ_5:57;
then
not
SW-corner (L~ (Cage (C,n))) in rng ((Rev (Lower_Seq (C,n))) -: (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 A10;
then
{(SW-corner (L~ (Cage (C,n))))} misses rng ((Rev (Lower_Seq (C,n))) -: (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 ZFMISC_1:50;
then
{(SW-corner (L~ (Cage (C,n))))} /\ (rng ((Rev (Lower_Seq (C,n))) -: (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)))))) = {}
;
then
(rng <*(SW-corner (L~ (Cage (C,n))))*>) /\ (rng ((Rev (Lower_Seq (C,n))) -: (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 FINSEQ_1:38;
then A59:
rng <*(SW-corner (L~ (Cage (C,n))))*> misses rng ((Rev (Lower_Seq (C,n))) -: (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)))))
;
<*(SW-corner (L~ (Cage (C,n))))*> is
one-to-one
by FINSEQ_3:93;
then A60:
<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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))))) is
one-to-one
by A59, FINSEQ_3:91;
set FiP2 =
First_Point (
(L~ (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 midU =
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))));
reconsider RevLS =
Rev (Lower_Seq (C,n)) as
special FinSequence of
(TOP-REAL 2) ;
(<*(SW-corner (L~ (Cage (C,n))))*> /. (len <*(SW-corner (L~ (Cage (C,n))))*>)) `1 =
(<*(SW-corner (L~ (Cage (C,n))))*> /. 1) `1
by FINSEQ_1:39
.=
(SW-corner (L~ (Cage (C,n)))) `1
by FINSEQ_4:16
.=
W-bound (L~ (Cage (C,n)))
by EUCLID:52
.=
(W-min (L~ (Cage (C,n)))) `1
by EUCLID:52
.=
((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1
by JORDAN1F:8
.=
((Rev (Lower_Seq (C,n))) /. 1) `1
by FINSEQ_5:65
.=
(((Rev (Lower_Seq (C,n))) -: (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))))) /. 1) `1
by A27, FINSEQ_5:44
;
then A61:
<*(SW-corner (L~ (Cage (C,n))))*> ^ (RevLS -: (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))))) is
special
by GOBOARD2:8;
not
(Rev (Lower_Seq (C,n))) -: (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)))) is
empty
by A27, FINSEQ_5:47;
then A62:
((<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) /. (len (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))))) `1 =
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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))))))) `1
by SPRECT_3:1
.=
(((Rev (Lower_Seq (C,n))) -: (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))))) /. ((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)))) .. (Rev (Lower_Seq (C,n))))) `1
by A27, FINSEQ_5:42
.=
(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)))) `1
by A27, FINSEQ_5:45
.=
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:52
.=
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. 1) `1
by FINSEQ_4:16
;
(
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is
one-to-one &
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is
special )
by FINSEQ_3:93;
then reconsider h =
(<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> as
one-to-one special FinSequence of
(TOP-REAL 2) by A26, A60, A62, A61, FINSEQ_3:91, GOBOARD2:8;
A63:
|[(E-bound (L~ (Cage (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)))) `2)]| `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
now for m being Nat st m in dom <*(SW-corner (L~ (Cage (C,n))))*> holds
( W-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*(SW-corner (L~ (Cage (C,n))))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )assume
m in dom <*(SW-corner (L~ (Cage (C,n))))*>
;
( W-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A64:
<*(SW-corner (L~ (Cage (C,n))))*> /. m = SW-corner (L~ (Cage (C,n)))
by FINSEQ_4:16;
then
(<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
hence
(
W-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 &
(<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) )
by SPRECT_1:21;
( S-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 & (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 = S-bound (L~ (Cage (C,n)))
by A64, EUCLID:52;
hence
(
S-bound (L~ (Cage (C,n))) <= (<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 &
(<*(SW-corner (L~ (Cage (C,n))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
by SPRECT_1:22;
verum end; then A65:
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
A66:
((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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)))))) =
((Rev (Lower_Seq (C,n))) -: (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))))) /. ((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)))) .. (Rev (Lower_Seq (C,n))))
by A27, FINSEQ_5:42
.=
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 A27, FINSEQ_5:45
;
now for m being Nat st m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> holds
( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> implies ( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )A67:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:21;
assume
m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>
;
( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A68:
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m = |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|
by FINSEQ_4:16;
then
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by EUCLID:52;
hence
(
W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 &
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) )
by A67, JORDAN6:1;
( S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 = N-bound (L~ (Cage (C,n)))
by A68, EUCLID:52;
hence
(
S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 &
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
by SPRECT_1:22;
verum end; then A69:
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
A70:
(
L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) &
First_Point (
(L~ (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 A12, A17, JORDAN5C:18, SPPOL_2:22;
Rev (Lower_Seq (C,n)) is_in_the_area_of Cage (
C,
n)
by JORDAN1E:18, SPRECT_3:51;
then
(Rev (Lower_Seq (C,n))) -: (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)))) is_in_the_area_of Cage (
C,
n)
by A27, JORDAN1E:1;
then
<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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))))) is_in_the_area_of Cage (
C,
n)
by A65, SPRECT_2:24;
then A71:
h is_in_the_area_of Cage (
C,
n)
by A69, SPRECT_2:24;
len (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) = 1
+ (len ((Rev (Lower_Seq (C,n))) -: (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 FINSEQ_5:8;
then A72:
len (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) >= 1
by NAT_1:11;
1
in dom h
by FINSEQ_5:6;
then
h /. 1
= h . 1
by PARTFUN1:def 6;
then A73:
(h /. 1) `2 =
((<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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)))))) /. 1) `2
by A72, FINSEQ_6:109
.=
(SW-corner (L~ (Cage (C,n)))) `2
by FINSEQ_5:15
.=
S-bound (L~ (Cage (C,n)))
by EUCLID:52
;
A74:
len h = (len (<*(SW-corner (L~ (Cage (C,n))))*> ^ ((Rev (Lower_Seq (C,n))) -: (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))))))) + 1
by FINSEQ_2:16;
then A75:
1
+ 1
<= len h
by A72, XREAL_1:7;
L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
by JORDAN1E:13;
then A76:
L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n))
by XBOOLE_1:7;
A77:
(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))))) /. (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)))))) =
(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 A47, A23, SPRECT_2:9
.=
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 A22, FINSEQ_5:38
;
A78:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A1, FINSEQ_6:42;
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 A22, A78, FINSEQ_5:9;
hence
contradiction
by A16, A40, EUCLID:52;
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 A24, XXREAL_0:1;
then A79:
(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 A80:
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 A43, A79, JORDAN4:8
.=
((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
in dom ((Rev (Lower_Seq (C,n))) -: (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 A28, FINSEQ_5:6;
then A81:
(((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) /. 1 =
((Rev (Lower_Seq (C,n))) -: (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))))) /. 1
by FINSEQ_4:68
.=
(Rev (Lower_Seq (C,n))) /. 1
by A27, FINSEQ_5:44
.=
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by FINSEQ_5:65
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
A82:
(SW-corner (L~ (Cage (C,n)))) `2 <= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:30;
len g = (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)))))) + 1
by FINSEQ_2:16;
then A83:
1
+ 1
<= len g
by A51, XREAL_1:7;
A84:
L~ g = (L~ (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)))))) \/ (LSeg (((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))))) /. (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))))))),|[(E-bound (L~ (Cage (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)))) `2)]|))
by A47, A23, SPPOL_2:19, SPRECT_2:7;
L~ (Rev (Lower_Seq (C,n))) = (L~ ((Rev (Lower_Seq (C,n))) -: (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)))))) \/ (L~ ((Rev (Lower_Seq (C,n))) :- (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 A27, SPPOL_2:24;
then
L~ ((Rev (Lower_Seq (C,n))) -: (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))))) c= L~ (Rev (Lower_Seq (C,n)))
by XBOOLE_1:7;
then A85:
L~ ((Rev (Lower_Seq (C,n))) -: (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))))) c= L~ (Lower_Seq (C,n))
by SPPOL_2:22;
A86:
(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)))) `2 <= N-bound (L~ (Cage (C,n)))
by A20, PSCOMP_1:24;
A87:
|[(E-bound (L~ (Cage (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)))) `2)]| `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)))) `2
by EUCLID:52;
then A88:
LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|) is
horizontal
by SPPOL_1:15;
(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)))) `1 = |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:52;
then A89:
LSeg (
(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)))),
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|) is
vertical
by SPPOL_1:16;
A90:
L~ (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))))) c= L~ (Upper_Seq (C,n))
by A47, A23, SPRECT_3:18;
(h /. (len h)) `2 =
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `2
by A74, FINSEQ_4:67
.=
N-bound (L~ (Cage (C,n)))
by EUCLID:52
;
then
h is_a_v.c._for Cage (
C,
n)
by A71, A73, SPRECT_2:def 3;
then
L~ g meets L~ h
by A52, A75, A83, SPRECT_2:29;
then consider x being
object such that A91:
x in L~ g
and A92:
x in L~ h
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A91;
L~ h =
L~ (<*(SW-corner (L~ (Cage (C,n))))*> ^ (((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>))
by FINSEQ_1:32
.=
(LSeg ((SW-corner (L~ (Cage (C,n)))),((((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) /. 1))) \/ (L~ (((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>))
by SPPOL_2:20
.=
(LSeg ((SW-corner (L~ (Cage (C,n)))),((((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) /. 1))) \/ ((L~ ((Rev (Lower_Seq (C,n))) -: (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)))))) \/ (LSeg ((((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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))))))),|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|)))
by A27, FINSEQ_5:47, SPPOL_2:19
;
then A93:
(
x in LSeg (
(SW-corner (L~ (Cage (C,n)))),
((((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) /. 1)) or
x in (L~ ((Rev (Lower_Seq (C,n))) -: (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)))))) \/ (LSeg ((((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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))))))),|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|)) )
by A92, XBOOLE_0:def 3;
A94:
(SW-corner (L~ (Cage (C,n)))) `1 = (W-min (L~ (Cage (C,n)))) `1
by PSCOMP_1:29;
then A95:
LSeg (
(SW-corner (L~ (Cage (C,n)))),
(W-min (L~ (Cage (C,n))))) is
vertical
by SPPOL_1:16;
now contradictionper cases
( x in LSeg ((SW-corner (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))) or x in L~ ((Rev (Lower_Seq (C,n))) -: (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))))) or x in LSeg ((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)))),|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|) )
by A93, A81, A66, XBOOLE_0:def 3;
suppose A96:
x in LSeg (
(SW-corner (L~ (Cage (C,n)))),
(W-min (L~ (Cage (C,n)))))
;
contradictionthen A97:
x `2 <= (W-min (L~ (Cage (C,n)))) `2
by A82, TOPREAL1:4;
A98:
x `1 = (SW-corner (L~ (Cage (C,n)))) `1
by A95, A96, SPPOL_1:41;
then A99:
x `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
now contradictionper cases
( x in L~ (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))))) or x in LSeg ((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)))),|[(E-bound (L~ (Cage (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)))) `2)]|) )
by A91, A84, A77, XBOOLE_0:def 3;
suppose A100:
x in L~ (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)))))
;
contradictionthen
x in L~ (Upper_Seq (C,n))
by A90;
then
x in W-most (L~ (Cage (C,n)))
by A76, A98, EUCLID:52, SPRECT_2:12;
then
x `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:31;
then
x `2 = (W-min (L~ (Cage (C,n)))) `2
by A97, XXREAL_0:1;
then
x = W-min (L~ (Cage (C,n)))
by A94, A98, TOPREAL3:6;
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 A46, A1, A24, A43, A100, Th37;
then
W-min (L~ (Cage (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 A1, A22, FINSEQ_5:38;
hence
contradiction
by A16, A40, EUCLID:52;
verum end; suppose
x in LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|)
;
contradictionend; hence
contradiction
;
verum end; suppose A101:
x in L~ ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradictionnow contradictionper cases
( x in L~ (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))))) or x in LSeg ((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)))),|[(E-bound (L~ (Cage (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)))) `2)]|) )
by A91, A84, A77, XBOOLE_0:def 3;
suppose A102:
x in L~ (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)))))
;
contradictionthen
x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
by A90, A85, A101, XBOOLE_0:def 4;
then A103:
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
now contradictionper cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A103, TARSKI:def 2;
suppose
x = W-min (L~ (Cage (C,n)))
;
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)) = 1
by A46, A1, A24, A43, A102, Th37;
then
W-min (L~ (Cage (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 A1, A22, FINSEQ_5:38;
hence
contradiction
by A16, A40, EUCLID:52;
verum end; suppose
x = E-max (L~ (Cage (C,n)))
;
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)) = len (Upper_Seq (C,n))
by A46, A30, A24, A43, A102, Th38;
then
E-max (L~ (Cage (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 A30, A22, FINSEQ_5:38;
hence
contradiction
by A32, A40, EUCLID:52;
verum end; hence
contradiction
;
verum end; suppose A104:
x in LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|)
;
contradiction
LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|) is
horizontal
by A87, SPPOL_1:15;
then A105:
x `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)))) `2
by A104, SPPOL_1:40;
consider i being
Nat such that A106:
1
<= i
and A107:
i + 1
<= len ((Rev (Lower_Seq (C,n))) -: (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)))))
and A108:
x in LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)))
by A101, SPPOL_2:14;
A109:
i < len ((Rev (Lower_Seq (C,n))) -: (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 A107, NAT_1:13;
then A110:
((Rev (Lower_Seq (C,n))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A70, A106, Th52;
i in Seg ((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)))) .. (Rev (Lower_Seq (C,n))))
by A29, A106, A109, FINSEQ_1:1;
then A111:
((Rev (Lower_Seq (C,n))) -: (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))))) /. i = (Rev (Lower_Seq (C,n))) /. i
by A27, FINSEQ_5:43;
i + 1
>= 1
by NAT_1:11;
then
i + 1
in Seg ((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)))) .. (Rev (Lower_Seq (C,n))))
by A29, A107, FINSEQ_1:1;
then A112:
((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1) = (Rev (Lower_Seq (C,n))) /. (i + 1)
by A27, FINSEQ_5:43;
A113:
(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 <= x `1
by A32, A40, A63, A104, TOPREAL1:3;
now contradictionper cases
( i + 1 < len ((Rev (Lower_Seq (C,n))) -: (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))))) or i + 1 = len ((Rev (Lower_Seq (C,n))) -: (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 A107, XXREAL_0:1;
suppose A114:
i + 1
< len ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradiction
(
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 or
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 )
;
then A115:
(
x `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 or
x `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 )
by A108, TOPREAL1:3;
((Rev (Lower_Seq (C,n))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A70, A114, Th52, NAT_1:11;
hence
contradiction
by A40, A113, A111, A112, A110, A115, XXREAL_0:2;
verum suppose A116:
i + 1
= len ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradictionthen
i + 1
<= len (Rev (Lower_Seq (C,n)))
by A27, A29, FINSEQ_4:21;
then
LSeg (
((Rev (Lower_Seq (C,n))) /. i),
((Rev (Lower_Seq (C,n))) /. (i + 1)))
= LSeg (
(Rev (Lower_Seq (C,n))),
i)
by A106, TOPREAL1:def 3;
then
(
LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1))) is
vertical or
LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1))) is
horizontal )
by A111, A112, SPPOL_1:19;
hence
contradiction
by A44, A45, A66, A105, A108, A111, A110, A116, SPPOL_1:16, SPPOL_1:40;
verum end; hence
contradiction
;
verum end; hence
contradiction
;
verum suppose A117:
x in LSeg (
(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)))),
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|)
;
contradictionthen A118:
(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)))) `2 <= x `2
by A8, A86, TOPREAL1:4;
A119:
x `1 = (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)))) `1
by A89, A117, SPPOL_1:41;
now contradictionper cases
( x in L~ (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))))) or x in LSeg ((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)))),|[(E-bound (L~ (Cage (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)))) `2)]|) )
by A91, A84, A77, XBOOLE_0:def 3;
suppose
x in L~ (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)))))
;
contradictionthen consider i being
Nat such that A120:
1
<= i
and A121:
i + 1
<= 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)))))
and A122:
x in LSeg (
((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))))) /. i),
((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))))) /. (i + 1)))
by SPPOL_2:14;
i + 2
>= 1
+ 1
by NAT_1:11;
then A123:
(i + 2) - 1
>= (1 + 1) - 1
by XREAL_1:9;
i < 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 A121, NAT_1:13;
then
i 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)))))
by A120, FINSEQ_3:25;
then A124:
(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))))) /. i =
(Upper_Seq (C,n)) /. ((i + 2) -' 1)
by A47, A23, A79, SPRECT_2:3
.=
(Upper_Seq (C,n)) /. (i + (2 - 1))
by A123, XREAL_0:def 2
;
(i + 1) + 2
>= 1
+ 1
by NAT_1:11;
then A125:
((i + 1) + 2) - 1
>= (1 + 1) - 1
by XREAL_1:9;
A126:
1
<= i + 1
by NAT_1:11;
then
i + 1
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)))))
by A121, FINSEQ_3:25;
then A127:
(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))))) /. (i + 1) =
(Upper_Seq (C,n)) /. (((i + 1) + 2) -' 1)
by A47, A23, A79, SPRECT_2:3
.=
(Upper_Seq (C,n)) /. ((i + 1) + (2 - 1))
by A125, XREAL_0:def 2
;
A128:
(i + 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))) - 1) + 1
by A80, A121, XREAL_1:7;
then
i + 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;
then A129:
((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))))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A124, Th51, NAT_1:11;
(i + 1) + 1
<= len (Upper_Seq (C,n))
by A43, A128, XXREAL_0:2;
then
LSeg (
((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))))) /. i),
((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))))) /. (i + 1)))
= LSeg (
(Upper_Seq (C,n)),
(i + 1))
by A124, A126, A127, TOPREAL1:def 3;
then A130:
(
LSeg (
((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))))) /. i),
((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))))) /. (i + 1))) is
vertical or
LSeg (
((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))))) /. i),
((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))))) /. (i + 1))) is
horizontal )
by SPPOL_1:19;
now contradictionper cases
( i + 1 < 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))))) or i + 1 = 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 A121, XXREAL_0:1;
suppose
i + 1
< 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)))))
;
contradictionthen
(i + 1) + 1
<= 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 NAT_1:13;
then
((i + 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))) - 1) + 1
by A80, XREAL_1:7;
then
(i + 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))
by NAT_1:13;
then A131:
((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))))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A127, Th51, NAT_1:11;
(
((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))))) /. i) `1 <= ((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))))) /. (i + 1)) `1 or
((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))))) /. (i + 1)) `1 <= ((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))))) /. i) `1 )
;
hence
contradiction
by A44, A119, A122, A129, A131, TOPREAL1:3;
verum end; suppose A132:
i + 1
= 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)))))
;
contradictionthen
((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))))) /. i) `2 = ((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))))) /. (i + 1)) `2
by A40, A77, A129, A130, SPPOL_1:15, SPPOL_1:16;
hence
contradiction
by A53, A77, A118, A122, A132, GOBOARD7:6;
verum end; hence
contradiction
;
verum end; suppose
x in LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|)
;
contradictionend; hence
contradiction
;
verum end; hence
contradiction
;
verum suppose A133:
SW-corner (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n)))
;
contradictionreconsider RevLS =
Rev (Lower_Seq (C,n)) as
special FinSequence of
(TOP-REAL 2) ;
set h =
((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>;
A134:
(
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is
one-to-one &
RevLS -: (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)))) is
special )
by FINSEQ_3:93;
rng ((Rev (Lower_Seq (C,n))) -: (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))))) misses {|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|}
by A25, ZFMISC_1:50;
then
(rng ((Rev (Lower_Seq (C,n))) -: (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)))))) /\ {|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|} = {}
;
then
(rng ((Rev (Lower_Seq (C,n))) -: (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)))))) /\ (rng <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>) = {}
by FINSEQ_1:38;
then A135:
rng ((Rev (Lower_Seq (C,n))) -: (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))))) misses rng <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>
;
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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))))))) `1 =
(((Rev (Lower_Seq (C,n))) -: (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))))) /. ((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)))) .. (Rev (Lower_Seq (C,n))))) `1
by A27, FINSEQ_5:42
.=
(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)))) `1
by A27, FINSEQ_5:45
.=
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:52
.=
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. 1) `1
by FINSEQ_4:16
;
then reconsider h =
((Rev (Lower_Seq (C,n))) -: (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))))) ^ <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> as
one-to-one special FinSequence of
(TOP-REAL 2) by A135, A134, FINSEQ_3:91, GOBOARD2:8;
now for m being Nat st m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> holds
( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> implies ( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )A136:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:21;
assume
m in dom <*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*>
;
( W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A137:
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m = |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|
by FINSEQ_4:16;
then
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by EUCLID:52;
hence
(
W-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 &
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `1 <= E-bound (L~ (Cage (C,n))) )
by A136, JORDAN6:1;
( S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 & (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 = N-bound (L~ (Cage (C,n)))
by A137, EUCLID:52;
hence
(
S-bound (L~ (Cage (C,n))) <= (<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 &
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
by SPRECT_1:22;
verum end; then A138:
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
Rev (Lower_Seq (C,n)) is_in_the_area_of Cage (
C,
n)
by JORDAN1E:18, SPRECT_3:51;
then
(Rev (Lower_Seq (C,n))) -: (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)))) is_in_the_area_of Cage (
C,
n)
by A27, JORDAN1E:1;
then A139:
h is_in_the_area_of Cage (
C,
n)
by A138, SPRECT_2:24;
A140:
len h = (len ((Rev (Lower_Seq (C,n))) -: (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)))))) + 1
by FINSEQ_2:16;
then A141:
(h /. (len h)) `2 =
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `2
by FINSEQ_4:67
.=
N-bound (L~ (Cage (C,n)))
by EUCLID:52
;
L~ (Rev (Lower_Seq (C,n))) = (L~ ((Rev (Lower_Seq (C,n))) -: (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)))))) \/ (L~ ((Rev (Lower_Seq (C,n))) :- (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 A27, SPPOL_2:24;
then
L~ ((Rev (Lower_Seq (C,n))) -: (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))))) c= L~ (Rev (Lower_Seq (C,n)))
by XBOOLE_1:7;
then A142:
L~ ((Rev (Lower_Seq (C,n))) -: (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))))) c= L~ (Lower_Seq (C,n))
by SPPOL_2:22;
A143:
(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)))) `2 <= N-bound (L~ (Cage (C,n)))
by A20, PSCOMP_1:24;
(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)))) .. (Rev (Lower_Seq (C,n))) >= 0 + 1
by A28, A29, NAT_1:13;
then A144:
len ((Rev (Lower_Seq (C,n))) -: (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))))) >= 1
by A27, FINSEQ_5:42;
1
in dom h
by FINSEQ_5:6;
then
h /. 1
= h . 1
by PARTFUN1:def 6;
then (h /. 1) `2 =
(((Rev (Lower_Seq (C,n))) -: (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))))) /. 1) `2
by A144, FINSEQ_6:109
.=
((Rev (Lower_Seq (C,n))) /. 1) `2
by A27, FINSEQ_5:44
.=
((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `2
by FINSEQ_5:65
.=
(W-min (L~ (Cage (C,n)))) `2
by JORDAN1F:8
.=
S-bound (L~ (Cage (C,n)))
by A133, EUCLID:52
;
then A145:
h is_a_v.c._for Cage (
C,
n)
by A139, A141, SPRECT_2:def 3;
set FiP2 =
First_Point (
(L~ (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 midU =
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))));
A146:
|[(E-bound (L~ (Cage (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)))) `2)]| `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
A147:
L~ g = (L~ (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)))))) \/ (LSeg (((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))))) /. (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))))))),|[(E-bound (L~ (Cage (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)))) `2)]|))
by A47, A23, SPPOL_2:19, SPRECT_2:7;
A148:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A1, FINSEQ_6:42;
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 A22, A148, FINSEQ_5:9;
hence
contradiction
by A16, A40, EUCLID:52;
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 A24, XXREAL_0:1;
then A149:
(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 A150:
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 A43, A149, JORDAN4:8
.=
((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)
;
(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)))) `1 = |[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:52;
then A151:
LSeg (
(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)))),
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|) is
vertical
by SPPOL_1:16;
len g = (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)))))) + 1
by FINSEQ_2:16;
then A152:
1
+ 1
<= len g
by A51, XREAL_1:7;
A153:
((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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)))))) =
((Rev (Lower_Seq (C,n))) -: (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))))) /. ((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)))) .. (Rev (Lower_Seq (C,n))))
by A27, FINSEQ_5:42
.=
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 A27, FINSEQ_5:45
;
1
+ 1
<= len h
by A144, A140, XREAL_1:7;
then
L~ g meets L~ h
by A52, A145, A152, SPRECT_2:29;
then consider x being
object such that A154:
x in L~ g
and A155:
x in L~ h
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A154;
A156:
L~ h = (L~ ((Rev (Lower_Seq (C,n))) -: (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)))))) \/ (LSeg ((((Rev (Lower_Seq (C,n))) -: (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))))) /. (len ((Rev (Lower_Seq (C,n))) -: (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))))))),|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|))
by A27, FINSEQ_5:47, SPPOL_2:19;
A157:
(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))))) /. (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)))))) =
(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 A47, A23, SPRECT_2:9
.=
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 A22, FINSEQ_5:38
;
A158:
L~ (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))))) c= L~ (Upper_Seq (C,n))
by A47, A23, SPRECT_3:18;
A159:
(
L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) &
First_Point (
(L~ (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 A12, A17, JORDAN5C:18, SPPOL_2:22;
A160:
|[(E-bound (L~ (Cage (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)))) `2)]| `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)))) `2
by EUCLID:52;
then A161:
LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|) is
horizontal
by SPPOL_1:15;
now contradictionper cases
( x in L~ ((Rev (Lower_Seq (C,n))) -: (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))))) or x in LSeg ((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)))),|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|) )
by A155, A156, A153, XBOOLE_0:def 3;
suppose A162:
x in L~ ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradictionnow contradictionper cases
( x in L~ (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))))) or x in LSeg ((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)))),|[(E-bound (L~ (Cage (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)))) `2)]|) )
by A154, A147, A157, XBOOLE_0:def 3;
suppose A163:
x in L~ (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)))))
;
contradictionthen
x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
by A158, A142, A162, XBOOLE_0:def 4;
then A164:
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
now contradictionper cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A164, TARSKI:def 2;
suppose
x = W-min (L~ (Cage (C,n)))
;
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)) = 1
by A46, A1, A24, A43, A163, Th37;
then
W-min (L~ (Cage (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 A1, A22, FINSEQ_5:38;
hence
contradiction
by A16, A40, EUCLID:52;
verum end; suppose
x = E-max (L~ (Cage (C,n)))
;
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)) = len (Upper_Seq (C,n))
by A46, A30, A24, A43, A163, Th38;
then
E-max (L~ (Cage (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 A30, A22, FINSEQ_5:38;
hence
contradiction
by A32, A40, EUCLID:52;
verum end; hence
contradiction
;
verum end; suppose A165:
x in LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|)
;
contradiction
LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|) is
horizontal
by A160, SPPOL_1:15;
then A166:
x `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)))) `2
by A165, SPPOL_1:40;
consider i being
Nat such that A167:
1
<= i
and A168:
i + 1
<= len ((Rev (Lower_Seq (C,n))) -: (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)))))
and A169:
x in LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)))
by A162, SPPOL_2:14;
A170:
i < len ((Rev (Lower_Seq (C,n))) -: (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 A168, NAT_1:13;
then A171:
((Rev (Lower_Seq (C,n))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A159, A167, Th52;
i in Seg ((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)))) .. (Rev (Lower_Seq (C,n))))
by A29, A167, A170, FINSEQ_1:1;
then A172:
((Rev (Lower_Seq (C,n))) -: (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))))) /. i = (Rev (Lower_Seq (C,n))) /. i
by A27, FINSEQ_5:43;
i + 1
>= 1
by NAT_1:11;
then
i + 1
in Seg ((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)))) .. (Rev (Lower_Seq (C,n))))
by A29, A168, FINSEQ_1:1;
then A173:
((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1) = (Rev (Lower_Seq (C,n))) /. (i + 1)
by A27, FINSEQ_5:43;
A174:
(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 <= x `1
by A32, A40, A146, A165, TOPREAL1:3;
now contradictionper cases
( i + 1 < len ((Rev (Lower_Seq (C,n))) -: (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))))) or i + 1 = len ((Rev (Lower_Seq (C,n))) -: (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 A168, XXREAL_0:1;
suppose A175:
i + 1
< len ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradiction
(
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 or
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 )
;
then A176:
(
x `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1)) `1 or
x `1 <= (((Rev (Lower_Seq (C,n))) -: (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))))) /. i) `1 )
by A169, TOPREAL1:3;
((Rev (Lower_Seq (C,n))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A159, A175, Th52, NAT_1:11;
hence
contradiction
by A40, A174, A172, A173, A171, A176, XXREAL_0:2;
verum suppose A177:
i + 1
= len ((Rev (Lower_Seq (C,n))) -: (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)))))
;
contradictionthen
i + 1
<= len (Rev (Lower_Seq (C,n)))
by A27, A29, FINSEQ_4:21;
then
LSeg (
((Rev (Lower_Seq (C,n))) /. i),
((Rev (Lower_Seq (C,n))) /. (i + 1)))
= LSeg (
(Rev (Lower_Seq (C,n))),
i)
by A167, TOPREAL1:def 3;
then
(
LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1))) is
vertical or
LSeg (
(((Rev (Lower_Seq (C,n))) -: (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))))) /. i),
(((Rev (Lower_Seq (C,n))) -: (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))))) /. (i + 1))) is
horizontal )
by A172, A173, SPPOL_1:19;
hence
contradiction
by A44, A45, A153, A166, A169, A172, A171, A177, SPPOL_1:16, SPPOL_1:40;
verum end; hence
contradiction
;
verum end; hence
contradiction
;
verum suppose A178:
x in LSeg (
(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)))),
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|)
;
contradictionthen A179:
(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)))) `2 <= x `2
by A8, A143, TOPREAL1:4;
A180:
x `1 = (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)))) `1
by A151, A178, SPPOL_1:41;
now contradictionper cases
( x in L~ (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))))) or x in LSeg ((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)))),|[(E-bound (L~ (Cage (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)))) `2)]|) )
by A154, A147, A157, XBOOLE_0:def 3;
suppose
x in L~ (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)))))
;
contradictionthen consider i being
Nat such that A181:
1
<= i
and A182:
i + 1
<= 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)))))
and A183:
x in LSeg (
((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))))) /. i),
((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))))) /. (i + 1)))
by SPPOL_2:14;
i + 2
>= 1
+ 1
by NAT_1:11;
then A184:
(i + 2) - 1
>= (1 + 1) - 1
by XREAL_1:9;
i < 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 A182, NAT_1:13;
then
i 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)))))
by A181, FINSEQ_3:25;
then A185:
(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))))) /. i =
(Upper_Seq (C,n)) /. ((i + 2) -' 1)
by A47, A23, A149, SPRECT_2:3
.=
(Upper_Seq (C,n)) /. (i + (2 - 1))
by A184, XREAL_0:def 2
;
(i + 1) + 2
>= 1
+ 1
by NAT_1:11;
then A186:
((i + 1) + 2) - 1
>= (1 + 1) - 1
by XREAL_1:9;
A187:
1
<= i + 1
by NAT_1:11;
then
i + 1
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)))))
by A182, FINSEQ_3:25;
then A188:
(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))))) /. (i + 1) =
(Upper_Seq (C,n)) /. (((i + 1) + 2) -' 1)
by A47, A23, A149, SPRECT_2:3
.=
(Upper_Seq (C,n)) /. ((i + 1) + (2 - 1))
by A186, XREAL_0:def 2
;
A189:
(i + 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))) - 1) + 1
by A150, A182, XREAL_1:7;
then
i + 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;
then A190:
((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))))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A185, Th51, NAT_1:11;
(i + 1) + 1
<= len (Upper_Seq (C,n))
by A43, A189, XXREAL_0:2;
then
LSeg (
((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))))) /. i),
((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))))) /. (i + 1)))
= LSeg (
(Upper_Seq (C,n)),
(i + 1))
by A185, A187, A188, TOPREAL1:def 3;
then A191:
(
LSeg (
((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))))) /. i),
((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))))) /. (i + 1))) is
vertical or
LSeg (
((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))))) /. i),
((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))))) /. (i + 1))) is
horizontal )
by SPPOL_1:19;
now contradictionper cases
( i + 1 < 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))))) or i + 1 = 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 A182, XXREAL_0:1;
suppose
i + 1
< 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)))))
;
contradictionthen
(i + 1) + 1
<= 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 NAT_1:13;
then
((i + 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))) - 1) + 1
by A150, XREAL_1:7;
then
(i + 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))
by NAT_1:13;
then A192:
((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))))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A188, Th51, NAT_1:11;
(
((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))))) /. i) `1 <= ((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))))) /. (i + 1)) `1 or
((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))))) /. (i + 1)) `1 <= ((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))))) /. i) `1 )
;
hence
contradiction
by A44, A180, A183, A190, A192, TOPREAL1:3;
verum end; suppose A193:
i + 1
= 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)))))
;
contradictionthen
((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))))) /. i) `2 = ((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))))) /. (i + 1)) `2
by A40, A157, A190, A191, SPPOL_1:15, SPPOL_1:16;
hence
contradiction
by A53, A157, A179, A183, A193, GOBOARD7:6;
verum end; hence
contradiction
;
verum end; suppose
x in LSeg (
(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)))),
|[(E-bound (L~ (Cage (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)))) `2)]|)
;
contradictionend; hence
contradiction
;
verum end; hence
contradiction
;
verum end;
hence
contradiction
; verum