let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Element of 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 Element of 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:23;
then
W-bound (L~ (Cage (C,n))) <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN6:2;
then A3:
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by EUCLID:56;
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= E-bound (L~ (Cage (C,n)))
by A2, JORDAN6:2;
then A4:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1
by EUCLID:56;
set GCw = (Gauge (C,n)) * ((Center (Gauge (C,n))),(width (Gauge (C,n))));
A5:
1 <= Center (Gauge (C,n))
by JORDAN1B:12;
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:91, JORDAN1B:14;
A7:
(SW-corner (L~ (Cage (C,n)))) `2 <= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:87;
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:56;
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:102;
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:51;
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:31;
A13:
4 <= len (Gauge (C,n))
by JORDAN8:13;
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:33;
then A16:
W-bound (L~ (Cage (C,n))) < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by XREAL_1:228;
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:31;
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:64;
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:17;
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 Th55;
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:30;
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:27;
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, Th43
.=
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by Th41
;
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:57;
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, Th51, JORDAN1B:16;
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:60;
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:56;
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:34;
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:55;
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:44;
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:56;
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))))]|} = {}
by XBOOLE_0:def 7;
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:55;
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))))]|*>
by XBOOLE_0:def 7;
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, Th56;
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:60;
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:50;
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:45;
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:31;
A32:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 < E-bound (L~ (Cage (C,n)))
by A15, XREAL_1:228;
then A33:
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 <= (E-max (L~ (Cage (C,n)))) `1
by EUCLID:56;
(W-min (L~ (Cage (C,n)))) `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A16, EUCLID:56;
then
( L~ (Upper_Seq (C,n)) meets Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2) & (L~ (Upper_Seq (C,n))) /\ (Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)) is closed )
by A31, A33, JORDAN6:64;
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:17;
now let m be
Element of
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:55;
then
m = 1
by FINSEQ_1:4, 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:25;
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:56;
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:23;
( 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:56;
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:71;
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:34;
now 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
set 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, Th61;
hence
contradiction
by A32, EUCLID:56;
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)]|}
by XBOOLE_0:def 7;
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:55;
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:27;
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:34;
A45:
now assume
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `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:11;
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:20;
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:56;
verum end;
len (Upper_Seq (C,n)) >= 3
by JORDAN1E:19;
then A46:
len (Upper_Seq (C,n)) > 2
by XXREAL_0:2;
then A47:
2 in dom (Upper_Seq (C,n))
by FINSEQ_3:27;
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:13
.=
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (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:41
.=
|[(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:56
.=
(<*|[(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:25
;
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:41;
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 Th39;
then
W-bound (L~ (Cage (C,n))) = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A39, JORDAN6:34;
hence
contradiction
by SPRECT_1:33;
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:39;
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:98, GOBOARD2:13;
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:21, SPRECT_2:26;
then A49:
g is_in_the_area_of Cage (C,n)
by A38, SPRECT_2:28;
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:11
.=
(<*|[(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:56
.=
|[(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:25
.=
E-bound (L~ (Cage (C,n)))
by EUCLID:56
;
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:9;
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:27;
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:83
.=
((Upper_Seq (C,n)) /. 2) `1
by A47, A23, SPRECT_2:12
.=
W-bound (L~ (Cage (C,n)))
by Th39
;
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 Th47;
now per 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:85;
then A56:
(SW-corner (L~ (Cage (C,n)))) `2 <> (W-min (L~ (Cage (C,n)))) `2
by A55, TOPREAL3:11;
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:36;
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:56;
then
SW-corner (L~ (Cage (C,n))) in W-most (L~ (Cage (C,n)))
by A57, A58, SPRECT_2:16;
then
(W-min (L~ (Cage (C,n)))) `2 <= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:88;
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:60;
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:56;
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)))))) = {}
by XBOOLE_0:def 7;
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:55;
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)))))
by XBOOLE_0:def 7;
<*(SW-corner (L~ (Cage (C,n))))*> is
one-to-one
by FINSEQ_3:102;
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:98;
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) ;
A61:
<*(SW-corner (L~ (Cage (C,n))))*> is
special
;
(<*(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:56
.=
(SW-corner (L~ (Cage (C,n)))) `1
by FINSEQ_4:25
.=
W-bound (L~ (Cage (C,n)))
by EUCLID:56
.=
(W-min (L~ (Cage (C,n)))) `1
by EUCLID:56
.=
((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1
by JORDAN1F:8
.=
((Rev (Lower_Seq (C,n))) /. 1) `1
by FINSEQ_5:68
.=
(((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:47
;
then A62:
<*(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:13;
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:50;
then A63:
((<*(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:11
.=
(((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:45
.=
(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:48
.=
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:56
.=
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. 1) `1
by FINSEQ_4:25
;
(
<*|[(((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:102;
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, A63, A62, FINSEQ_3:98, GOBOARD2:13;
A64:
|[(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:56;
now let m be
Element of
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:55;
then
m = 1
by FINSEQ_1:4, TARSKI:def 1;
then A65:
<*(SW-corner (L~ (Cage (C,n))))*> /. m = SW-corner (L~ (Cage (C,n)))
by FINSEQ_4:25;
then
(<*(SW-corner (L~ (Cage (C,n))))*> /. m) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:56;
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:23;
( 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 A65, EUCLID:56;
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:24;
verum end; then A66:
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
A67:
((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:45
.=
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:48
;
now let m be
Element of
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))) ) )A68:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:23;
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:55;
then
m = 1
by FINSEQ_1:4, TARSKI:def 1;
then A69:
<*|[(((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:25;
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:56;
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 A68, JORDAN6:2;
( 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 A69, EUCLID:56;
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:24;
verum end; then A70:
<*|[(((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;
A71:
(
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:22, SPRECT_3:68;
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:5;
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 A66, SPRECT_2:28;
then A72:
h is_in_the_area_of Cage (
C,
n)
by A70, SPRECT_2:28;
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 A73:
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 8;
then A74:
(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 A73, FINSEQ_6:115
.=
(SW-corner (L~ (Cage (C,n)))) `2
by FINSEQ_5:16
.=
S-bound (L~ (Cage (C,n)))
by EUCLID:56
;
A75:
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:19;
then A76:
1
+ 1
<= len h
by A73, XREAL_1:9;
L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
by JORDAN1E:17;
then A77:
L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n))
by XBOOLE_1:7;
A78:
(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:13
.=
First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (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:41
;
A79:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A1, FINSEQ_6:46;
now assume
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) = 1
;
contradictionthen (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) =
((Upper_Seq (C,n)) /. 1) .. (Upper_Seq (C,n))
by FINSEQ_6:47
.=
(W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
by JORDAN1F:5
;
then
First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (Cage (C,n)))),
(E-max (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
= W-min (L~ (Cage (C,n)))
by A22, A79, FINSEQ_5:10;
hence
contradiction
by A16, A40, EUCLID:56;
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 A80:
(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:21;
then
((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) -' 2
= ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) - 2
by XREAL_0:def 2;
then A81:
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, A80, JORDAN4:20
.=
((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (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 A82:
(((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:83
.=
(Rev (Lower_Seq (C,n))) /. 1
by A27, FINSEQ_5:47
.=
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by FINSEQ_5:68
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
A83:
(SW-corner (L~ (Cage (C,n)))) `2 <= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:87;
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:19;
then A84:
1
+ 1
<= len g
by A51, XREAL_1:9;
A85:
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:11;
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:25;
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 A86:
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;
A87:
(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:71;
A88:
|[(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:56;
then A89:
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:36;
(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:56;
then A90:
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:37;
A91:
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:34;
(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 A75, FINSEQ_4:82
.=
N-bound (L~ (Cage (C,n)))
by EUCLID:56
;
then
h is_a_v.c._for Cage (
C,
n)
by A72, A74, SPRECT_2:def 3;
then
L~ g meets L~ h
by A52, A76, A84, SPRECT_2:33;
then consider x being
set such that A92:
x in L~ g
and A93:
x in L~ h
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A92;
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:45
.=
(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:50, SPPOL_2:19
;
then A94:
(
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 A93, XBOOLE_0:def 3;
A95:
(SW-corner (L~ (Cage (C,n)))) `1 = (W-min (L~ (Cage (C,n)))) `1
by PSCOMP_1:85;
then A96:
LSeg (
(SW-corner (L~ (Cage (C,n)))),
(W-min (L~ (Cage (C,n))))) is
vertical
by SPPOL_1:37;
now per 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 A94, A82, A67, XBOOLE_0:def 3;
suppose A97:
x in LSeg (
(SW-corner (L~ (Cage (C,n)))),
(W-min (L~ (Cage (C,n)))))
;
contradictionthen A98:
x `2 <= (W-min (L~ (Cage (C,n)))) `2
by A83, TOPREAL1:10;
A99:
x `1 = (SW-corner (L~ (Cage (C,n)))) `1
by A96, A97, SPPOL_1:64;
then A100:
x `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:56;
now per 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 A92, A85, A78, XBOOLE_0:def 3;
suppose A101:
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 A91;
then
x in W-most (L~ (Cage (C,n)))
by A77, A99, EUCLID:56, SPRECT_2:16;
then
x `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:88;
then
x `2 = (W-min (L~ (Cage (C,n)))) `2
by A98, XXREAL_0:1;
then
x = W-min (L~ (Cage (C,n)))
by A95, A99, TOPREAL3:11;
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, A101, Th45;
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:41;
hence
contradiction
by A16, A40, EUCLID:56;
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 A102:
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 per 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 A92, A85, A78, XBOOLE_0:def 3;
suppose A103:
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 A91, A86, A102, XBOOLE_0:def 4;
then A104:
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:20;
now per cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A104, 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, A103, Th45;
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:41;
hence
contradiction
by A16, A40, EUCLID:56;
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, A103, Th46;
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:41;
hence
contradiction
by A32, A40, EUCLID:56;
verum end; hence
contradiction
;
verum end; suppose A105:
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 A88, SPPOL_1:36;
then A106:
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 A105, SPPOL_1:63;
consider i being
Element of
NAT such that A107:
1
<= i
and A108:
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 A109:
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 A102, SPPOL_2:14;
A110:
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 A108, NAT_1:13;
then A111:
((Rev (Lower_Seq (C,n))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A71, A107, Th60;
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, A107, A110, FINSEQ_1:3;
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 = (Rev (Lower_Seq (C,n))) /. i
by A27, FINSEQ_5:46;
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, A108, FINSEQ_1:3;
then A113:
((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:46;
A114:
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (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, A64, A105, TOPREAL1:9;
now per 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 A108, XXREAL_0:1;
suppose A115:
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 A116:
(
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 A109, TOPREAL1:9;
((Rev (Lower_Seq (C,n))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A71, A115, Th60, NAT_1:11;
hence
contradiction
by A40, A114, A112, A113, A111, A116, XXREAL_0:2;
verum suppose A117:
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:31;
then
LSeg (
((Rev (Lower_Seq (C,n))) /. i),
((Rev (Lower_Seq (C,n))) /. (i + 1)))
= LSeg (
(Rev (Lower_Seq (C,n))),
i)
by A107, TOPREAL1:def 5;
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 A112, A113, SPPOL_1:41;
hence
contradiction
by A44, A45, A67, A106, A109, A112, A111, A117, SPPOL_1:37, SPPOL_1:63;
verum end; hence
contradiction
;
verum end; hence
contradiction
;
verum suppose A118:
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 A119:
(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, A87, TOPREAL1:10;
A120:
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 A90, A118, SPPOL_1:64;
now per 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 A92, A85, A78, 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
Element of
NAT such that A121:
1
<= i
and A122:
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 A123:
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 A124:
(i + 2) - 1
>= (1 + 1) - 1
by XREAL_1:11;
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 A122, 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 A121, FINSEQ_3:27;
then A125:
(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, A80, SPRECT_2:7
.=
(Upper_Seq (C,n)) /. (i + (2 - 1))
by A124, XREAL_0:def 2
;
(i + 1) + 2
>= 1
+ 1
by NAT_1:11;
then A126:
((i + 1) + 2) - 1
>= (1 + 1) - 1
by XREAL_1:11;
A127:
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 A122, FINSEQ_3:27;
then A128:
(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, A80, SPRECT_2:7
.=
(Upper_Seq (C,n)) /. ((i + 1) + (2 - 1))
by A126, XREAL_0:def 2
;
A129:
(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 A81, A122, XREAL_1:9;
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 A130:
((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, A125, Th59, NAT_1:11;
(i + 1) + 1
<= len (Upper_Seq (C,n))
by A43, A129, 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 A125, A127, A128, TOPREAL1:def 5;
then A131:
(
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:41;
now per 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 A122, 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 A81, XREAL_1:9;
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 A132:
((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, A128, Th59, 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, A120, A123, A130, A132, TOPREAL1:9;
verum end; suppose A133:
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, A78, A130, A131, SPPOL_1:36, SPPOL_1:37;
hence
contradiction
by A53, A78, A119, A123, A133, 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 A134:
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))))]|*>;
A135:
(
<*|[(((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:102;
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:56;
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))))]|} = {}
by XBOOLE_0:def 7;
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:55;
then A136:
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))))]|*>
by XBOOLE_0:def 7;
A137:
<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> is
special
;
(((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:45
.=
(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:48
.=
|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]| `1
by A44, EUCLID:56
.=
(<*|[(((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2),(N-bound (L~ (Cage (C,n))))]|*> /. 1) `1
by FINSEQ_4:25
;
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 A136, A135, FINSEQ_3:98, GOBOARD2:13;
now let m be
Element of
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))) ) )A138:
W-bound (L~ (Cage (C,n))) <= E-bound (L~ (Cage (C,n)))
by SPRECT_1:23;
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:55;
then
m = 1
by FINSEQ_1:4, TARSKI:def 1;
then A139:
<*|[(((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:25;
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:56;
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 A138, JORDAN6:2;
( 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 A139, EUCLID:56;
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:24;
verum end; then A140:
<*|[(((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:22, SPRECT_3:68;
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:5;
then A141:
h is_in_the_area_of Cage (
C,
n)
by A140, SPRECT_2:28;
A142:
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:19;
then A143:
(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:82
.=
N-bound (L~ (Cage (C,n)))
by EUCLID:56
;
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:25;
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 A144:
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;
A145:
(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:71;
(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 A146:
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:45;
1
in dom h
by FINSEQ_5:6;
then
h /. 1
= h . 1
by PARTFUN1:def 8;
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 A146, FINSEQ_6:115
.=
((Rev (Lower_Seq (C,n))) /. 1) `2
by A27, FINSEQ_5:47
.=
((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `2
by FINSEQ_5:68
.=
(W-min (L~ (Cage (C,n)))) `2
by JORDAN1F:8
.=
S-bound (L~ (Cage (C,n)))
by A134, EUCLID:56
;
then A147:
h is_a_v.c._for Cage (
C,
n)
by A141, A143, 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))));
A148:
|[(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:56;
A149:
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:11;
A150:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A1, FINSEQ_6:46;
now assume
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) = 1
;
contradictionthen (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) =
((Upper_Seq (C,n)) /. 1) .. (Upper_Seq (C,n))
by FINSEQ_6:47
.=
(W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
by JORDAN1F:5
;
then
First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (Cage (C,n)))),
(E-max (L~ (Cage (C,n)))),
(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))
= W-min (L~ (Cage (C,n)))
by A22, A150, FINSEQ_5:10;
hence
contradiction
by A16, A40, EUCLID:56;
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 A151:
(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:21;
then
((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) -' 2
= ((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))) - 2
by XREAL_0:def 2;
then A152:
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, A151, JORDAN4:20
.=
((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (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:56;
then A153:
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:37;
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:19;
then A154:
1
+ 1
<= len g
by A51, XREAL_1:9;
A155:
((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:45
.=
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:48
;
1
+ 1
<= len h
by A146, A142, XREAL_1:9;
then
L~ g meets L~ h
by A52, A147, A154, SPRECT_2:33;
then consider x being
set such that A156:
x in L~ g
and A157:
x in L~ h
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A156;
A158:
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:50, SPPOL_2:19;
A159:
(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:13
.=
First_Point (
(L~ (Upper_Seq (C,n))),
(W-min (L~ (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:41
;
A160:
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:34;
A161:
(
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;
A162:
|[(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:56;
then A163:
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:36;
now per 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 A157, A158, A155, XBOOLE_0:def 3;
suppose A164:
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 per 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 A156, A149, A159, XBOOLE_0:def 3;
suppose A165:
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 A160, A144, A164, XBOOLE_0:def 4;
then A166:
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:20;
now per cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A166, 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, A165, Th45;
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:41;
hence
contradiction
by A16, A40, EUCLID:56;
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, A165, Th46;
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:41;
hence
contradiction
by A32, A40, EUCLID:56;
verum end; hence
contradiction
;
verum end; suppose A167:
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 A162, SPPOL_1:36;
then A168:
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 A167, SPPOL_1:63;
consider i being
Element of
NAT such that A169:
1
<= i
and A170:
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 A171:
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 A164, SPPOL_2:14;
A172:
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 A170, NAT_1:13;
then A173:
((Rev (Lower_Seq (C,n))) /. i) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A161, A169, Th60;
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, A169, A172, FINSEQ_1:3;
then A174:
((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:46;
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, A170, FINSEQ_1:3;
then A175:
((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:46;
A176:
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (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, A148, A167, TOPREAL1:9;
now per 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 A170, XXREAL_0:1;
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)))))
;
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 A178:
(
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 A171, TOPREAL1:9;
((Rev (Lower_Seq (C,n))) /. (i + 1)) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A29, A161, A177, Th60, NAT_1:11;
hence
contradiction
by A40, A176, A174, A175, A173, A178, XXREAL_0:2;
verum suppose A179:
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:31;
then
LSeg (
((Rev (Lower_Seq (C,n))) /. i),
((Rev (Lower_Seq (C,n))) /. (i + 1)))
= LSeg (
(Rev (Lower_Seq (C,n))),
i)
by A169, TOPREAL1:def 5;
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 A174, A175, SPPOL_1:41;
hence
contradiction
by A44, A45, A155, A168, A171, A174, A173, A179, SPPOL_1:37, SPPOL_1:63;
verum end; hence
contradiction
;
verum end; hence
contradiction
;
verum suppose A180:
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 A181:
(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, A145, TOPREAL1:10;
A182:
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 A153, A180, SPPOL_1:64;
now per 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 A156, A149, A159, 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
Element of
NAT such that A183:
1
<= i
and A184:
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 A185:
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 A186:
(i + 2) - 1
>= (1 + 1) - 1
by XREAL_1:11;
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 A184, 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 A183, FINSEQ_3:27;
then A187:
(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, A151, SPRECT_2:7
.=
(Upper_Seq (C,n)) /. (i + (2 - 1))
by A186, XREAL_0:def 2
;
(i + 1) + 2
>= 1
+ 1
by NAT_1:11;
then A188:
((i + 1) + 2) - 1
>= (1 + 1) - 1
by XREAL_1:11;
A189:
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 A184, FINSEQ_3:27;
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) =
(Upper_Seq (C,n)) /. (((i + 1) + 2) -' 1)
by A47, A23, A151, SPRECT_2:7
.=
(Upper_Seq (C,n)) /. ((i + 1) + (2 - 1))
by A188, XREAL_0:def 2
;
A191:
(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 A152, A184, XREAL_1:9;
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 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 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by A21, A187, Th59, NAT_1:11;
(i + 1) + 1
<= len (Upper_Seq (C,n))
by A43, A191, 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 A187, A189, A190, TOPREAL1:def 5;
then A193:
(
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:41;
now per 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 A184, 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 A152, XREAL_1:9;
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 A194:
((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, A190, Th59, 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, A182, A185, A192, A194, TOPREAL1:9;
verum end; suppose A195:
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, A159, A192, A193, SPPOL_1:36, SPPOL_1:37;
hence
contradiction
by A53, A159, A181, A185, A195, 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