let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let n be Element of NAT ; :: thesis:
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, SPPOL_2:39;
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 ; :: thesis:
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 ; :: thesis:
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 )]|*> ; :: thesis:
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; :: thesis:
(<*|[(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; :: thesis:

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 )]|} <> {} ; :: thesis:
then 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; :: thesis:

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 ; :: thesis:
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)) = Last_Point (L~ (Lower_Seq C,n)),(E-max (L~ (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; :: thesis:

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) ; :: thesis:
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; :: thesis:

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 ; :: thesis:
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 ;

suppose A55: SW-corner (L~ (Cage C,n)) <> W-min (L~ (Cage C,n)) ; :: thesis:

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) ; :: thesis:
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; :: thesis:

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) by SPPOL_2:42;
A61: <*(SW-corner (L~ (Cage C,n)))*> is special by SPPOL_2:39;
(<*(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 A61, 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, SPPOL_2:39;
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 ; :: thesis:
assume m in dom <*(SW-corner (L~ (Cage C,n)))*> ; :: thesis:
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; :: thesis:
(<*(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; :: thesis:

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 ; :: thesis:
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)))]|*> ; :: thesis:
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; :: thesis:
(<*|[(((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; :: thesis:

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, JORDAN3:17
.= (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 ; :: thesis:
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) = ((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; :: thesis:

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 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))) ; :: thesis:

then 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 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))) ; :: thesis:

then 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; :: thesis:

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 )]| ; :: thesis:

hence contradiction by A16, A32, A40, A64, A100, TOPREAL1:9; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

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)))) ; :: thesis:

now

per cases 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))) ; :: thesis:

then 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 by A104, TARSKI:def 2;

suppose x = W-min (L~ (Cage C,n)) ; :: thesis:

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, 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; :: thesis:

end;

suppose x = E-max (L~ (Cage C,n)) ; :: thesis:

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) = 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; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

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 )]| ; :: thesis:

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 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)))) ; :: thesis:

( (((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; :: thesis:

end;

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)))) ; :: thesis:

then 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, SPPOL_2:42;
hence contradiction by A44, A45, A67, A106, A109, A112, A111, A117, SPPOL_1:37, SPPOL_1:63; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

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)))]| ; :: thesis:

then 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 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))) ; :: thesis:

then 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 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))) ; :: thesis:

then (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; :: thesis:

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))) ; :: thesis:

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))) /. 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; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

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 )]| ; :: thesis:

hence contradiction by A53, A89, A119, SPPOL_1:63; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose A134: SW-corner (L~ (Cage C,n)) = W-min (L~ (Cage C,n)) ; :: thesis:

reconsider RevLS = Rev (Lower_Seq C,n) as special FinSequence of (TOP-REAL 2) by SPPOL_2:42;
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 by SPPOL_2:39;
(((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, A137, FINSEQ_3:98, GOBOARD2:13;

now

let m be Element of NAT ; :: thesis:
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)))]|*> ; :: thesis:
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; :: thesis:
(<*|[(((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; :: thesis:

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, JORDAN3:17
.= ((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 ; :: thesis:
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) = ((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; :: thesis:

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 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)))) ; :: thesis:

now

per cases 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))) ; :: thesis:

then 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 by A166, TARSKI:def 2;

suppose x = W-min (L~ (Cage C,n)) ; :: thesis:

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, 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; :: thesis:

end;

suppose x = E-max (L~ (Cage C,n)) ; :: thesis:

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) = 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; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

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 )]| ; :: thesis:

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 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)))) ; :: thesis:

( (((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; :: thesis:

end;

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)))) ; :: thesis:

then 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, SPPOL_2:42;
hence contradiction by A44, A45, A155, A168, A171, A174, A173, A179, SPPOL_1:37, SPPOL_1:63; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

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)))]| ; :: thesis:

then 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 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))) ; :: thesis:

then 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 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))) ; :: thesis:

then (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; :: thesis:

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))) ; :: thesis:

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))) /. 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; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

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 )]| ; :: thesis:

hence contradiction by A53, A163, A181, SPPOL_1:63; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis: