let f be V22() 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 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_0:30;

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_0:30;

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 object 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;

A71: 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 A72: (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 A73: (len f) -' 2 >= 1 by NAT_D:45;

A74: ((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 A75: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) = {(f /. ((len f) -' 1))} by A73, A74, TOPREAL1:def 6;

A76: 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 A77: LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A1, A69, A76, TOPREAL1:6;

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

A79: ((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 A80: (f /. 2) `2 = N-bound (L~ f) by A17, EUCLID:52;

A81: <*((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 A81, 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 A82: <*((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;

A83: (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 A78, SPPOL_1:16;

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

A85: (NW-corner (L~ f)) `2 = (N-min (L~ f)) `2 by PSCOMP_1:37;

A86: (NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:38;

(N-min (L~ f)) `1 <= (f /. 2) `1 by A76, PSCOMP_1:39;

then N-min (L~ f) in LSeg ((NW-corner (L~ f)),(f /. 2)) by A17, A79, A85, A86, GOBOARD7:8;

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

A89: f /. ((len f) -' 1) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by RLTOPSP1:68;

A90: (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 RLVECT_1:def 5;

then A91: (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 A83, A90;

then A92: 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 A89, TOPREAL1:6;

LSeg ((f /. ((len f) -' 1)),(f /. (len f))) = LSeg (f,((len f) -' 1)) by A59, A61, TOPREAL1:def 3;

then A93: LSeg ((f /. ((len f) -' 1)),(f /. (len f))) c= L~ f by TOPREAL3:19;

then A94: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= L~ f by A92, XBOOLE_1:1;

A95: 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, A92, TOPREAL1:def 3;

A96: ((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 A78, TOPREAL3:2

.= (N-min (L~ f)) `1 ;

then A97: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) is vertical by A78, A83, SPPOL_1:16;

A98: (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 A99: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in L~ f by A94;

then A101: 1 + 1 <= (len f) -' 1 by NAT_D:49;

then A102: 1 <= ((len f) -' 1) -' 1 by NAT_D:49;

A103: (((len f) -' 1) -' 1) + 1 = (len f) -' 1 by A101, XREAL_1:235, XXREAL_0:2;

A104: (((len f) -' 1) -' 1) + 2 = ((len f) -' 2) + 2 by NAT_D:45

.= len f by A7, XREAL_1:235, XXREAL_0:2 ;

A105: for i, j being 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)))

(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))}

set G = GoB f;

A136: 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 A136, XBOOLE_0:def 7

.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} ;

then A137: (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 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= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A137, XBOOLE_1:1;

A139: for i, j being 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)))))))

then A161: <*((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 A162: (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, A82, A161, 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 A163: 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;

A164: 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 RLVECT_1:def 5;

then A165: (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 A166: 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 A164, TOPREAL1:6;

A167: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by A8, TOPREAL1:def 3;

then A168: LSeg ((f /. 1),(f /. 2)) c= L~ f by TOPREAL3:19;

then A169: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= L~ f by A166, XBOOLE_1:1;

A170: ((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 A79, TOPREAL3:2

.= N-bound (L~ f) by EUCLID:52 ;

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

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

A173: for i, j being 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))

(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)}

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)))))))

then A227: (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, A82, A165, SPRECT_3:48;

A228: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) is horizontal by A80, A170, SPPOL_1:15;

A229: (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 A230: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ f by A169;

A231: <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by A169, A229, SPRECT_2:21, SPRECT_3:46;

A232: 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 A233: (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 A234: 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;

A235: 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 A236: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A235, JORDAN5C:def 2;

then A237: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def 4;

A238: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red9 by A236, XBOOLE_0:def 4;

then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> Red9 . (len Red9) by A55, A65, A237, 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 A238, JORDAN3:34;

1 in dom Red by FINSEQ_5:6;

then A240: Red /. 1 = Red . 1 by PARTFUN1:def 6

.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A238, JORDAN3:23 ;

A241: (L~ (SpStSeq (L~ f))) /\ (L~ Red) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A55, A56, A65, Th5;

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 A242: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red by A65, A233, A237, A238, JORDAN5B:22;

Red is_in_the_area_of SpStSeq (L~ f) by A47, A48, A54, A55, SPRECT_3:54;

then A243: Red is_in_the_area_of f by SPRECT_3:53;

A244: L~ Red c= L~ Red9 by A238, JORDAN3:42;

A245: L~ f misses L~ Red by A232, A238, 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 A246: 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 A242, 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 A247: 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 A242, XBOOLE_0:3;

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

A249: (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 A250: 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 A247, A249, JORDAN5C:def 1;

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 L~ Red by XBOOLE_0:def 4;

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 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 A250, 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))))))))) <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A94, A98, A232, A244, A251, XBOOLE_0:3;

A254: (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 A255: 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 A252, TOPREAL1:6;

then A256: 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 A71, A88, A135, SPRECT_3:9, XBOOLE_1:63;

A257: for i, j being 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)))))))

then A263: 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)),(

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 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_0:30;

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_0:30;

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 object 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;

A71: 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 A72: (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 A73: (len f) -' 2 >= 1 by NAT_D:45;

A74: ((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 A75: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) = {(f /. ((len f) -' 1))} by A73, A74, TOPREAL1:def 6;

A76: 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 A77: LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A1, A69, A76, TOPREAL1:6;

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

A79: ((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 A80: (f /. 2) `2 = N-bound (L~ f) by A17, EUCLID:52;

A81: <*((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 A81, 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 A82: <*((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;

A83: (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 A78, SPPOL_1:16;

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

A85: (NW-corner (L~ f)) `2 = (N-min (L~ f)) `2 by PSCOMP_1:37;

A86: (NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:38;

(N-min (L~ f)) `1 <= (f /. 2) `1 by A76, PSCOMP_1:39;

then N-min (L~ f) in LSeg ((NW-corner (L~ f)),(f /. 2)) by A17, A79, A85, A86, GOBOARD7:8;

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

A89: f /. ((len f) -' 1) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by RLTOPSP1:68;

A90: (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 RLVECT_1:def 5;

then A91: (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 A83, A90;

then A92: 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 A89, TOPREAL1:6;

LSeg ((f /. ((len f) -' 1)),(f /. (len f))) = LSeg (f,((len f) -' 1)) by A59, A61, TOPREAL1:def 3;

then A93: LSeg ((f /. ((len f) -' 1)),(f /. (len f))) c= L~ f by TOPREAL3:19;

then A94: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= L~ f by A92, XBOOLE_1:1;

A95: 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, A92, TOPREAL1:def 3;

A96: ((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 A78, TOPREAL3:2

.= (N-min (L~ f)) `1 ;

then A97: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) is vertical by A78, A83, SPPOL_1:16;

A98: (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 A99: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in L~ f by A94;

A100: now :: thesis: not (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = N-min (L~ f)

(1 + 1) + 1 <= len f
by GOBOARD7:34, XXREAL_0:2;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, A83, SPRECT_3:5;

hence contradiction by A58, A60, A61, GOBOARD7:29; :: thesis: verum

end;then f /. ((len f) -' 1) = f /. (len f) by A1, A6, A67, A83, SPRECT_3:5;

hence contradiction by A58, A60, A61, GOBOARD7:29; :: thesis: verum

then A101: 1 + 1 <= (len f) -' 1 by NAT_D:49;

then A102: 1 <= ((len f) -' 1) -' 1 by NAT_D:49;

A103: (((len f) -' 1) -' 1) + 1 = (len f) -' 1 by A101, XREAL_1:235, XXREAL_0:2;

A104: (((len f) -' 1) -' 1) + 2 = ((len f) -' 2) + 2 by NAT_D:45

.= len f by A7, XREAL_1:235, XXREAL_0:2 ;

A105: for i, j being 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

A126:
for j being Nat st 1 <= j & j < (len f) -' 1 holds
let l, j be 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

A106: 1 <= l and

A107: l <= j and

A108: 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

A109: 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 A109, XBOOLE_0:def 4;

then consider ii being Nat such that

A110: 1 <= ii and

A111: ii + 1 <= len (mid (f,l,j)) and

A112: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

(len f) -' 1 > l by A107, A108, XXREAL_0:2;

then (len f) -' 1 > 1 by A106, XXREAL_0:2;

then A113: (len f) -' 1 < len f by NAT_D:51;

then A114: j < len f by A108, XXREAL_0:2;

then len (mid (f,l,j)) = (j -' l) + 1 by A106, A107, JORDAN4:8;

then A115: ii < (j -' l) + 1 by A111, NAT_1:13;

set k = (ii + l) -' 1;

A116: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A109, XBOOLE_0:def 4;

end;assume that

A106: 1 <= l and

A107: l <= j and

A108: 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

A109: 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 A109, XBOOLE_0:def 4;

then consider ii being Nat such that

A110: 1 <= ii and

A111: ii + 1 <= len (mid (f,l,j)) and

A112: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

(len f) -' 1 > l by A107, A108, XXREAL_0:2;

then (len f) -' 1 > 1 by A106, XXREAL_0:2;

then A113: (len f) -' 1 < len f by NAT_D:51;

then A114: j < len f by A108, XXREAL_0:2;

then len (mid (f,l,j)) = (j -' l) + 1 by A106, A107, JORDAN4:8;

then A115: ii < (j -' l) + 1 by A111, NAT_1:13;

set k = (ii + l) -' 1;

A116: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A109, XBOOLE_0:def 4;

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

end;

suppose AB:
l = j
; :: thesis: contradiction

then
j in dom f
by A106, A114, FINSEQ_3:25;

then len (mid (f,l,j)) = 1 by AB, JORDAN4:15;

then L~ (mid (f,l,j)) = {} by TOPREAL1:22;

hence contradiction by A112, SPPOL_2:17; :: thesis: verum

end;then len (mid (f,l,j)) = 1 by AB, JORDAN4:15;

then L~ (mid (f,l,j)) = {} by TOPREAL1:22;

hence contradiction by A112, SPPOL_2:17; :: thesis: verum

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

A118:
ii + 1 >= 1 + 1
by A110, XREAL_1:6;

ii + l >= ii + 1 by A106, XREAL_1:6;

then A119: ii + l >= 1 + 1 by A118, XXREAL_0:2;

then A120: (ii + l) -' 1 >= 1 by NAT_D:49;

A121: ii + l >= 1 by A119, XXREAL_0:2;

.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A106, A114, A110, A115, A117, JORDAN4:19;

then A125: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A95, A116, A112, 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 A113, A122, GOBOARD5:def 4;

then (ii + l) -' 1 = 1 by A120, XXREAL_0:1;

then p = f /. 1 by A125, A124, TARSKI:def 1;

hence contradiction by A1, A67, A91, A100, A116, SPRECT_3:6; :: thesis: verum

end;ii + l >= ii + 1 by A106, XREAL_1:6;

then A119: ii + l >= 1 + 1 by A118, XXREAL_0:2;

then A120: (ii + l) -' 1 >= 1 by NAT_D:49;

A121: ii + l >= 1 by A119, XXREAL_0:2;

A122: now :: thesis: not ((ii + l) -' 1) + 1 >= (len f) -' 1

A124: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) =
{(f . 1)}
by JORDAN4:42
assume
((ii + l) -' 1) + 1 >= (len f) -' 1
; :: thesis: contradiction

then (ii + l) -' 1 >= ((len f) -' 1) -' 1 by NAT_D:53;

then A123: ii + l >= (len f) -' 1 by A121, NAT_D:56;

ii + l < ((j -' l) + 1) + l by A115, XREAL_1:6;

then ii + l < ((j -' l) + l) + 1 ;

then ii + l < j + 1 by A117, XREAL_1:235;

then (len f) -' 1 < j + 1 by A123, XXREAL_0:2;

hence contradiction by A108, NAT_1:13; :: thesis: verum

end;then (ii + l) -' 1 >= ((len f) -' 1) -' 1 by NAT_D:53;

then A123: ii + l >= (len f) -' 1 by A121, NAT_D:56;

ii + l < ((j -' l) + 1) + l by A115, XREAL_1:6;

then ii + l < ((j -' l) + l) + 1 ;

then ii + l < j + 1 by A117, XREAL_1:235;

then (len f) -' 1 < j + 1 by A123, XXREAL_0:2;

hence contradiction by A108, NAT_1:13; :: thesis: verum

.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A106, A114, A110, A115, A117, JORDAN4:19;

then A125: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A95, A116, A112, 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 A113, A122, GOBOARD5:def 4;

then (ii + l) -' 1 = 1 by A120, XXREAL_0:1;

then p = f /. 1 by A125, A124, TARSKI:def 1;

hence contradiction by A1, A67, A91, A100, A116, SPRECT_3:6; :: thesis: verum

(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

A132:
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)))))))
let j be 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

A127: 1 <= j and

A128: 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))}

A129: 1 <= (len f) -' 1 by A127, A128, XXREAL_0:2;

A130: ((len f) -' 1) -' 1 = (len f) -' 2 by NAT_D:45;

then A131: L~ (mid (f,j,((len f) -' 1))) = (LSeg (f,((len f) -' 2))) \/ (L~ (mid (f,j,((len f) -' 2)))) by A127, A128, NAT_D:35, SPRECT_3:20;

j <= (len f) -' 2 by A128, A130, 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 A105, A127, A129, A130, 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 A131, XBOOLE_1:78

.= {(f /. ((len f) -' 1))} by A75, A95, RLTOPSP1:68, ZFMISC_1:124 ;

:: thesis: verum

end;assume that

A127: 1 <= j and

A128: 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))}

A129: 1 <= (len f) -' 1 by A127, A128, XXREAL_0:2;

A130: ((len f) -' 1) -' 1 = (len f) -' 2 by NAT_D:45;

then A131: L~ (mid (f,j,((len f) -' 1))) = (LSeg (f,((len f) -' 2))) \/ (L~ (mid (f,j,((len f) -' 2)))) by A127, A128, NAT_D:35, SPRECT_3:20;

j <= (len f) -' 2 by A128, A130, 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 A105, A127, A129, A130, 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 A131, XBOOLE_1:78

.= {(f /. ((len f) -' 1))} by A75, A95, RLTOPSP1:68, ZFMISC_1:124 ;

:: thesis: verum

proof

A135:
((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 <> (N-min (L~ f)) `2
by A96, A100, TOPREAL3:6;
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

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

A134: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A133, XBOOLE_0:def 4;

p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A133, XBOOLE_0:def 4;

then p in {(N-min (L~ f))} by A1, A67, A84, A92, A134, XBOOLE_0:def 4;

then p = N-min (L~ f) by TARSKI:def 1;

hence contradiction by A1, A67, A91, A100, A134, SPRECT_3:6; :: thesis: verum

end;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

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

A134: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A133, XBOOLE_0:def 4;

p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A133, XBOOLE_0:def 4;

then p in {(N-min (L~ f))} by A1, A67, A84, A92, A134, XBOOLE_0:def 4;

then p = N-min (L~ f) by TARSKI:def 1;

hence contradiction by A1, A67, A91, A100, A134, SPRECT_3:6; :: thesis: verum

set G = GoB f;

A136: 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 A136, XBOOLE_0:def 7

.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} ;

then A137: (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 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= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A137, XBOOLE_1:1;

A139: for i, j being 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

A160:
<*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> is_in_the_area_of f
by A94, A98, SPRECT_2:21, SPRECT_3:46;
len f >= 1 + 1
by GOBOARD7:34, XXREAL_0:2;

then A140: (len f) -' 1 >= 1 by NAT_D:49;

let l, j be 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

A141: 1 <= l and

A142: l < j and

A143: 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

A144: 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 A144, XBOOLE_0:def 4;

then consider ii being Nat such that

A145: 1 <= ii and

A146: ii + 1 <= len (mid (f,l,j)) and

A147: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A148: len (mid (f,l,j)) = (j -' l) + 1 by A141, A142, A143, JORDAN4:8;

then ii < (j -' l) + 1 by A146, NAT_1:13;

then A149: p in LSeg (f,((ii + l) -' 1)) by A141, A142, A143, A145, A147, JORDAN4:19;

set k = (ii + l) -' 1;

A150: ii + 1 >= 1 + 1 by A145, 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 A151: (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 A138, 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 A144, 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 A149, XBOOLE_0:def 4;

then p = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A151, 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 A91, A149, XBOOLE_0:def 4;

then A152: (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, A140, TOPREAL1:def 3;

then A153: LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;

ii + l >= ii + 1 by A141, XREAL_1:6;

then ii + l >= 1 + 1 by A150, XXREAL_0:2;

then A154: (ii + l) -' 1 >= 1 by NAT_D:49;

end;then A140: (len f) -' 1 >= 1 by NAT_D:49;

let l, j be 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

A141: 1 <= l and

A142: l < j and

A143: 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

A144: 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 A144, XBOOLE_0:def 4;

then consider ii being Nat such that

A145: 1 <= ii and

A146: ii + 1 <= len (mid (f,l,j)) and

A147: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A148: len (mid (f,l,j)) = (j -' l) + 1 by A141, A142, A143, JORDAN4:8;

then ii < (j -' l) + 1 by A146, NAT_1:13;

then A149: p in LSeg (f,((ii + l) -' 1)) by A141, A142, A143, A145, A147, JORDAN4:19;

set k = (ii + l) -' 1;

A150: ii + 1 >= 1 + 1 by A145, 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 A151: (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 A138, 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 A144, 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 A149, XBOOLE_0:def 4;

then p = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A151, 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 A91, A149, XBOOLE_0:def 4;

then A152: (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, A140, TOPREAL1:def 3;

then A153: LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;

ii + l >= ii + 1 by A141, XREAL_1:6;

then ii + l >= 1 + 1 by A150, XXREAL_0:2;

then A154: (ii + l) -' 1 >= 1 by NAT_D:49;

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

end;

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

A156: (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 A154, A155, XXREAL_0:1;

hence contradiction by A1, A100, A152, A156, TARSKI:def 1; :: thesis: verum

end;.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

(ii + l) -' 1 = 1 by A154, A155, XXREAL_0:1;

hence contradiction by A1, A100, A152, A156, TARSKI:def 1; :: thesis: verum

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

ii <= j -' l
by A146, A148, XREAL_1:6;

then ii + l <= j by A142, NAT_D:54;

then A158: ii + l < len f by A143, XXREAL_0:2;

ii + l >= l by NAT_1:11;

then ii + l >= 1 by A141, XXREAL_0:2;

then (ii + l) -' 1 < (len f) -' 1 by A158, NAT_D:56;

then A159: (ii + l) -' 1 <= ((len f) -' 1) -' 1 by NAT_D:49;

(ii + l) -' 1 >= ((len f) -' 1) -' 1 by A157, NAT_D:53;

then (ii + l) -' 1 = ((len f) -' 1) -' 1 by A159, 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 A102, A103, A104, A152, 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, A83, A100, SPRECT_3:5; :: thesis: verum

end;then ii + l <= j by A142, NAT_D:54;

then A158: ii + l < len f by A143, XXREAL_0:2;

ii + l >= l by NAT_1:11;

then ii + l >= 1 by A141, XXREAL_0:2;

then (ii + l) -' 1 < (len f) -' 1 by A158, NAT_D:56;

then A159: (ii + l) -' 1 <= ((len f) -' 1) -' 1 by NAT_D:49;

(ii + l) -' 1 >= ((len f) -' 1) -' 1 by A157, NAT_D:53;

then (ii + l) -' 1 = ((len f) -' 1) -' 1 by A159, 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 A102, A103, A104, A152, 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, A83, A100, SPRECT_3:5; :: thesis: verum

then A161: <*((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 A162: (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, A82, A161, 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 A163: 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;

A164: 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 RLVECT_1:def 5;

then A165: (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 A166: 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 A164, TOPREAL1:6;

A167: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by A8, TOPREAL1:def 3;

then A168: LSeg ((f /. 1),(f /. 2)) c= L~ f by TOPREAL3:19;

then A169: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= L~ f by A166, XBOOLE_1:1;

A170: ((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 A79, TOPREAL3:2

.= N-bound (L~ f) by EUCLID:52 ;

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

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

A173: for i, j being 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

A191:
for j being Nat st 2 < j & j <= len f holds
let l, j be 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

A174: 2 < l and

A175: l <= j and

A176: 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

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

A178: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A177, XBOOLE_0:def 4;

p in L~ (mid (f,l,j)) by A177, XBOOLE_0:def 4;

then consider ii being Nat such that

A179: 1 <= ii and

A180: ii + 1 <= len (mid (f,l,j)) and

A181: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A182: 1 < l by A174, XXREAL_0:2;

then A183: len (mid (f,l,j)) = (j -' l) + 1 by A175, A176, JORDAN4:8;

then A184: ii < (j -' l) + 1 by A180, NAT_1:13;

set k = (ii + l) -' 1;

A185: ii + 2 >= 1 + 2 by A179, XREAL_1:6;

ii + l > ii + 2 by A174, XREAL_1:6;

then ii + l > 1 + 2 by A185, XXREAL_0:2;

then A186: (ii + l) -' 1 > 1 + 1 by NAT_D:52;

end;assume that

A174: 2 < l and

A175: l <= j and

A176: 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

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

A178: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A177, XBOOLE_0:def 4;

p in L~ (mid (f,l,j)) by A177, XBOOLE_0:def 4;

then consider ii being Nat such that

A179: 1 <= ii and

A180: ii + 1 <= len (mid (f,l,j)) and

A181: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A182: 1 < l by A174, XXREAL_0:2;

then A183: len (mid (f,l,j)) = (j -' l) + 1 by A175, A176, JORDAN4:8;

then A184: ii < (j -' l) + 1 by A180, NAT_1:13;

set k = (ii + l) -' 1;

A185: ii + 2 >= 1 + 2 by A179, XREAL_1:6;

ii + l > ii + 2 by A174, XREAL_1:6;

then ii + l > 1 + 2 by A185, XXREAL_0:2;

then A186: (ii + l) -' 1 > 1 + 1 by NAT_D:52;

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

end;

suppose AB:
l = j
; :: thesis: contradiction

then
j in dom f
by A176, A182, FINSEQ_3:25;

then len (mid (f,l,j)) = 1 by AB, JORDAN4:15;

then L~ (mid (f,l,j)) = {} by TOPREAL1:22;

hence contradiction by A181, SPPOL_2:17; :: thesis: verum

end;then len (mid (f,l,j)) = 1 by AB, JORDAN4:15;

then L~ (mid (f,l,j)) = {} by TOPREAL1:22;

hence contradiction by A181, SPPOL_2:17; :: thesis: verum

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

A188: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) =
{(f . 1)}
by JORDAN4:42

.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

ii <= j -' l by A180, A183, XREAL_1:6;

then ii + l <= j by A175, NAT_D:54;

then ii + l <= len f by A176, XXREAL_0:2;

then A189: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;

LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A176, A182, A179, A184, A187, JORDAN4:19;

then A190: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A166, A167, A178, A181, 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 A186, GOBOARD5:def 4;

then (ii + l) -' 1 >= (len f) -' 1 by NAT_D:53;

then (ii + l) -' 1 = (len f) -' 1 by A189, XXREAL_0:1;

then p = f /. 1 by A190, A188, TARSKI:def 1;

hence contradiction by A1, A165, A172, A178, SPRECT_3:6; :: thesis: verum

end;.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

ii <= j -' l by A180, A183, XREAL_1:6;

then ii + l <= j by A175, NAT_D:54;

then ii + l <= len f by A176, XXREAL_0:2;

then A189: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;

LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A176, A182, A179, A184, A187, JORDAN4:19;

then A190: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A166, A167, A178, A181, 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 A186, GOBOARD5:def 4;

then (ii + l) -' 1 >= (len f) -' 1 by NAT_D:53;

then (ii + l) -' 1 = (len f) -' 1 by A189, XXREAL_0:1;

then p = f /. 1 by A190, A188, TARSKI:def 1;

hence contradiction by A1, A165, A172, A178, SPRECT_3:6; :: thesis: verum

(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

A196:
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)))
A192:
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 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

A193: 2 < j and

A194: 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 A193, NAT_1:13;

then A195: 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 A173, A194;

L~ (mid (f,2,j)) = (LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),j))) by A193, A194, 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 A195, XBOOLE_1:78

.= {(f /. 2)} by A72, A164, A165, A167, A192, TOPREAL1:6, ZFMISC_1:124 ;

:: thesis: verum

end;let j be 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

A193: 2 < j and

A194: 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 A193, NAT_1:13;

then A195: 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 A173, A194;

L~ (mid (f,2,j)) = (LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),j))) by A193, A194, 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 A195, XBOOLE_1:78

.= {(f /. 2)} by A72, A164, A165, A167, A192, TOPREAL1:6, ZFMISC_1:124 ;

:: thesis: verum

proof

A199:
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)))))))
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

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

A198: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A197, XBOOLE_0:def 4;

p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A197, XBOOLE_0:def 4;

then p in {(N-min (L~ f))} by A1, A87, A166, A198, XBOOLE_0:def 4;

then p = N-min (L~ f) by TARSKI:def 1;

hence contradiction by A1, A165, A172, A198, SPRECT_3:6; :: thesis: verum

end;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

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

A198: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A197, XBOOLE_0:def 4;

p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A197, XBOOLE_0:def 4;

then p in {(N-min (L~ f))} by A1, A87, A166, A198, XBOOLE_0:def 4;

then p = N-min (L~ f) by TARSKI:def 1;

hence contradiction by A1, A165, A172, A198, SPRECT_3:6; :: thesis: verum

proof

A203:
for i, j being Nat st 1 < i & i < j & j <= len f holds
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

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

A201: 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 A200, XBOOLE_0:def 4;

A202: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A200, 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 A77, A163, A165, SPRECT_3:11;

then p in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A70, A202, A201, 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 A202, 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 A169, A171, 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 A172, TARSKI:def 1; :: thesis: verum

end;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

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

A201: 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 A200, XBOOLE_0:def 4;

A202: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A200, 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 A77, A163, A165, SPRECT_3:11;

then p in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A70, A202, A201, 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 A202, 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 A169, A171, 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 A172, TARSKI:def 1; :: thesis: verum

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

LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))
by A1, SPRECT_3:31;
A204:
len f >= 2
by GOBOARD7:34, XXREAL_0:2;

A205: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;

A206: (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 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

A207: 1 < l and

A208: l < j and

A209: 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

A210: 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 A210, XBOOLE_0:def 4;

then consider ii being Nat such that

A211: 1 <= ii and

A212: ii + 1 <= len (mid (f,l,j)) and

A213: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A214: len (mid (f,l,j)) = (j -' l) + 1 by A207, A208, A209, JORDAN4:8;

then ii < (j -' l) + 1 by A212, NAT_1:13;

then A215: p in LSeg (f,((ii + l) -' 1)) by A207, A208, A209, A211, A213, JORDAN4:19;

set k = (ii + l) -' 1;

set G = GoB f;

A216: (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 A205, 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 A206, XBOOLE_1:1;

then 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= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A216, 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 A210, 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 A215, XBOOLE_0:def 4;

then p = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A217, 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 A165, A215, XBOOLE_0:def 4;

then A218: (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 A204, TOPREAL1:def 3;

then LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;

then A219: ( (ii + l) -' 1 <= 1 + 1 or ((ii + l) -' 1) + 1 >= len f ) by GOBOARD5:def 4;

A220: ii + 1 >= 1 + 1 by A211, XREAL_1:6;

ii + l > ii + 1 by A207, XREAL_1:6;

then ii + l > 1 + 1 by A220, XXREAL_0:2;

then A221: (ii + l) -' 1 > 1 by NAT_D:52;

end;A205: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;

A206: (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 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

A207: 1 < l and

A208: l < j and

A209: 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

A210: 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 A210, XBOOLE_0:def 4;

then consider ii being Nat such that

A211: 1 <= ii and

A212: ii + 1 <= len (mid (f,l,j)) and

A213: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;

A214: len (mid (f,l,j)) = (j -' l) + 1 by A207, A208, A209, JORDAN4:8;

then ii < (j -' l) + 1 by A212, NAT_1:13;

then A215: p in LSeg (f,((ii + l) -' 1)) by A207, A208, A209, A211, A213, JORDAN4:19;

set k = (ii + l) -' 1;

set G = GoB f;

A216: (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 A205, 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 A206, XBOOLE_1:1;

then 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= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A216, 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 A210, 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 A215, XBOOLE_0:def 4;

then p = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A217, 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 A165, A215, XBOOLE_0:def 4;

then A218: (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 A204, TOPREAL1:def 3;

then LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;

then A219: ( (ii + l) -' 1 <= 1 + 1 or ((ii + l) -' 1) + 1 >= len f ) by GOBOARD5:def 4;

A220: ii + 1 >= 1 + 1 by A211, XREAL_1:6;

ii + l > ii + 1 by A207, XREAL_1:6;

then ii + l > 1 + 1 by A220, XXREAL_0:2;

then A221: (ii + l) -' 1 > 1 by NAT_D:52;

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

end;

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

(ii + l) -' 1 >= 1 + 1
by A221, NAT_1:13;

then A223: (ii + l) -' 1 = 2 by A222, 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 A218, A223, 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, A172, SPRECT_3:5; :: thesis: verum

end;then A223: (ii + l) -' 1 = 2 by A222, 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 A218, A223, 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, A172, SPRECT_3:5; :: thesis: verum

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

A225: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) =
{(f . 1)}
by JORDAN4:42

.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

ii <= j -' l by A212, A214, XREAL_1:6;

then ii + l <= j by A208, NAT_D:54;

then ii + l <= len f by A209, XXREAL_0:2;

then A226: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;

(ii + l) -' 1 >= (len f) -' 1 by A224, NAT_D:53;

then (ii + l) -' 1 = (len f) -' 1 by A226, XXREAL_0:1;

hence contradiction by A1, A172, A218, A225, TARSKI:def 1; :: thesis: verum

end;.= {(f /. 1)} by A15, PARTFUN1:def 6 ;

ii <= j -' l by A212, A214, XREAL_1:6;

then ii + l <= j by A208, NAT_D:54;

then ii + l <= len f by A209, XXREAL_0:2;

then A226: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;

(ii + l) -' 1 >= (len f) -' 1 by A224, NAT_D:53;

then (ii + l) -' 1 = (len f) -' 1 by A226, XXREAL_0:1;

hence contradiction by A1, A172, A218, A225, TARSKI:def 1; :: thesis: verum

then A227: (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, A82, A165, SPRECT_3:48;

A228: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) is horizontal by A80, A170, SPPOL_1:15;

A229: (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 A230: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ f by A169;

A231: <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by A169, A229, SPRECT_2:21, SPRECT_3:46;

A232: 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 A233: (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 A234: 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;

A235: 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 A236: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A235, JORDAN5C:def 2;

then A237: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def 4;

A238: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red9 by A236, XBOOLE_0:def 4;

A239: now :: thesis: not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ f

len Red9 in dom Red9
by FINSEQ_5:6;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 A238, XBOOLE_0:def 4;

hence contradiction by A232, XBOOLE_0:def 7; :: thesis: verum

end;then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ f) /\ (L~ Red9) by A238, XBOOLE_0:def 4;

hence contradiction by A232, XBOOLE_0:def 7; :: thesis: verum

then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> Red9 . (len Red9) by A55, A65, A237, 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 A238, JORDAN3:34;

1 in dom Red by FINSEQ_5:6;

then A240: Red /. 1 = Red . 1 by PARTFUN1:def 6

.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A238, JORDAN3:23 ;

A241: (L~ (SpStSeq (L~ f))) /\ (L~ Red) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A55, A56, A65, Th5;

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 A242: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red by A65, A233, A237, A238, JORDAN5B:22;

Red is_in_the_area_of SpStSeq (L~ f) by A47, A48, A54, A55, SPRECT_3:54;

then A243: Red is_in_the_area_of f by SPRECT_3:53;

A244: L~ Red c= L~ Red9 by A238, JORDAN3:42;

A245: L~ f misses L~ Red by A232, A238, 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 A246: 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 A242, 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 A247: 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 A242, XBOOLE_0:3;

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

A249: (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 A250: 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 A247, A249, JORDAN5C:def 1;

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 L~ Red by XBOOLE_0:def 4;

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 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 A250, 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))))))))) <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A94, A98, A232, A244, A251, XBOOLE_0:3;

A254: (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 A255: 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 A252, TOPREAL1:6;

then A256: 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 A71, A88, A135, SPRECT_3:9, XBOOLE_1:63;

A257: for i, j being 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 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

A258: 1 <= i and

A259: i < j and

A260: 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 A139, A258, A259, A260;

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 A252, A254, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum

end;assume that

A258: 1 <= i and

A259: i < j and

A260: 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 A139, A258, A259, A260;

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 A252, A254, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum

A261: now :: thesis: not 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

L~ Red is_an_arc_of Red /. 1,Red /. (len Red)
by TOPREAL1:25;A262:
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 A237, A240, A262, 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 A252, XBOOLE_0:def 4;

hence contradiction by A162, A253, TARSKI:def 1; :: thesis: verum

end;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 A237, A240, A262, 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 A252, XBOOLE_0:def 4;

hence contradiction by A162, A253, TARSKI:def 1; :: thesis: verum

then A263: 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)),(