let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies LeftComp f <> RightComp f )
set A = N-min (L~ f);
assume that
A1: f /. 1 = N-min (L~ f) and
A2: LeftComp f = RightComp f ; :: thesis: contradiction
A3: LeftComp (SpStSeq (L~ f)) c= LeftComp f by A1, SPRECT_3:41;
consider i being Element of NAT such that
A4: 1 <= i and
A5: i < len (GoB f) and
A6: N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by SPRECT_3:28;
set w = width (GoB f);
A7: len f > 4 by GOBOARD7:34;
A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
A9: width (GoB f) > 1 by GOBOARD7:33;
then A10: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
A11: [i,(width (GoB f))] in Indices (GoB f) by A4, A5, A9, MATRIX_1:36;
A12: 1 <= i + 1 by NAT_1:11;
A13: i + 1 <= len (GoB f) by A5, NAT_1:13;
then A14: [(i + 1),(width (GoB f))] in Indices (GoB f) by A9, A12, MATRIX_1:36;
A15: 1 in dom f by FINSEQ_5:6;
A16: i in dom (GoB f) by A4, A5, FINSEQ_3:25;
then A17: f /. (1 + 1) = (GoB f) * ((i + 1),(width (GoB f))) by A1, A6, SPRECT_3:29;
then A18: right_cell (f,1) = cell ((GoB f),i,((width (GoB f)) -' 1)) by A1, A6, A8, A10, A11, A14, GOBOARD5:28;
set z2 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))));
set p1 = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))));
set p2 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))));
A19: 1 <= (width (GoB f)) -' 1 by GOBOARD7:33, NAT_D:49;
then A20: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in Int (cell ((GoB f),i,((width (GoB f)) -' 1))) by A4, A10, A13, GOBOARD6:31;
A21: Int (right_cell (f,1)) c= RightComp f by A8, GOBOARD9:25;
A22: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
A23: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
A24: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A25: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
A26: 1 < i + 1 by A4, NAT_1:13;
A27: 1 <= len (GoB f) by A4, A5, XXREAL_0:2;
A28: (width (GoB f)) -' 1 < width (GoB f) by A10, XREAL_1:29;
A29: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = (1 / 2) * ((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) by A4, A6, A10, A13, A19, GOBOARD7:9;
then A30: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `1) by TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `1) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) by TOPREAL3:2
.= ((1 / 2) * ((N-min (L~ f)) `1)) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) ;
A31: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `2) by A29, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `2) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) by TOPREAL3:2
.= (1 / 2) * ((N-bound (L~ f)) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) by EUCLID:52
.= ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) ;
A32: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;
A33: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;
A34: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;
A35: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;
N-min (L~ f) in L~ f by SPRECT_1:11;
then (N-min (L~ f)) `1 >= W-bound (L~ f) by PSCOMP_1:24;
then A36: (1 / 2) * ((N-min (L~ f)) `1) >= (1 / 2) * (W-bound (L~ f)) by XREAL_1:64;
A37: ((GoB f) * (1,((width (GoB f)) -' 1))) `1 = ((GoB f) * (1,1)) `1 by A19, A27, A28, GOBOARD5:2;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > ((GoB f) * (1,((width (GoB f)) -' 1))) `1 by A13, A19, A26, A28, GOBOARD5:3;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > W-bound (L~ f) by A37, JORDAN5D:37;
then (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) > (1 / 2) * (W-bound (L~ f)) by XREAL_1:68;
then A38: W-bound (L~ (SpStSeq (L~ f))) < ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by A22, A30, A32, A36, XREAL_1:8;
N-max (L~ f) in L~ f by SPRECT_1:11;
then (N-max (L~ f)) `1 <= E-bound (L~ f) by PSCOMP_1:24;
then (N-min (L~ f)) `1 < E-bound (L~ f) by SPRECT_2:51, XXREAL_0:2;
then A39: (1 / 2) * ((N-min (L~ f)) `1) < (1 / 2) * (E-bound (L~ f)) by XREAL_1:68;
A40: ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A19, A27, A28, GOBOARD5:2;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 by A12, A13, A19, A28, SPRECT_3:13;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= E-bound (L~ f) by A40, JORDAN5D:39;
then (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) <= (1 / 2) * (E-bound (L~ f)) by XREAL_1:64;
then A41: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 < E-bound (L~ (SpStSeq (L~ f))) by A25, A30, A35, A39, XREAL_1:8;
A42: (1 / 2) * (N-bound (L~ f)) > (1 / 2) * (S-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;
A43: ((GoB f) * ((i + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A9, A12, A13, GOBOARD5:1;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= ((GoB f) * ((i + 1),1)) `2 by A12, A13, A19, A28, SPRECT_3:12;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= S-bound (L~ f) by A43, JORDAN5D:38;
then (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) >= (1 / 2) * (S-bound (L~ f)) by XREAL_1:64;
then A44: S-bound (L~ (SpStSeq (L~ f))) < ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 by A23, A31, A33, A42, XREAL_1:8;
A45: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < ((GoB f) * ((i + 1),(width (GoB f)))) `2 by A12, A13, A19, A28, GOBOARD5:4;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < N-bound (L~ f) by A45, JORDAN5D:40;
then (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) < (1 / 2) * (N-bound (L~ f)) by XREAL_1:68;
then A46: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 < N-bound (L~ (SpStSeq (L~ f))) by A24, A31, A34, XREAL_1:6;
RightComp (SpStSeq (L~ f)) = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ (SpStSeq (L~ f))) < q `1 & q `1 < E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) < q `2 & q `2 < N-bound (L~ (SpStSeq (L~ f))) ) } by SPRECT_3:37;
then A47: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in RightComp (SpStSeq (L~ f)) by A38, A41, A44, A46;
consider z1 being set such that
A48: z1 in LeftComp (SpStSeq (L~ f)) by XBOOLE_0:def 1;
LeftComp (SpStSeq (L~ f)) misses RightComp (SpStSeq (L~ f)) by SPRECT_1:88;
then A49: z1 <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A47, A48, XBOOLE_0:3;
reconsider z1 = z1 as Point of (TOP-REAL 2) by A48;
consider P being Subset of (TOP-REAL 2) such that
A50: P is_S-P_arc_joining z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) and
A51: P c= RightComp f by A2, A3, A18, A20, A21, A48, A49, TOPREAL4:29;
consider Red9 being FinSequence of (TOP-REAL 2) such that
A52: Red9 is being_S-Seq and
A53: P = L~ Red9 and
A54: z1 = Red9 /. 1 and
A55: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = Red9 /. (len Red9) by A50, TOPREAL4:def 1;
A56: L~ (SpStSeq (L~ f)) meets L~ Red9 by A47, A48, A52, A54, A55, SPRECT_3:33;
A57: 2 in dom f by A8, FINSEQ_3:25;
A58: len f in dom f by FINSEQ_5:6;
A59: (len f) -' 1 >= 1 by A8, NAT_D:49;
(len f) -' 1 <= len f by NAT_D:44;
then A60: (len f) -' 1 in dom f by A59, FINSEQ_3:25;
1 <= len f by A58, FINSEQ_3:25;
then A61: ((len f) -' 1) + 1 = len f by XREAL_1:235;
then A62: (len f) -' 1 < len f by NAT_1:13;
A63: <*(NW-corner (L~ f))*> is_in_the_area_of f by SPRECT_2:26;
A64: (width (GoB f)) -' 1 < width (GoB f) by A10, NAT_1:13;
then Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ (SpStSeq (L~ f)) by A4, A5, A19, SPRECT_3:55;
then A65: not (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ (SpStSeq (L~ f)) by A20, XBOOLE_0:3;
A66: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) c= L~ (SpStSeq (L~ f)) by SPRECT_3:14;
A67: f /. 1 = f /. (len f) by FINSEQ_6:def 1;
A68: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
A69: N-min (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by SPRECT_3:15;
then A70: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A68, TOPREAL1:6;
A72: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) is horizontal by A70, SPRECT_1:9;
1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then A73: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def 6;
len f >= 2 + 1 by GOBOARD7:34, XXREAL_0:2;
then (len f) -' 1 >= 1 + 1 by NAT_D:49;
then ((len f) -' 1) -' 1 >= 1 by NAT_D:49;
then A74: (len f) -' 2 >= 1 by NAT_D:45;
A75: ((len f) -' 2) + 1 = (((len f) -' 1) -' 1) + 1 by NAT_D:45
.= (len f) -' 1 by A59, XREAL_1:235 ;
((len f) -' 2) + 2 = len f by A7, XREAL_1:235, XXREAL_0:2;
then A76: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) = {(f /. ((len f) -' 1))} by A74, A75, TOPREAL1:def 6;
A77: f /. 2 in N-most (L~ f) by A1, SPRECT_2:30;
N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
then A78: LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A1, A69, A77, TOPREAL1:6;
A79: ((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by A4, A5, A19, A64, GOBOARD5:2
.= (N-min (L~ f)) `1 by A4, A5, A6, A9, GOBOARD5:2 ;
A80: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1
.= (N-min (L~ f)) `2 by A4, A5, A6, A9, GOBOARD5:1 ;
then A81: (f /. 2) `2 = N-bound (L~ f) by A17, EUCLID:52;
A82: <*((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by A9, A12, A13, SPRECT_3:49;
<*((GoB f) * (i,((width (GoB f)) -' 1)))*> is_in_the_area_of f by A4, A5, A19, A64, SPRECT_3:49;
then <*((GoB f) * (i,((width (GoB f)) -' 1))),((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by A82, SPRECT_3:42;
then <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by SPRECT_3:50;
then A83: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of SpStSeq (L~ f) by SPRECT_3:53;
A84: (GoB f) * (i,((width (GoB f)) -' 1)) = f /. ((len f) -' 1) by A1, A6, A16, SPRECT_3:29;
then LSeg ((N-min (L~ f)),(f /. ((len f) -' 1))) is vertical by A79, SPPOL_1:16;
then A85: (LSeg ((N-min (L~ f)),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) = {(N-min (L~ f))} by A70, SPRECT_1:9, SPRECT_3:10;
A86: (NW-corner (L~ f)) `2 = (N-min (L~ f)) `2 by PSCOMP_1:37;
A87: (NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:38;
(N-min (L~ f)) `1 <= (f /. 2) `1 by A77, PSCOMP_1:39;
then N-min (L~ f) in LSeg ((NW-corner (L~ f)),(f /. 2)) by A17, A80, A86, A87, GOBOARD7:8;
then A88: (LSeg ((N-min (L~ f)),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) = {(N-min (L~ f))} by TOPREAL1:8;
((GoB f) * (i,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A4, A5, A9, GOBOARD5:1
.= ((GoB f) * ((i + 1),(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1 ;
then (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) `2 = (((GoB f) * (i,((width (GoB f)) -' 1))) `2) + (((GoB f) * ((i + 1),(width (GoB f)))) `2) by TOPREAL3:2
.= (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2 by TOPREAL3:2 ;
then ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) by TOPREAL3:4
.= ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 by TOPREAL3:4 ;
then A89: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) is horizontal by SPPOL_1:15;
A90: f /. ((len f) -' 1) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by RLTOPSP1:68;
A91: (GoB f) * (i,(width (GoB f))) = f /. (len f) by A1, A6, FINSEQ_6:def 1;
(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = ((1 / 2) * ((GoB f) * (i,((width (GoB f)) -' 1)))) + ((1 - (1 / 2)) * ((GoB f) * (i,(width (GoB f))))) by EUCLID:32;
then A92: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by A84, A91;
then A93: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by A90, TOPREAL1:6;
LSeg ((f /. ((len f) -' 1)),(f /. (len f))) = LSeg (f,((len f) -' 1)) by A59, A61, TOPREAL1:def 3;
then A94: LSeg ((f /. ((len f) -' 1)),(f /. (len f))) c= L~ f by TOPREAL3:19;
then A95: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= L~ f by A93, XBOOLE_1:1;
A96: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= LSeg (f,((len f) -' 1)) by A59, A61, A93, TOPREAL1:def 3;
A97: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `1 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + (N-min (L~ f))) `1) by A6, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `1) + ((N-min (L~ f)) `1)) by A79, TOPREAL3:2
.= (N-min (L~ f)) `1 ;
then A98: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) is vertical by A79, A84, SPPOL_1:16;
A99: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by RLTOPSP1:68;
then A100: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in L~ f by A95;

A101: now

assume (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = N-min (L~ f) ; :: thesis: contradiction
then f /. ((len f) -' 1) = f /. (len f) by A1, A6, A67, A84, SPRECT_3:5;
hence contradiction by A58, A60, A61, GOBOARD7:29; :: thesis: verum

end;

(1 + 1) + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A102: 1 + 1 <= (len f) -' 1 by NAT_D:49;
then A103: 1 <= ((len f) -' 1) -' 1 by NAT_D:49;
A104: (((len f) -' 1) -' 1) + 1 = (len f) -' 1 by A102, XREAL_1:235, XXREAL_0:2;
A105: (((len f) -' 1) -' 1) + 2 = ((len f) -' 2) + 2 by NAT_D:45
.= len f by A7, XREAL_1:235, XXREAL_0:2 ;
A106: for i, j being Element of NAT st 1 <= i & i <= j & j < (len f) -' 1 holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))

proof

let l, j be Element of NAT ; :: thesis: ( 1 <= l & l <= j & j < (len f) -' 1 implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) )
assume that
A107: 1 <= l and
A108: l <= j and
A109: j < (len f) -' 1 ; :: thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))
assume L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) ; :: thesis: contradiction
then (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A110: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) by SUBSET_1:4;
p in L~ (mid (f,l,j)) by A110, XBOOLE_0:def 4;
then consider ii being Element of NAT such that
A111: 1 <= ii and
A112: ii + 1 <= len (mid (f,l,j)) and
A113: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
(len f) -' 1 > l by A108, A109, XXREAL_0:2;
then (len f) -' 1 > 1 by A107, XXREAL_0:2;
then A114: (len f) -' 1 < len f by NAT_D:51;
then A115: j < len f by A109, XXREAL_0:2;
then len (mid (f,l,j)) = (j -' l) + 1 by A107, A108, JORDAN4:8;
then A116: ii < (j -' l) + 1 by A112, NAT_1:13;
set k = (ii + l) -' 1;
A117: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A110, XBOOLE_0:def 4;

per cases ( l = j or l < j ) by A108, XXREAL_0:1;

suppose l = j ; :: thesis: contradiction

then len (mid (f,l,j)) = 1 by A107, A115, JORDAN4:15;
then L~ (mid (f,l,j)) = {} by TOPREAL1:22;
hence contradiction by A113, SPPOL_2:17; :: thesis: verum

end;

suppose A118: l < j ; :: thesis: contradiction

A119: ii + 1 >= 1 + 1 by A111, XREAL_1:6;
ii + l >= ii + 1 by A107, XREAL_1:6;
then A120: ii + l >= 1 + 1 by A119, XXREAL_0:2;
then A121: (ii + l) -' 1 >= 1 by NAT_D:49;
A122: ii + l >= 1 by A120, XXREAL_0:2;

A123: now

assume ((ii + l) -' 1) + 1 >= (len f) -' 1 ; :: thesis: contradiction
then (ii + l) -' 1 >= ((len f) -' 1) -' 1 by NAT_D:53;
then A124: ii + l >= (len f) -' 1 by A122, NAT_D:56;
ii + l < ((j -' l) + 1) + l by A116, XREAL_1:6;
then ii + l < ((j -' l) + l) + 1 ;
then ii + l < j + 1 by A118, XREAL_1:235;
then (len f) -' 1 < j + 1 by A124, XXREAL_0:2;
hence contradiction by A109, NAT_1:13; :: thesis: verum

end;

A125: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def 6 ;
LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A107, A115, A111, A116, A118, JORDAN4:19;
then A126: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A96, A117, A113, XBOOLE_0:def 4;
then LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
then (ii + l) -' 1 <= 1 by A114, A123, GOBOARD5:def 4;
then (ii + l) -' 1 = 1 by A121, XXREAL_0:1;
then p = f /. 1 by A126, A125, TARSKI:def 1;
hence contradiction by A1, A67, A92, A101, A117, SPRECT_3:6; :: thesis: verum

end;

end;

end;

A127: for j being Element of NAT st 1 <= j & j < (len f) -' 1 holds
(L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))}

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < (len f) -' 1 implies (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))} )
assume that
A128: 1 <= j and
A129: j < (len f) -' 1 ; :: thesis: (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))}
A130: 1 <= (len f) -' 1 by A128, A129, XXREAL_0:2;
A131: ((len f) -' 1) -' 1 = (len f) -' 2 by NAT_D:45;
then A132: L~ (mid (f,j,((len f) -' 1))) = (LSeg (f,((len f) -' 2))) \/ (L~ (mid (f,j,((len f) -' 2)))) by A128, A129, NAT_D:35, SPRECT_3:20;
j <= (len f) -' 2 by A129, A131, NAT_D:49;
then LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ (mid (f,j,((len f) -' 2))) by A106, A128, A130, A131, JORDAN5B:1;
hence (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = (LSeg (f,((len f) -' 2))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) by A132, XBOOLE_1:78
.= {(f /. ((len f) -' 1))} by A76, A96, RLTOPSP1:68, ZFMISC_1:124 ;
:: thesis: verum

end;

A133: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))

proof

assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) ; :: thesis: contradiction
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A134: p in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) by SUBSET_1:4;
A135: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A134, XBOOLE_0:def 4;
p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A134, XBOOLE_0:def 4;
then p in {(N-min (L~ f))} by A1, A67, A85, A93, A135, XBOOLE_0:def 4;
then p = N-min (L~ f) by TARSKI:def 1;
hence contradiction by A1, A67, A92, A101, A135, SPRECT_3:6; :: thesis: verum

end;

A136: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 <> (N-min (L~ f)) `2 by A97, A101, TOPREAL3:6;
set G = GoB f;
A137: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;
(L~ f) /\ ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) = ((L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1))))) \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) by XBOOLE_1:23
.= {} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) by A137, XBOOLE_0:def 7
.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} ;
then A138: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ f) c= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A4, A5, A10, A19, A64, GOBOARD6:40, XBOOLE_1:26;
(L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by XBOOLE_1:17;
then A139: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ f) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A138, XBOOLE_1:1;
A140: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))

proof

len f >= 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A141: (len f) -' 1 >= 1 by NAT_D:49;
let l, j be Element of NAT ; :: thesis: ( 1 <= l & l < j & j < len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) )
assume that
A142: 1 <= l and
A143: l < j and
A144: j < len f ; :: thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
assume L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) ; :: thesis: contradiction
then (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A145: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by SUBSET_1:4;
p in L~ (mid (f,l,j)) by A145, XBOOLE_0:def 4;
then consider ii being Element of NAT such that
A146: 1 <= ii and
A147: ii + 1 <= len (mid (f,l,j)) and
A148: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A149: len (mid (f,l,j)) = (j -' l) + 1 by A142, A143, A144, JORDAN4:8;
then ii < (j -' l) + 1 by A147, NAT_1:13;
then A150: p in LSeg (f,((ii + l) -' 1)) by A142, A143, A144, A146, A148, JORDAN4:19;
set k = (ii + l) -' 1;
A151: ii + 1 >= 1 + 1 by A146, XREAL_1:6;
(LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) c= (L~ f) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by TOPREAL3:19, XBOOLE_1:26;
then A152: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A139, XBOOLE_1:1;
p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A145, XBOOLE_0:def 4;
then p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by A150, XBOOLE_0:def 4;
then p = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A152, TARSKI:def 1;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg ((f /. ((len f) -' 1)),(f /. (len f)))) by A92, A150, XBOOLE_0:def 4;
then A153: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A61, A141, TOPREAL1:def 3;
then A154: LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
ii + l >= ii + 1 by A142, XREAL_1:6;
then ii + l >= 1 + 1 by A151, XXREAL_0:2;
then A155: (ii + l) -' 1 >= 1 by NAT_D:49;

per cases ( (ii + l) -' 1 <= 1 or ((ii + l) -' 1) + 1 >= (len f) -' 1 ) by A62, A154, GOBOARD5:def 4;

suppose A156: (ii + l) -' 1 <= 1 ; :: thesis: contradiction

A157: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def 6 ;
(ii + l) -' 1 = 1 by A155, A156, XXREAL_0:1;
hence contradiction by A1, A101, A153, A157, TARSKI:def 1; :: thesis: verum

end;

suppose A158: ((ii + l) -' 1) + 1 >= (len f) -' 1 ; :: thesis: contradiction

ii <= j -' l by A147, A149, XREAL_1:6;
then ii + l <= j by A143, NAT_D:54;
then A159: ii + l < len f by A144, XXREAL_0:2;
ii + l >= l by NAT_1:11;
then ii + l >= 1 by A142, XXREAL_0:2;
then (ii + l) -' 1 < (len f) -' 1 by A159, NAT_D:56;
then A160: (ii + l) -' 1 <= ((len f) -' 1) -' 1 by NAT_D:49;
(ii + l) -' 1 >= ((len f) -' 1) -' 1 by A158, NAT_D:53;
then (ii + l) -' 1 = ((len f) -' 1) -' 1 by A160, XXREAL_0:1;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in {(f /. ((len f) -' 1))} by A103, A104, A105, A153, TOPREAL1:def 6;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = f /. ((len f) -' 1) by TARSKI:def 1;
hence contradiction by A6, A84, A101, SPRECT_3:5; :: thesis: verum

end;

end;

end;

A161: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> is_in_the_area_of f by A95, A99, SPRECT_2:21, SPRECT_3:46;
then A162: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> is_in_the_area_of SpStSeq (L~ f) by SPRECT_3:53;
<*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> = <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> by FINSEQ_1:def 9;
then A163: (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A65, A83, A162, SPRECT_2:24, SPRECT_3:47;
((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by A4, A5, A19, GOBOARD5:2, NAT_D:35
.= ((GoB f) * (i,(width (GoB f)))) `1 by A4, A5, A9, GOBOARD5:2 ;
then (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 = (((GoB f) * (i,((width (GoB f)) -' 1))) `1) + (((GoB f) * ((i + 1),(width (GoB f)))) `1) by TOPREAL3:2
.= (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 by TOPREAL3:2 ;
then ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1) by TOPREAL3:4
.= ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by TOPREAL3:4 ;
then A164: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) is vertical by SPPOL_1:16;
A165: f /. 2 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
(1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) = ((1 / 2) * ((GoB f) * (i,(width (GoB f))))) + ((1 - (1 / 2)) * ((GoB f) * ((i + 1),(width (GoB f))))) by EUCLID:32;
then A166: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg ((f /. 1),(f /. 2)) by A1, A6, A17;
then A167: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= LSeg ((f /. 1),(f /. 2)) by A165, TOPREAL1:6;
A168: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by A8, TOPREAL1:def 3;
then A169: LSeg ((f /. 1),(f /. 2)) c= L~ f by TOPREAL3:19;
then A170: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= L~ f by A167, XBOOLE_1:1;
A171: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) by A6, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-min (L~ f)) `2)) by A80, TOPREAL3:2
.= N-bound (L~ f) by EUCLID:52 ;
A172: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
A173: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) <> N-min (L~ f) by A1, A6, A15, A17, A57, GOBOARD7:29, SPRECT_3:5;
A174: for i, j being Element of NAT st 2 < i & i <= j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))

proof

let l, j be Element of NAT ; :: thesis: ( 2 < l & l <= j & j <= len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) )
assume that
A175: 2 < l and
A176: l <= j and
A177: j <= len f ; :: thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))
assume L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) ; :: thesis: contradiction
then (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A178: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) by SUBSET_1:4;
A179: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A178, XBOOLE_0:def 4;
p in L~ (mid (f,l,j)) by A178, XBOOLE_0:def 4;
then consider ii being Element of NAT such that
A180: 1 <= ii and
A181: ii + 1 <= len (mid (f,l,j)) and
A182: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A183: 1 < l by A175, XXREAL_0:2;
then A184: len (mid (f,l,j)) = (j -' l) + 1 by A176, A177, JORDAN4:8;
then A185: ii < (j -' l) + 1 by A181, NAT_1:13;
set k = (ii + l) -' 1;
A186: ii + 2 >= 1 + 2 by A180, XREAL_1:6;
ii + l > ii + 2 by A175, XREAL_1:6;
then ii + l > 1 + 2 by A186, XXREAL_0:2;
then A187: (ii + l) -' 1 > 1 + 1 by NAT_D:52;

per cases ( l = j or l < j ) by A176, XXREAL_0:1;

suppose l = j ; :: thesis: contradiction

then len (mid (f,l,j)) = 1 by A177, A183, JORDAN4:15;
then L~ (mid (f,l,j)) = {} by TOPREAL1:22;
hence contradiction by A182, SPPOL_2:17; :: thesis: verum

end;

suppose A188: l < j ; :: thesis: contradiction

A189: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def 6 ;
ii <= j -' l by A181, A184, XREAL_1:6;
then ii + l <= j by A176, NAT_D:54;
then ii + l <= len f by A177, XXREAL_0:2;
then A190: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A177, A183, A180, A185, A188, JORDAN4:19;
then A191: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A167, A168, A179, A182, XBOOLE_0:def 4;
then LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;
then ((ii + l) -' 1) + 1 >= len f by A187, GOBOARD5:def 4;
then (ii + l) -' 1 >= (len f) -' 1 by NAT_D:53;
then (ii + l) -' 1 = (len f) -' 1 by A190, XXREAL_0:1;
then p = f /. 1 by A191, A189, TARSKI:def 1;
hence contradiction by A1, A166, A173, A179, SPRECT_3:6; :: thesis: verum

end;

end;

end;

A192: for j being Element of NAT st 2 < j & j <= len f holds
(L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)}

proof

A193: f /. 2 in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
let j be Element of NAT ; :: thesis: ( 2 < j & j <= len f implies (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)} )
assume that
A194: 2 < j and
A195: j <= len f ; :: thesis: (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)}
2 + 1 <= j by A194, NAT_1:13;
then A196: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ (mid (f,(2 + 1),j)) by A174, A195;
L~ (mid (f,2,j)) = (LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),j))) by A194, A195, SPRECT_3:19;
hence (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = (LSeg (f,2)) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) by A196, XBOOLE_1:78
.= {(f /. 2)} by A73, A165, A166, A168, A193, TOPREAL1:6, ZFMISC_1:124 ;
:: thesis: verum

end;

A197: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))

proof

assume LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) meets LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; :: thesis: contradiction
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A198: p in (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) by SUBSET_1:4;
A199: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A198, XBOOLE_0:def 4;
p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A198, XBOOLE_0:def 4;
then p in {(N-min (L~ f))} by A1, A88, A167, A199, XBOOLE_0:def 4;
then p = N-min (L~ f) by TARSKI:def 1;
hence contradiction by A1, A166, A173, A199, SPRECT_3:6; :: thesis: verum

end;

A200: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))

proof

assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A201: p in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by SUBSET_1:4;
A202: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A201, XBOOLE_0:def 4;
A203: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A201, XBOOLE_0:def 4;
(LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A78, A164, A166, SPRECT_3:11;
then p in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A70, A203, A202, XBOOLE_0:def 4;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A203, TARSKI:def 1;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) by A170, A172, XBOOLE_0:def 4;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in {(N-min (L~ f))} by PSCOMP_1:43;
hence contradiction by A173, TARSKI:def 1; :: thesis: verum

end;

A204: for i, j being Element of NAT st 1 < i & i < j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))

proof

A205: len f >= 2 by GOBOARD7:34, XXREAL_0:2;
A206: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;
A207: (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by XBOOLE_1:17;
let l, j be Element of NAT ; :: thesis: ( 1 < l & l < j & j <= len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) )
assume that
A208: 1 < l and
A209: l < j and
A210: j <= len f ; :: thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
assume L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
A211: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by SUBSET_1:4;
p in L~ (mid (f,l,j)) by A211, XBOOLE_0:def 4;
then consider ii being Element of NAT such that
A212: 1 <= ii and
A213: ii + 1 <= len (mid (f,l,j)) and
A214: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A215: len (mid (f,l,j)) = (j -' l) + 1 by A208, A209, A210, JORDAN4:8;
then ii < (j -' l) + 1 by A213, NAT_1:13;
then A216: p in LSeg (f,((ii + l) -' 1)) by A208, A209, A210, A212, A214, JORDAN4:19;
set k = (ii + l) -' 1;
set G = GoB f;
A217: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= (L~ f) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by TOPREAL3:19, XBOOLE_1:26;
(L~ f) /\ ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) = ((L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1))))) \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) by XBOOLE_1:23
.= {} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) by A206, XBOOLE_0:def 7
.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} ;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ f) c= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A4, A5, A10, A19, A64, GOBOARD6:41, XBOOLE_1:26;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ f) c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A207, XBOOLE_1:1;
then A218: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A217, XBOOLE_1:1;
p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A211, XBOOLE_0:def 4;
then p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A216, XBOOLE_0:def 4;
then p = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A218, TARSKI:def 1;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg ((f /. 1),(f /. (1 + 1)))) by A166, A216, XBOOLE_0:def 4;
then A219: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A205, TOPREAL1:def 3;
then LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;
then A220: ( (ii + l) -' 1 <= 1 + 1 or ((ii + l) -' 1) + 1 >= len f ) by GOBOARD5:def 4;
A221: ii + 1 >= 1 + 1 by A212, XREAL_1:6;
ii + l > ii + 1 by A208, XREAL_1:6;
then ii + l > 1 + 1 by A221, XXREAL_0:2;
then A222: (ii + l) -' 1 > 1 by NAT_D:52;

per cases ( (ii + l) -' 1 <= 2 or ((ii + l) -' 1) + 1 >= len f ) by A220;

suppose A223: (ii + l) -' 1 <= 2 ; :: thesis: contradiction

(ii + l) -' 1 >= 1 + 1 by A222, NAT_1:13;
then A224: (ii + l) -' 1 = 2 by A223, XXREAL_0:1;
1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in {(f /. (1 + 1))} by A219, A224, TOPREAL1:def 6;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) = f /. (1 + 1) by TARSKI:def 1;
hence contradiction by A6, A17, A173, SPRECT_3:5; :: thesis: verum

end;

suppose A225: ((ii + l) -' 1) + 1 >= len f ; :: thesis: contradiction

A226: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def 6 ;
ii <= j -' l by A213, A215, XREAL_1:6;
then ii + l <= j by A209, NAT_D:54;
then ii + l <= len f by A210, XXREAL_0:2;
then A227: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
(ii + l) -' 1 >= (len f) -' 1 by A225, NAT_D:53;
then (ii + l) -' 1 = (len f) -' 1 by A227, XXREAL_0:1;
hence contradiction by A1, A173, A219, A226, TARSKI:def 1; :: thesis: verum

end;

end;

end;

LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A1, SPRECT_3:31;
then A228: (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A65, A83, A166, SPRECT_3:48;
A229: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) is horizontal by A81, A171, SPPOL_1:15;
A230: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
then A231: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ f by A170;
A232: <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by A170, A230, SPRECT_2:21, SPRECT_3:46;
A233: L~ f misses L~ Red9 by A51, A53, SPRECT_3:25, XBOOLE_1:63;
reconsider Red9 = Red9 as S-Sequence_in_R2 by A52;
len Red9 in dom Red9 by FINSEQ_5:6;
then A234: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red9 by A55, SPPOL_2:44;
set u1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))));
set Red = L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))));
set u2 = First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))));
set u3 = First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))));
NW-corner (L~ (SpStSeq (L~ f))) = NW-corner (L~ f) by SPRECT_1:62;
then A235: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> NW-corner (L~ f) by A47, A48, A54, A55, SPRECT_3:38;
A236: L~ Red9 is_an_arc_of z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A54, A55, TOPREAL1:25;
(L~ Red9) /\ (L~ (SpStSeq (L~ f))) is closed by TOPS_1:8;
then A237: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A236, JORDAN5C:def 2;
then A238: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def 4;
A239: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red9 by A237, XBOOLE_0:def 4;

A240: now

assume Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ f ; :: thesis: contradiction
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ f) /\ (L~ Red9) by A239, XBOOLE_0:def 4;
hence contradiction by A233, XBOOLE_0:def 7; :: thesis: verum

end;

len Red9 in dom Red9 by FINSEQ_5:6;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> Red9 . (len Red9) by A55, A65, A238, PARTFUN1:def 6;
then reconsider Red = L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) as S-Sequence_in_R2 by A239, JORDAN3:34;
1 in dom Red by FINSEQ_5:6;
then A241: Red /. 1 = Red . 1 by PARTFUN1:def 6
.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A239, JORDAN3:23 ;
A242: (L~ (SpStSeq (L~ f))) /\ (L~ Red) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A55, A56, A65, Th6;
len Red9 in dom Red9 by FINSEQ_5:6;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = Red9 . (len Red9) by A55, PARTFUN1:def 6;
then A243: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red by A65, A234, A238, A239, JORDAN5B:22;
Red is_in_the_area_of SpStSeq (L~ f) by A47, A48, A54, A55, SPRECT_3:54;
then A244: Red is_in_the_area_of f by SPRECT_3:53;
A245: L~ Red c= L~ Red9 by A239, JORDAN3:42;
A246: L~ f misses L~ Red by A233, A239, JORDAN3:42, XBOOLE_1:63;
(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A247: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) meets L~ Red by A243, XBOOLE_0:3;
(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A248: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) meets L~ Red by A243, XBOOLE_0:3;
A249: (L~ Red) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is closed by TOPS_1:8;
A250: (L~ Red) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is closed by TOPS_1:8;
L~ Red is_an_arc_of Red /. 1,Red /. (len Red) by TOPREAL1:25;
then A251: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) by A248, A250, JORDAN5C:def 1;
then A252: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ Red by XBOOLE_0:def 4;
A253: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A251, XBOOLE_0:def 4;
A254: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A95, A99, A233, A245, A252, XBOOLE_0:3;
A255: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A256: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) c= LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A253, TOPREAL1:6;
then A257: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A72, A89, A136, SPRECT_3:9, XBOOLE_1:63;
A258: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))

proof

let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j < len f implies L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) )
assume that
A259: 1 <= i and
A260: i < j and
A261: j < len f ; :: thesis: L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A140, A259, A260, A261;
hence L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A253, A255, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum

end;

A262: now

A263: 1 in dom Red by FINSEQ_5:6;
assume First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) = Red . 1 ; :: thesis: contradiction
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ (SpStSeq (L~ f)) by A238, A241, A263, PARTFUN1:def 6;
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ (SpStSeq (L~ f))) by A253, XBOOLE_0:def 4;
hence contradiction by A163, A254, TARSKI:def 1; :: thesis: verum

end;

L~ Red is_an_arc_of Red /. 1,Red /. (len Red) by TOPREAL1:25;
then A264: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) by A247, A249, JORDAN5C:def 1;
then A265: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red by XBOOLE_0:def 4;
A266: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A264, XBOOLE_0:def 4;
A267: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A170, A230, A233, A245, A265, XBOOLE_0:3;
A268: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A269: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) c= LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A266, TOPREAL1:6;
A270: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A200, A266, A268, TOPREAL1:6, XBOOLE_1:63;
A271: for i, j being Element of NAT st 1 < i & i < j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i < j & j <= len f implies L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) )
assume that
A272: 1 < i and
A273: i < j and
A274: j <= len f ; :: thesis: L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A204, A272, A273, A274;
hence L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A266, A268, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum

end;

A275: now

A276: 1 in dom Red by FINSEQ_5:6;
assume First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) = Red . 1 ; :: thesis: contradiction
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ (SpStSeq (L~ f)) by A238, A241, A276, PARTFUN1:def 6;
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A228, A266, XBOOLE_0:def 4;
hence contradiction by A267, TARSKI:def 1; :: thesis: verum

end;

reconsider Red2 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) as S-Sequence_in_R2 by A252, A262, JORDAN3:35;
A278: Red2 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A241, A252, SPRECT_3:22;
A279: len Red2 in dom Red2 by FINSEQ_5:6;
A280: (Rev Red2) /. 1 = Red2 /. (len Red2) by FINSEQ_5:65
.= Red2 . (len Red2) by A279, PARTFUN1:def 6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A252, JORDAN3:24 ;
then A281: ((Rev Red2) /. 1) `2 = ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 by A89, A253, SPPOL_1:40;
A282: (Rev Red2) /. 1 <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A95, A99, A233, A245, A252, A280, XBOOLE_0:3;
A283: L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
A284: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ Red2 by A252, A262, JORDAN5B:20;
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) by RLTOPSP1:68;
then A285: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (L~ Red2) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A284, XBOOLE_0:def 4;

now

assume Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A238, XBOOLE_0:def 4;
hence contradiction by A100, A163, A240, TARSKI:def 1; :: thesis: verum

end;

then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A241, A248, Th1;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A253, A255, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A285, ZFMISC_1:33;
then reconsider RB2 = <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ (Rev Red2) as S-Sequence_in_R2 by A280, A281, A282, A283, SPRECT_3:16;
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red by A93, A94, A246, XBOOLE_1:1, XBOOLE_1:63;
then LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red2 by A252, JORDAN3:41, XBOOLE_1:63;
then A286: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ Red2) = {} by XBOOLE_0:def 7;
1 in dom Red2 by FINSEQ_5:6;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red2 by A278, SPPOL_2:44;
then A287: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red2) by A238, XBOOLE_0:def 4;
(L~ (SpStSeq (L~ f))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A242, A252, JORDAN3:41, XBOOLE_1:26;
then A288: (L~ (SpStSeq (L~ f))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A287, ZFMISC_1:33;
reconsider Red1 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) as S-Sequence_in_R2 by A265, A275, JORDAN3:35;
len Red1 in dom Red1 by FINSEQ_5:6;
then A289: Red1 /. (len Red1) = Red1 . (len Red1) by PARTFUN1:def 6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A265, JORDAN3:24 ;
A290: Red1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A241, A265, SPRECT_3:22;
A291: (Red1 /. (len Red1)) `1 = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by A164, A266, A289, SPPOL_1:41;
A292: Red1 /. (len Red1) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A170, A230, A233, A245, A265, A289, XBOOLE_0:3;
A293: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red1 by A265, A275, JORDAN5B:20;
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) by RLTOPSP1:68;
then A294: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (L~ Red1) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) by A293, XBOOLE_0:def 4;

now

assume Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A238, XBOOLE_0:def 4;
hence contradiction by A228, A231, A240, TARSKI:def 1; :: thesis: verum

end;

then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A241, A247, Th1;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A266, A268, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A294, ZFMISC_1:33;
then reconsider RB1 = Red1 ^ <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> as S-Sequence_in_R2 by A289, A291, A292, SPRECT_2:61;
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red by A167, A169, A246, XBOOLE_1:1, XBOOLE_1:63;
then LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red1 by A265, JORDAN3:41, XBOOLE_1:63;
then A295: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ Red1) = {} by XBOOLE_0:def 7;
1 in dom Red1 by FINSEQ_5:6;
then A296: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red1 by A290, SPPOL_2:44;
then A297: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red1) by A238, XBOOLE_0:def 4;
(L~ (SpStSeq (L~ f))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A242, A265, JORDAN3:41, XBOOLE_1:26;
then A298: (L~ (SpStSeq (L~ f))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A297, ZFMISC_1:33;
len (Rev Red2) = len Red2 by FINSEQ_5:def 3;
then A299: RB2 /. (len RB2) = (Rev Red2) /. (len Red2) by SPRECT_3:1
.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A278, FINSEQ_5:65 ;
A300: RB2 /. 1 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by FINSEQ_5:15;
L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
then A301: L~ RB2 = (L~ Red2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A280, SPPOL_2:20;
then A302: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ RB2) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A286, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A89, A98, A256, SPRECT_1:9, SPRECT_3:10 ;
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))*> is_in_the_area_of f by A244, A252, SPRECT_3:46;
then Red2 is_in_the_area_of f by A244, A252, SPRECT_3:52;
then Rev Red2 is_in_the_area_of f by SPRECT_3:51;
then A303: RB2 is_in_the_area_of f by A161, SPRECT_2:24;
1 in dom Red1 by FINSEQ_5:6;
then A304: RB1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A290, FINSEQ_4:68;
len <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> = 1 by FINSEQ_1:39;
then len RB1 = (len Red1) + 1 by FINSEQ_1:22;
then A305: RB1 /. (len RB1) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by FINSEQ_4:67;
A306: L~ RB1 = (L~ Red1) \/ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A289, SPPOL_2:19;
then A307: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A295, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A164, A229, A269, SPRECT_1:10, SPRECT_3:10 ;
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))*> is_in_the_area_of f by A244, A265, SPRECT_3:46;
then Red1 is_in_the_area_of f by A244, A265, SPRECT_3:52;
then A308: RB1 is_in_the_area_of f by A232, SPRECT_2:24;
A309: L~ Red9 is_an_arc_of z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A50, A53, TOPREAL4:2;
(L~ Red9) /\ (L~ (SpStSeq (L~ f))) is closed by TOPS_1:8;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A309, JORDAN5C:def 2;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def 4;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by SPRECT_1:41;
then A310: ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def 3;
A311: N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
A312: N-min (L~ f) in N-most (L~ f) by PSCOMP_1:42;
then LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) = (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) \/ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A311, TOPREAL1:5;
then A313: ( not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) ) by XBOOLE_0:def 3;

per cases ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) = NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) <> NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) = W-max (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) <> W-max (L~ f) ) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by A310, A313, XBOOLE_0:def 3;

suppose A314: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; :: thesis: contradiction

A315: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A311, A312, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A314, A315, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A316: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A298, XBOOLE_1:26;
A317: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A318: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A314, TOPREAL1:6, XBOOLE_1:63;
then A319: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {} by XBOOLE_0:def 7;
Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by RLTOPSP1:68;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by A296, XBOOLE_0:def 4;
then {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} c= (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by ZFMISC_1:31;
then (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A316, XBOOLE_0:def 10;
then A320: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ RB1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} \/ {} by A306, A319, XBOOLE_1:23
.= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} ;
(NW-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
then (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 = (NW-corner (L~ f)) `2 by A314, A317, GOBOARD7:6;
then reconsider M3 = <*(NW-corner (L~ f))*> ^ RB1 as S-Sequence_in_R2 by A235, A304, A320, SPRECT_3:16;
A321: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
set i1 = (S-min (L~ f)) .. f;
set i2 = (E-min (L~ f)) .. f;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (N-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then 2 <= (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
then A322: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A197, A314, A318, TOPREAL1:6, XBOOLE_1:63;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) = {} by XBOOLE_0:def 7;
then A323: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M3) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1)) by A304, A321, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A307 ;
A324: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
(W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A325: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
A326: E-min (L~ f) in rng f by SPRECT_2:45;
then A327: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A328: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M4 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A322, JORDAN4:40;
L~ M4 misses L~ Red by A57, A246, A327, SPRECT_3:18, XBOOLE_1:63;
then A329: L~ M4 misses L~ Red1 by A265, JORDAN3:41, XBOOLE_1:63;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A330: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A331: 2 < (S-min (L~ f)) .. f by A322, XXREAL_0:2;
then 1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A325, JORDAN4:40;
A332: L~ M1 misses L~ M4 by A330, A325, A322, SPRECT_2:47;
A333: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A174, A325, A331;
A334: len M1 >= 2 by TOPREAL1:def 8;
A335: M4 /. 1 = f /. 2 by A57, A327, SPRECT_2:8;
L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A271, A322, A328;
then A336: L~ RB1 misses L~ M4 by A306, A329, XBOOLE_1:70;
A337: LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A314, A318, TOPREAL1:6;

A338: now

A339: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
assume L~ f meets LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) ; :: thesis: contradiction
then consider u being set such that
A340: u in L~ f and
A341: u in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by XBOOLE_0:3;
reconsider u = u as Point of (TOP-REAL 2) by A340;
u in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) by A337, A340, A341, XBOOLE_0:def 4;
then u = N-min (L~ f) by A339, TARSKI:def 1;
hence contradiction by A240, A314, A340, A341, SPRECT_3:6; :: thesis: verum

end;

then L~ M4 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A57, A327, SPRECT_3:18, XBOOLE_1:63;
then A342: L~ M3 misses L~ M4 by A304, A321, A336, XBOOLE_1:70;
A343: S-min (L~ f) in rng f by SPRECT_2:41;
then A344: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A345: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A346: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A344, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def 1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A344, SPRECT_2:8
.= (S-min (L~ f)) `2 by A343, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A347: M1 is_a_v.c._for f by A345, A346, SPRECT_2:def 3;
A348: <*(NW-corner (L~ f))*> ^ RB1 is_in_the_area_of f by A63, A308, SPRECT_2:24;
1 < (S-min (L~ f)) .. f by A331, XXREAL_0:2;
then A349: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A271, A325;
A350: M3 /. (len M3) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A305, SPRECT_3:1;
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M4) = {(f /. 2)} by A192, A322, A328;
then reconsider M2 = M3 ^ M4 as S-Sequence_in_R2 by A81, A171, A350, A335, A342, A323, SPRECT_3:21;
M2 = <*(NW-corner (L~ f))*> ^ (RB1 ^ (mid (f,2,((E-min (L~ f)) .. f)))) by FINSEQ_1:32;
then A351: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;
mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A327, SPRECT_2:23;
then A352: M2 is_in_the_area_of f by A348, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A327, SPRECT_2:9
.= (E-min (L~ f)) `1 by A326, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A353: M2 is_a_h.c._for f by A352, A351, SPRECT_2:def 2;
A354: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1)))) \/ (L~ M4) by SPPOL_2:23;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A334, A347, A353, SPRECT_2:29;
then L~ M1 meets (L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1))) by A354, A332, XBOOLE_1:70;
then A355: L~ M1 meets L~ M3 by A350, A335, A333, XBOOLE_1:70;
L~ M1 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A58, A344, A338, SPRECT_3:18, XBOOLE_1:63;
then L~ M1 meets L~ RB1 by A304, A355, A324, XBOOLE_1:70;
then L~ M1 meets L~ Red1 by A306, A349, XBOOLE_1:70;
then L~ M1 meets L~ Red by A265, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A58, A246, A344, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose that A356: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A357: N-min (L~ f) = NW-corner (L~ f) ; :: thesis: contradiction

set i1 = (S-max (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A358: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
(S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
then (S-max (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then ((S-max (L~ f)) .. f) + 1 <= (W-min (L~ f)) .. f by NAT_1:13;
then ((S-max (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:76, XXREAL_0:2;
then A359: (S-max (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
(E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then A360: (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A361: 1 < (S-max (L~ f)) .. f by A358, XXREAL_0:2;
then reconsider M4 = mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A359, JORDAN4:39;
A362: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A258, A359, A361;
(S-max (L~ f)) .. f < len f by A359, NAT_D:44;
then A363: (E-max (L~ f)) .. f < len f by A360, XXREAL_0:2;
then ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M2 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A358, JORDAN4:39;
A364: L~ M2 misses L~ M4 by A62, A360, A359, A358, SPRECT_2:47;
(E-max (L~ f)) .. f < (len f) -' 1 by A360, A359, XXREAL_0:2;
then A365: L~ M2 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A106, A358;
A366: len M2 >= 2 by TOPREAL1:def 8;
A367: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A258, A358, A363;
A368: E-max (L~ f) in rng f by SPRECT_2:46;
then A369: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A370: (M2 /. (len M2)) `1 = (f /. ((E-max (L~ f)) .. f)) `1 by A15, SPRECT_2:9
.= (E-max (L~ f)) `1 by A368, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
A371: S-max (L~ f) in rng f by SPRECT_2:42;
then A372: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then L~ M4 misses L~ Red by A60, A246, SPRECT_3:18, XBOOLE_1:63;
then L~ M4 misses L~ Red2 by A252, JORDAN3:41, XBOOLE_1:63;
then A373: L~ RB2 misses L~ M4 by A301, A362, XBOOLE_1:70;
A374: M2 is_in_the_area_of f by A15, A369, SPRECT_2:23;
(M2 /. 1) `1 = (f /. 1) `1 by A15, A369, SPRECT_2:8
.= W-bound (L~ f) by A1, A357, EUCLID:52 ;
then A375: M2 is_a_h.c._for f by A374, A370, SPRECT_2:def 2;
A376: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A377: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A378: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A372, SPRECT_2:9;
then (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A127, A359, A361;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A79, A84, A97, A300, A302, A378, A373, SPRECT_3:21;
mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A372, SPRECT_2:23;
then A379: M1 is_in_the_area_of f by A303, SPRECT_2:24;
A380: (M1 /. (len M1)) `2 = (RB2 /. (len RB2)) `2 by SPRECT_3:1
.= N-bound (L~ f) by A299, A356, A377, A376, GOBOARD7:6 ;
not mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is empty by A60, A372, SPRECT_2:7;
then 1 in dom (mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-max (L~ f)) .. f)) `2 by A60, A372, SPRECT_2:8
.= (S-max (L~ f)) `2 by A371, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A381: M1 is_a_v.c._for f by A379, A380, SPRECT_2:def 3;
A382: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A300, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
len M1 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A366, A381, A375, SPRECT_2:29;
then L~ M2 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A382, A364, XBOOLE_1:70;
then L~ M2 meets L~ RB2 by A378, A365, XBOOLE_1:70;
then L~ M2 meets L~ Red2 by A301, A367, XBOOLE_1:70;
then L~ M2 meets L~ Red by A252, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A15, A246, A369, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose that A383: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A384: N-min (L~ f) <> NW-corner (L~ f) ; :: thesis: contradiction

set i1 = (S-min (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
A385: (S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
W-max (L~ f) <> N-min (L~ f) by A384, PSCOMP_1:61;
then (S-min (L~ f)) .. f < (W-max (L~ f)) .. f by A1, A385, SPRECT_2:75, XXREAL_0:2;
then ((S-min (L~ f)) .. f) + 1 <= (W-max (L~ f)) .. f by NAT_1:13;
then ((S-min (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:77, XXREAL_0:2;
then A386: (S-min (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
A387: N-min (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
A388: (N-min (L~ f)) `2 = (NW-corner (L~ f)) `2 by PSCOMP_1:37;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A389: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
(E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A390: (E-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A391: 1 < (S-min (L~ f)) .. f by A389, XXREAL_0:2;
then reconsider M4 = mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A386, JORDAN4:39;
A392: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A258, A386, A391;
(S-min (L~ f)) .. f < len f by A386, NAT_D:44;
then A393: (E-max (L~ f)) .. f < len f by A390, XXREAL_0:2;
then ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M3 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A389, JORDAN4:39;
A394: L~ M3 misses L~ M4 by A62, A390, A386, A389, SPRECT_2:47;
(E-max (L~ f)) .. f < (len f) -' 1 by A390, A386, XXREAL_0:2;
then A395: L~ M3 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A106, A389;
A396: L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A258, A389, A393;
A397: E-max (L~ f) in rng f by SPRECT_2:46;
then A398: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A399: M3 /. 1 = N-min (L~ f) by A1, A15, SPRECT_2:8;
A400: S-min (L~ f) in rng f by SPRECT_2:41;
then A401: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then L~ M4 misses L~ Red by A60, A246, SPRECT_3:18, XBOOLE_1:63;
then L~ M4 misses L~ Red2 by A252, JORDAN3:41, XBOOLE_1:63;
then A402: L~ RB2 misses L~ M4 by A301, A392, XBOOLE_1:70;
A403: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A401, SPRECT_2:9;
then (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A127, A386, A391;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A79, A84, A97, A300, A302, A403, A402, SPRECT_3:21;
A404: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A300, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
1 in dom M3 by FINSEQ_5:6;
then N-min (L~ f) in L~ M3 by A399, SPPOL_2:44;
then N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by A387, XBOOLE_0:def 4;
then A405: {(N-min (L~ f))} c= (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by ZFMISC_1:31;
A406: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) c= {(N-min (L~ f))} by A15, A398, SPRECT_3:18, XBOOLE_1:26;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) = {(N-min (L~ f))} by A405, XBOOLE_0:def 10;
then reconsider M2 = <*(NW-corner (L~ f))*> ^ M3 as S-Sequence_in_R2 by A384, A388, A399, SPRECT_3:16;
A407: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;

A408: now

assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ M4 ; :: thesis: contradiction
then A409: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) <> {} by XBOOLE_0:def 7;
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) c= {(N-min (L~ f))} by A60, A401, A406, SPRECT_3:18, XBOOLE_1:26;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) = {(N-min (L~ f))} by A409, ZFMISC_1:33;
then N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) by TARSKI:def 1;
then N-min (L~ f) in L~ M4 by XBOOLE_0:def 4;
hence contradiction by A1, A62, A386, A391, SPRECT_3:30; :: thesis: verum

end;

A410: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A411: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
mid (f,1,((E-max (L~ f)) .. f)) is_in_the_area_of f by A15, A398, SPRECT_2:23;
then A412: M2 is_in_the_area_of f by A63, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,1,((E-max (L~ f)) .. f))) /. (len (mid (f,1,((E-max (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-max (L~ f)) .. f)) `1 by A15, A398, SPRECT_2:9
.= (E-max (L~ f)) `1 by A397, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A413: M2 is_a_h.c._for f by A412, A407, SPRECT_2:def 2;
A414: L~ M2 = (LSeg ((NW-corner (L~ f)),(M3 /. 1))) \/ (L~ M3) by SPPOL_2:20;
mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A401, SPRECT_2:23;
then A415: M1 is_in_the_area_of f by A303, SPRECT_2:24;
A416: (M1 /. (len M1)) `2 = (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 by A299, SPRECT_3:1
.= N-bound (L~ f) by A383, A411, A410, GOBOARD7:6 ;
not mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A401, SPRECT_2:7;
then 1 in dom (mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-min (L~ f)) .. f)) `2 by A60, A401, SPRECT_2:8
.= (S-min (L~ f)) `2 by A400, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A417: M1 is_a_v.c._for f by A415, A416, SPRECT_2:def 3;
A418: len M1 >= 2 by TOPREAL1:def 8;

now

NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A311, A312, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A419: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A288, XBOOLE_1:26;
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ Red2 ; :: thesis: contradiction
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) <> {} by XBOOLE_0:def 7;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A419, ZFMISC_1:33;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) by TARSKI:def 1;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by XBOOLE_0:def 4;
then A420: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A383, XBOOLE_0:def 4;
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) = {(N-min (L~ f))} by A311, A312, TOPREAL1:8;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) = N-min (L~ f) by A420, TARSKI:def 1;
hence contradiction by A240, SPRECT_1:11; :: thesis: verum

end;

then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ RB2 by A257, A301, XBOOLE_1:70;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) by A133, A403, XBOOLE_1:70;
then A421: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ M1 by A404, A408, XBOOLE_1:70;
len M2 >= 2 by TOPREAL1:def 8;
then A422: L~ M1 meets L~ M2 by A418, A417, A413, SPRECT_2:29;
M3 /. 1 = f /. 1 by A15, A398, SPRECT_2:8;
then L~ M3 meets L~ M1 by A1, A422, A421, A414, XBOOLE_1:70;
then L~ M3 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A404, A394, XBOOLE_1:70;
then L~ M3 meets L~ RB2 by A403, A395, XBOOLE_1:70;
then L~ M3 meets L~ Red2 by A301, A396, XBOOLE_1:70;
then L~ M3 meets L~ Red by A252, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A15, A246, A398, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose that A423: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A424: N-min (L~ f) = W-max (L~ f) ; :: thesis: contradiction

A425: (RB2 /. 1) `1 = W-bound (L~ f) by A97, A300, A424, EUCLID:52;
A426: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
(NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
then (RB2 /. (len RB2)) `1 = E-bound (L~ f) by A299, A423, A426, GOBOARD7:5;
then A427: RB2 is_a_h.c._for f by A303, A425, SPRECT_2:def 2;
set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
A428: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
(N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A429: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
W-min (L~ f) in rng f by SPRECT_2:43;
then (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A430: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
A431: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
A432: S-max (L~ f) in rng f by SPRECT_2:42;
then A433: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A431, A429, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A428;
A434: len RB2 >= 2 by TOPREAL1:def 8;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then (S-max (L~ f)) .. f < len f by A430, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A258, A431, A429;
then A435: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A428, SPPOL_2:22;
A436: N-max (L~ f) in rng f by SPRECT_2:40;
then A437: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A438: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A433, SPRECT_2:9
.= (N-max (L~ f)) `2 by A436, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
A439: M1 is_in_the_area_of f by A433, A437, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A433, A437, SPRECT_2:8
.= (S-max (L~ f)) `2 by A432, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A440: M1 is_a_v.c._for f by A439, A438, SPRECT_2:def 3;
len M1 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ RB2 by A434, A440, A427, SPRECT_2:29;
then L~ M1 meets L~ Red2 by A301, A435, XBOOLE_1:70;
then L~ M1 meets L~ Red by A252, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A246, A433, A437, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose that A441: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A442: N-min (L~ f) <> W-max (L~ f) ; :: thesis: contradiction

set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
(W-max (L~ f)) .. f <= (len f) -' 1 by A1, NAT_D:49, SPRECT_2:77;
then A443: (W-min (L~ f)) .. f < (len f) -' 1 by A1, A442, SPRECT_2:75, XXREAL_0:2;
A444: W-min (L~ f) in rng f by SPRECT_2:43;
then A445: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A446: 1 <= (W-min (L~ f)) .. f by FINSEQ_3:25;
then reconsider M3 = mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A443, JORDAN4:39;
L~ M3 misses L~ Red by A60, A246, A445, SPRECT_3:18, XBOOLE_1:63;
then A447: L~ M3 misses L~ Red2 by A252, JORDAN3:41, XBOOLE_1:63;
L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A258, A443, A446;
then A448: L~ RB2 misses L~ M3 by A301, A447, XBOOLE_1:70;
A449: M3 /. (len M3) = f /. ((len f) -' 1) by A60, A445, SPRECT_2:9;
then (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M3) = {(M3 /. (len M3))} by A127, A443, A446;
then reconsider M2 = M3 ^ RB2 as S-Sequence_in_R2 by A79, A84, A97, A300, A302, A449, A448, SPRECT_3:21;
mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A445, SPRECT_2:23;
then A450: M2 is_in_the_area_of f by A303, SPRECT_2:24;
A451: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
A452: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
(N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A453: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
A454: S-max (L~ f) in rng f by SPRECT_2:42;
then A455: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A452, A453, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A451;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A456: (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then A457: L~ M1 misses L~ M3 by A62, A452, A453, A443, SPRECT_2:50;
(W-min (L~ f)) .. f < len f by A61, A443, NAT_1:13;
then (S-max (L~ f)) .. f < len f by A456, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A258, A452, A453;
then A458: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A451, SPPOL_2:22;
A459: len M1 >= 2 by TOPREAL1:def 8;
A460: N-max (L~ f) in rng f by SPRECT_2:40;
then A461: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A462: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A455, SPRECT_2:9
.= (N-max (L~ f)) `2 by A460, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
(S-max (L~ f)) .. f < (len f) -' 1 by A456, A443, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A106, A452, A453;
then A463: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A451, SPPOL_2:22;
A464: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A465: (NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A466: (M2 /. (len M2)) `1 = (RB2 /. (len RB2)) `1 by SPRECT_3:1
.= E-bound (L~ f) by A299, A441, A465, A464, GOBOARD7:5 ;
not mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A445, SPRECT_2:7;
then 1 in dom (mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M2 /. 1) `1 = ((mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) /. 1) `1 by FINSEQ_4:68
.= (f /. ((W-min (L~ f)) .. f)) `1 by A60, A445, SPRECT_2:8
.= (W-min (L~ f)) `1 by A444, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
then A467: M2 is_a_h.c._for f by A450, A466, SPRECT_2:def 2;
A468: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A300, SPPOL_2:23
.= (L~ M3) \/ ((LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
A469: M1 is_in_the_area_of f by A455, A461, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A455, A461, SPRECT_2:8
.= (S-max (L~ f)) `2 by A454, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A470: M1 is_a_v.c._for f by A469, A462, SPRECT_2:def 3;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A459, A470, A467, SPRECT_2:29;
then L~ M1 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3)))) by A468, A457, XBOOLE_1:70;
then L~ M1 meets L~ RB2 by A449, A463, XBOOLE_1:70;
then L~ M1 meets L~ Red2 by A301, A458, XBOOLE_1:70;
then L~ M1 meets L~ Red by A252, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A246, A455, A461, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose A471: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) ; :: thesis: contradiction

A472: (SW-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
(SE-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
then (RB1 /. 1) `2 = S-bound (L~ f) by A304, A471, A472, GOBOARD7:6;
then A473: RB1 is_a_v.c._for f by A171, A305, A308, SPRECT_2:def 3;
A474: len RB1 >= 2 by TOPREAL1:def 8;
set i1 = (E-min (L~ f)) .. f;
set i2 = (W-min (L~ f)) .. f;
A475: mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) = Rev (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) by JORDAN4:18;
(E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A476: (E-min (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then A477: 1 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A478: W-min (L~ f) in rng f by SPRECT_2:43;
then A479: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A480: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f)) is S-Sequence_in_R2 by A477, A476, JORDAN4:40;
then reconsider M2 = mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A475;
L~ (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A271, A477, A476, A480;
then A481: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A475, SPPOL_2:22;
A482: E-min (L~ f) in rng f by SPRECT_2:45;
then A483: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A484: M2 is_in_the_area_of f by A479, SPRECT_2:23;
A485: (M2 /. 1) `1 = (f /. ((W-min (L~ f)) .. f)) `1 by A483, A479, SPRECT_2:8
.= (W-min (L~ f)) `1 by A478, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
(M2 /. (len M2)) `1 = (f /. ((E-min (L~ f)) .. f)) `1 by A483, A479, SPRECT_2:9
.= (E-min (L~ f)) `1 by A482, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A486: M2 is_a_h.c._for f by A484, A485, SPRECT_2:def 2;
len M2 >= 2 by TOPREAL1:def 8;
then L~ RB1 meets L~ M2 by A474, A473, A486, SPRECT_2:29;
then L~ M2 meets L~ Red1 by A306, A481, XBOOLE_1:70;
then L~ M2 meets L~ Red by A265, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A246, A483, A479, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

suppose A487: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ; :: thesis: contradiction

A488: (SW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
set i1 = (S-min (L~ f)) .. f;
set i3 = (E-min (L~ f)) .. f;
A489: (NW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then (E-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then A490: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A491: E-min (L~ f) in rng f by SPRECT_2:45;
then A492: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A493: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M3 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A490, JORDAN4:40;
L~ M3 misses L~ Red by A57, A246, A492, SPRECT_3:18, XBOOLE_1:63;
then A494: L~ M3 misses L~ Red1 by A265, JORDAN3:41, XBOOLE_1:63;
L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A271, A490, A493;
then A495: L~ RB1 misses L~ M3 by A306, A494, XBOOLE_1:70;
A496: M3 /. 1 = f /. 2 by A57, A492, SPRECT_2:8;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) /\ (L~ M3) = {(M3 /. 1)} by A192, A490, A493;
then reconsider M2 = RB1 ^ M3 as S-Sequence_in_R2 by A81, A171, A305, A307, A496, A495, SPRECT_3:21;
A497: (M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A492, SPRECT_2:9
.= (E-min (L~ f)) `1 by A491, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A492, SPRECT_2:23;
then A498: M2 is_in_the_area_of f by A308, SPRECT_2:24;
1 in dom RB1 by FINSEQ_5:6;
then (M2 /. 1) `1 = (RB1 /. 1) `1 by FINSEQ_4:68
.= W-bound (L~ f) by A304, A487, A489, A488, GOBOARD7:5 ;
then A499: M2 is_a_h.c._for f by A498, A497, SPRECT_2:def 2;
A500: L~ M2 = ((L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1)))) \/ (L~ M3) by A305, SPPOL_2:23;
(W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A501: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
(E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then A502: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A503: 2 < (S-min (L~ f)) .. f by A490, XXREAL_0:2;
then A504: 1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A501, JORDAN4:40;
A505: L~ M1 misses L~ M3 by A502, A501, A490, SPRECT_2:47;
A506: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A174, A501, A503;
A507: S-min (L~ f) in rng f by SPRECT_2:41;
then A508: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A509: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A510: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A508, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def 1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A508, SPRECT_2:8
.= (S-min (L~ f)) `2 by A507, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A511: M1 is_a_v.c._for f by A509, A510, SPRECT_2:def 3;
A512: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A271, A501, A504;
A513: len M1 >= 2 by TOPREAL1:def 8;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A513, A511, A499, SPRECT_2:29;
then L~ M1 meets (L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) by A500, A505, XBOOLE_1:70;
then L~ M1 meets L~ RB1 by A496, A506, XBOOLE_1:70;
then L~ M1 meets L~ Red1 by A306, A512, XBOOLE_1:70;
then L~ M1 meets L~ Red by A265, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A58, A246, A508, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum

end;

end;