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;
A100: now :: thesis: not (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = N-min (L~ f)
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;
(1 + 1) + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
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
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;
per cases ( l = j or l < j ) by A107, XXREAL_0:1;
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;
A122: now :: thesis: not ((ii + l) -' 1) + 1 >= (len f) -' 1
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;
A124: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def 6 ;
LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by 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;
end;
end;
A126: for j being Nat st 1 <= j & j < (len f) -' 1 holds
(L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))}
proof
let j be 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;
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)))))))
proof
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) ; :: thesis: contradiction
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
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;
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;
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
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;
per cases ( (ii + l) -' 1 <= 1 or ((ii + l) -' 1) + 1 >= (len f) -' 1 ) by A62, A153, GOBOARD5:def 4;
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;
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;
end;
end;
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;
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
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;
per cases ( l = j or l < j ) by A175, XXREAL_0:1;
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;
end;
end;
A191: for j being Nat st 2 < j & j <= len f holds
(L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)}
proof
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;
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)))
proof
assume LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) meets LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; :: thesis: contradiction
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
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;
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)))))))
proof
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) <> {} by XBOOLE_0:def 7;
then consider p being Point of (TOP-REAL 2) such that
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;
A203: 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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
proof
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;
per cases ( (ii + l) -' 1 <= 2 or ((ii + l) -' 1) + 1 >= len f ) by A219;
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;
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;
end;
end;
LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A1, SPRECT_3:31;
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
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;
len Red9 in dom Red9 by FINSEQ_5:6;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> Red9 . (len Red9) by A55, A65, 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;
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
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;
L~ Red is_an_arc_of Red /. 1,Red /. (len Red) by TOPREAL1:25;
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)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) by A246, A248, JORDAN5C:def 1;
then A264: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red by XBOOLE_0:def 4;
A265: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in 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 A263, XBOOLE_0:def 4;
A266: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A169, A229, A232, A244, A264, XBOOLE_0:3;
A267: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A268: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) c= LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A265, TOPREAL1:6;
A269: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A199, A265, A267, TOPREAL1:6, XBOOLE_1:63;
A270: 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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
proof
let i, j be Nat; :: thesis: ( 1 < i & i < j & j <= len f implies L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) )
assume that
A271: 1 < i and
A272: i < j and
A273: j <= len f ; :: thesis: L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A203, A271, A272, A273;
hence L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A265, A267, TOPREAL1:6, XBOOLE_1:63; :: thesis: verum
end;
A274: 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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) = Red . 1
A275: 1 in dom Red by FINSEQ_5:6;
assume First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) = Red . 1 ; :: thesis: contradiction
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ (SpStSeq (L~ f)) by A237, A240, A275, PARTFUN1:def 6;
then First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A227, A265, XBOOLE_0:def 4;
hence contradiction by A266, TARSKI:def 1; :: thesis: verum
end;
reconsider Red2 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) as S-Sequence_in_R2 by A251, A261, JORDAN3:35;
A276: Red2 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A240, A251, SPRECT_3:22;
A277: len Red2 in dom Red2 by FINSEQ_5:6;
A278: (Rev Red2) /. 1 = Red2 /. (len Red2) by FINSEQ_5:65
.= Red2 . (len Red2) by A277, PARTFUN1:def 6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A251, JORDAN3:24 ;
then A279: ((Rev Red2) /. 1) `2 = ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 by A88, A252, SPPOL_1:40;
A280: (Rev Red2) /. 1 <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A94, A98, A232, A244, A251, A278, XBOOLE_0:3;
A281: L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
A282: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ Red2 by A251, A261, JORDAN5B:20;
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) by RLTOPSP1:68;
then A283: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (L~ Red2) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A282, XBOOLE_0:def 4;
now :: thesis: not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
assume Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A237, XBOOLE_0:def 4;
hence contradiction by A99, A162, A239, TARSKI:def 1; :: thesis: verum
end;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A240, A247, Th1;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A252, A254, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A283, ZFMISC_1:33;
then reconsider RB2 = <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ (Rev Red2) as S-Sequence_in_R2 by A278, A279, A280, A281, SPRECT_3:16;
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red by A92, A93, A245, XBOOLE_1:1, XBOOLE_1:63;
then LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A284: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ Red2) = {} by XBOOLE_0:def 7;
1 in dom Red2 by FINSEQ_5:6;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red2 by A276, SPPOL_2:44;
then A285: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red2) by A237, XBOOLE_0:def 4;
(L~ (SpStSeq (L~ f))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A241, A251, JORDAN3:41, XBOOLE_1:26;
then A286: (L~ (SpStSeq (L~ f))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A285, ZFMISC_1:33;
reconsider Red1 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) as S-Sequence_in_R2 by A264, A274, JORDAN3:35;
len Red1 in dom Red1 by FINSEQ_5:6;
then A287: Red1 /. (len Red1) = Red1 . (len Red1) by PARTFUN1:def 6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A264, JORDAN3:24 ;
A288: Red1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A240, A264, SPRECT_3:22;
A289: (Red1 /. (len Red1)) `1 = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by A163, A265, A287, SPPOL_1:41;
A290: Red1 /. (len Red1) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A169, A229, A232, A244, A264, A287, XBOOLE_0:3;
A291: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red1 by A264, A274, JORDAN5B:20;
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) by RLTOPSP1:68;
then A292: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (L~ Red1) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) by A291, XBOOLE_0:def 4;
now :: thesis: not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
assume Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; :: thesis: contradiction
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A237, XBOOLE_0:def 4;
hence contradiction by A227, A230, A239, TARSKI:def 1; :: thesis: verum
end;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A240, A246, Th1;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A265, A267, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A292, ZFMISC_1:33;
then reconsider RB1 = Red1 ^ <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> as S-Sequence_in_R2 by A287, A289, A290, SPRECT_2:61;
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red by A166, A168, A245, XBOOLE_1:1, XBOOLE_1:63;
then LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
then A293: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ Red1) = {} by XBOOLE_0:def 7;
1 in dom Red1 by FINSEQ_5:6;
then A294: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red1 by A288, SPPOL_2:44;
then A295: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red1) by A237, XBOOLE_0:def 4;
(L~ (SpStSeq (L~ f))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A241, A264, JORDAN3:41, XBOOLE_1:26;
then A296: (L~ (SpStSeq (L~ f))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A295, ZFMISC_1:33;
len (Rev Red2) = len Red2 by FINSEQ_5:def 3;
then A297: RB2 /. (len RB2) = (Rev Red2) /. (len Red2) by SPRECT_3:1
.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A276, FINSEQ_5:65 ;
A298: RB2 /. 1 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by FINSEQ_5:15;
L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
then A299: L~ RB2 = (L~ Red2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A278, SPPOL_2:20;
then A300: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ RB2) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A284, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A88, A97, A255, SPRECT_1:9, SPRECT_3:10 ;
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))*> is_in_the_area_of f by A243, A251, SPRECT_3:46;
then Red2 is_in_the_area_of f by A243, A251, SPRECT_3:52;
then Rev Red2 is_in_the_area_of f by SPRECT_3:51;
then A301: RB2 is_in_the_area_of f by A160, SPRECT_2:24;
1 in dom Red1 by FINSEQ_5:6;
then A302: RB1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A288, FINSEQ_4:68;
len <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> = 1 by FINSEQ_1:39;
then len RB1 = (len Red1) + 1 by FINSEQ_1:22;
then A303: RB1 /. (len RB1) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by FINSEQ_4:67;
A304: L~ RB1 = (L~ Red1) \/ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A287, SPPOL_2:19;
then A305: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A293, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A163, A228, A268, SPRECT_1:10, SPRECT_3:10 ;
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))*> is_in_the_area_of f by A243, A264, SPRECT_3:46;
then Red1 is_in_the_area_of f by A243, A264, SPRECT_3:52;
then A306: RB1 is_in_the_area_of f by A231, SPRECT_2:24;
A307: L~ Red9 is_an_arc_of z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A50, A53, TOPREAL4:2;
(L~ Red9) /\ (L~ (SpStSeq (L~ f))) is closed by TOPS_1:8;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A307, JORDAN5C:def 2;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def 4;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by SPRECT_1:41;
then A308: ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def 3;
A309: N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
A310: N-min (L~ f) in N-most (L~ f) by PSCOMP_1:42;
then LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) = (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) \/ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A309, TOPREAL1:5;
then A311: ( not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) ) by XBOOLE_0:def 3;
per cases ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) = NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) <> NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) = W-max (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) <> W-max (L~ f) ) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by A308, A311, XBOOLE_0:def 3;
suppose A312: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; :: thesis: contradiction
A313: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A309, A310, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A312, A313, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A314: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A296, XBOOLE_1:26;
A315: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A316: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A269, A312, TOPREAL1:6, XBOOLE_1:63;
then A317: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {} by XBOOLE_0:def 7;
Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by RLTOPSP1:68;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by A294, XBOOLE_0:def 4;
then {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} c= (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by ZFMISC_1:31;
then (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A314, XBOOLE_0:def 10;
then A318: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ RB1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} \/ {} by A304, A317, XBOOLE_1:23
.= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} ;
(NW-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
then (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 = (NW-corner (L~ f)) `2 by A312, A315, GOBOARD7:6;
then reconsider M3 = <*(NW-corner (L~ f))*> ^ RB1 as S-Sequence_in_R2 by A234, A302, A318, SPRECT_3:16;
A319: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
set i1 = (S-min (L~ f)) .. f;
set i2 = (E-min (L~ f)) .. f;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (N-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then 2 <= (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
then A320: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A196, A312, A316, TOPREAL1:6, XBOOLE_1:63;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) = {} by XBOOLE_0:def 7;
then A321: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M3) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1)) by A302, A319, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A305 ;
A322: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
(W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A323: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
A324: E-min (L~ f) in rng f by SPRECT_2:45;
then A325: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A326: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M4 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A320, JORDAN4:40;
L~ M4 misses L~ Red by A57, A245, A325, SPRECT_3:18, XBOOLE_1:63;
then A327: L~ M4 misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A328: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A329: 2 < (S-min (L~ f)) .. f by A320, XXREAL_0:2;
then 1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A323, JORDAN4:40;
A330: L~ M1 misses L~ M4 by A328, A323, A320, SPRECT_2:47;
A331: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A173, A323, A329;
A332: len M1 >= 2 by TOPREAL1:def 8;
A333: M4 /. 1 = f /. 2 by A57, A325, SPRECT_2:8;
L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A320, A326;
then A334: L~ RB1 misses L~ M4 by A304, A327, XBOOLE_1:70;
A335: LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A312, A316, TOPREAL1:6;
A336: now :: thesis: not L~ f meets LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))
A337: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
assume L~ f meets LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) ; :: thesis: contradiction
then consider u being object such that
A338: u in L~ f and
A339: u in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by XBOOLE_0:3;
reconsider u = u as Point of (TOP-REAL 2) by A338;
u in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) by A335, A338, A339, XBOOLE_0:def 4;
then u = N-min (L~ f) by A337, TARSKI:def 1;
hence contradiction by A239, A312, A338, A339, SPRECT_3:6; :: thesis: verum
end;
then L~ M4 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A57, A325, SPRECT_3:18, XBOOLE_1:63;
then A340: L~ M3 misses L~ M4 by A302, A319, A334, XBOOLE_1:70;
A341: S-min (L~ f) in rng f by SPRECT_2:41;
then A342: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A343: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A344: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A342, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def 1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A342, SPRECT_2:8
.= (S-min (L~ f)) `2 by A341, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A345: M1 is_a_v.c._for f by A343, A344, SPRECT_2:def 3;
A346: <*(NW-corner (L~ f))*> ^ RB1 is_in_the_area_of f by A63, A306, SPRECT_2:24;
1 < (S-min (L~ f)) .. f by A329, XXREAL_0:2;
then A347: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A323;
A348: M3 /. (len M3) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A303, SPRECT_3:1;
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M4) = {(f /. 2)} by A191, A320, A326;
then reconsider M2 = M3 ^ M4 as S-Sequence_in_R2 by A80, A170, A348, A333, A340, A321, SPRECT_3:21;
M2 = <*(NW-corner (L~ f))*> ^ (RB1 ^ (mid (f,2,((E-min (L~ f)) .. f)))) by FINSEQ_1:32;
then A349: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;
mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A325, SPRECT_2:23;
then A350: M2 is_in_the_area_of f by A346, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A325, SPRECT_2:9
.= (E-min (L~ f)) `1 by A324, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A351: M2 is_a_h.c._for f by A350, A349, SPRECT_2:def 2;
A352: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1)))) \/ (L~ M4) by SPPOL_2:23;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A332, A345, A351, SPRECT_2:29;
then L~ M1 meets (L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1))) by A352, A330, XBOOLE_1:70;
then A353: L~ M1 meets L~ M3 by A348, A333, A331, XBOOLE_1:70;
L~ M1 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A58, A342, A336, SPRECT_3:18, XBOOLE_1:63;
then L~ M1 meets L~ RB1 by A302, A353, A322, XBOOLE_1:70;
then L~ M1 meets L~ Red1 by A304, A347, XBOOLE_1:70;
then L~ M1 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A58, A245, A342, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose that A354: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A355: N-min (L~ f) = NW-corner (L~ f) ; :: thesis: contradiction
set i1 = (S-max (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A356: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
(S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
then (S-max (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then ((S-max (L~ f)) .. f) + 1 <= (W-min (L~ f)) .. f by NAT_1:13;
then ((S-max (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:76, XXREAL_0:2;
then A357: (S-max (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
(E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then A358: (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A359: 1 < (S-max (L~ f)) .. f by A356, XXREAL_0:2;
then reconsider M4 = mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A357, JORDAN4:39;
A360: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A357, A359;
(S-max (L~ f)) .. f < len f by A357, NAT_D:44;
then A361: (E-max (L~ f)) .. f < len f by A358, XXREAL_0:2;
then ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M2 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A356, JORDAN4:39;
A362: L~ M2 misses L~ M4 by A62, A358, A357, A356, SPRECT_2:47;
(E-max (L~ f)) .. f < (len f) -' 1 by A358, A357, XXREAL_0:2;
then A363: L~ M2 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A356;
A364: len M2 >= 2 by TOPREAL1:def 8;
A365: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A356, A361;
A366: E-max (L~ f) in rng f by SPRECT_2:46;
then A367: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A368: (M2 /. (len M2)) `1 = (f /. ((E-max (L~ f)) .. f)) `1 by A15, SPRECT_2:9
.= (E-max (L~ f)) `1 by A366, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
A369: S-max (L~ f) in rng f by SPRECT_2:42;
then A370: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then L~ M4 misses L~ Red by A60, A245, SPRECT_3:18, XBOOLE_1:63;
then L~ M4 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A371: L~ RB2 misses L~ M4 by A299, A360, XBOOLE_1:70;
A372: M2 is_in_the_area_of f by A15, A367, SPRECT_2:23;
(M2 /. 1) `1 = (f /. 1) `1 by A15, A367, SPRECT_2:8
.= W-bound (L~ f) by A1, A355, EUCLID:52 ;
then A373: M2 is_a_h.c._for f by A372, A368, SPRECT_2:def 2;
A374: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A375: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A376: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A370, SPRECT_2:9;
then (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A126, A357, A359;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A376, A371, SPRECT_3:21;
mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A370, SPRECT_2:23;
then A377: M1 is_in_the_area_of f by A301, SPRECT_2:24;
A378: (M1 /. (len M1)) `2 = (RB2 /. (len RB2)) `2 by SPRECT_3:1
.= N-bound (L~ f) by A297, A354, A375, A374, GOBOARD7:6 ;
not mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is empty by A60, A370, SPRECT_2:7;
then 1 in dom (mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-max (L~ f)) .. f)) `2 by A60, A370, SPRECT_2:8
.= (S-max (L~ f)) `2 by A369, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A379: M1 is_a_v.c._for f by A377, A378, SPRECT_2:def 3;
A380: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
len M1 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A364, A379, A373, SPRECT_2:29;
then L~ M2 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A380, A362, XBOOLE_1:70;
then L~ M2 meets L~ RB2 by A376, A363, XBOOLE_1:70;
then L~ M2 meets L~ Red2 by A299, A365, XBOOLE_1:70;
then L~ M2 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A15, A245, A367, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose that A381: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A382: N-min (L~ f) <> NW-corner (L~ f) ; :: thesis: contradiction
set i1 = (S-min (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
A383: (S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
W-max (L~ f) <> N-min (L~ f) by A382, PSCOMP_1:61;
then (S-min (L~ f)) .. f < (W-max (L~ f)) .. f by A1, A383, SPRECT_2:75, XXREAL_0:2;
then ((S-min (L~ f)) .. f) + 1 <= (W-max (L~ f)) .. f by NAT_1:13;
then ((S-min (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:77, XXREAL_0:2;
then A384: (S-min (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
A385: N-min (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
A386: (N-min (L~ f)) `2 = (NW-corner (L~ f)) `2 by PSCOMP_1:37;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A387: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
(E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A388: (E-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A389: 1 < (S-min (L~ f)) .. f by A387, XXREAL_0:2;
then reconsider M4 = mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A384, JORDAN4:39;
A390: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A384, A389;
(S-min (L~ f)) .. f < len f by A384, NAT_D:44;
then A391: (E-max (L~ f)) .. f < len f by A388, XXREAL_0:2;
then ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M3 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A387, JORDAN4:39;
A392: L~ M3 misses L~ M4 by A62, A388, A384, A387, SPRECT_2:47;
(E-max (L~ f)) .. f < (len f) -' 1 by A388, A384, XXREAL_0:2;
then A393: L~ M3 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A387;
A394: L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A387, A391;
A395: E-max (L~ f) in rng f by SPRECT_2:46;
then A396: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A397: M3 /. 1 = N-min (L~ f) by A1, A15, SPRECT_2:8;
A398: S-min (L~ f) in rng f by SPRECT_2:41;
then A399: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then L~ M4 misses L~ Red by A60, A245, SPRECT_3:18, XBOOLE_1:63;
then L~ M4 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A400: L~ RB2 misses L~ M4 by A299, A390, XBOOLE_1:70;
A401: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A399, SPRECT_2:9;
then (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A126, A384, A389;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A401, A400, SPRECT_3:21;
A402: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
1 in dom M3 by FINSEQ_5:6;
then N-min (L~ f) in L~ M3 by A397, SPPOL_2:44;
then N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by A385, XBOOLE_0:def 4;
then A403: {(N-min (L~ f))} c= (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by ZFMISC_1:31;
A404: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) c= {(N-min (L~ f))} by A15, A396, SPRECT_3:18, XBOOLE_1:26;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) = {(N-min (L~ f))} by A403, XBOOLE_0:def 10;
then reconsider M2 = <*(NW-corner (L~ f))*> ^ M3 as S-Sequence_in_R2 by A382, A386, A397, SPRECT_3:16;
A405: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;
A406: now :: thesis: not LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ M4
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ M4 ; :: thesis: contradiction
then A407: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) <> {} by XBOOLE_0:def 7;
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) c= {(N-min (L~ f))} by A60, A399, A404, SPRECT_3:18, XBOOLE_1:26;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) = {(N-min (L~ f))} by A407, ZFMISC_1:33;
then N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) by TARSKI:def 1;
then N-min (L~ f) in L~ M4 by XBOOLE_0:def 4;
hence contradiction by A1, A62, A384, A389, SPRECT_3:30; :: thesis: verum
end;
A408: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A409: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
mid (f,1,((E-max (L~ f)) .. f)) is_in_the_area_of f by A15, A396, SPRECT_2:23;
then A410: M2 is_in_the_area_of f by A63, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,1,((E-max (L~ f)) .. f))) /. (len (mid (f,1,((E-max (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-max (L~ f)) .. f)) `1 by A15, A396, SPRECT_2:9
.= (E-max (L~ f)) `1 by A395, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A411: M2 is_a_h.c._for f by A410, A405, SPRECT_2:def 2;
A412: L~ M2 = (LSeg ((NW-corner (L~ f)),(M3 /. 1))) \/ (L~ M3) by SPPOL_2:20;
mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A399, SPRECT_2:23;
then A413: M1 is_in_the_area_of f by A301, SPRECT_2:24;
A414: (M1 /. (len M1)) `2 = (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 by A297, SPRECT_3:1
.= N-bound (L~ f) by A381, A409, A408, GOBOARD7:6 ;
not mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A399, SPRECT_2:7;
then 1 in dom (mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-min (L~ f)) .. f)) `2 by A60, A399, SPRECT_2:8
.= (S-min (L~ f)) `2 by A398, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A415: M1 is_a_v.c._for f by A413, A414, SPRECT_2:def 3;
A416: len M1 >= 2 by TOPREAL1:def 8;
now :: thesis: not LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ Red2
NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A309, A310, TOPREAL1:6;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A417: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A286, XBOOLE_1:26;
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ Red2 ; :: thesis: contradiction
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) <> {} by XBOOLE_0:def 7;
then (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A417, ZFMISC_1:33;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) by TARSKI:def 1;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by XBOOLE_0:def 4;
then A418: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A381, XBOOLE_0:def 4;
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) = {(N-min (L~ f))} by A309, A310, TOPREAL1:8;
then Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) = N-min (L~ f) by A418, TARSKI:def 1;
hence contradiction by A239, SPRECT_1:11; :: thesis: verum
end;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ RB2 by A256, A299, XBOOLE_1:70;
then LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) by A132, A401, XBOOLE_1:70;
then A419: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ M1 by A402, A406, XBOOLE_1:70;
len M2 >= 2 by TOPREAL1:def 8;
then A420: L~ M1 meets L~ M2 by A416, A415, A411, SPRECT_2:29;
M3 /. 1 = f /. 1 by A15, A396, SPRECT_2:8;
then L~ M3 meets L~ M1 by A1, A420, A419, A412, XBOOLE_1:70;
then L~ M3 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A402, A392, XBOOLE_1:70;
then L~ M3 meets L~ RB2 by A401, A393, XBOOLE_1:70;
then L~ M3 meets L~ Red2 by A299, A394, XBOOLE_1:70;
then L~ M3 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A15, A245, A396, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose that A421: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A422: N-min (L~ f) = W-max (L~ f) ; :: thesis: contradiction
A423: (RB2 /. 1) `1 = W-bound (L~ f) by A96, A298, A422, EUCLID:52;
A424: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
(NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
then (RB2 /. (len RB2)) `1 = E-bound (L~ f) by A297, A421, A424, GOBOARD7:5;
then A425: RB2 is_a_h.c._for f by A301, A423, SPRECT_2:def 2;
set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
A426: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
(N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A427: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
W-min (L~ f) in rng f by SPRECT_2:43;
then (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A428: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
A429: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
A430: S-max (L~ f) in rng f by SPRECT_2:42;
then A431: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A429, A427, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A426;
A432: len RB2 >= 2 by TOPREAL1:def 8;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then (S-max (L~ f)) .. f < len f by A428, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A429, A427;
then A433: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A426, SPPOL_2:22;
A434: N-max (L~ f) in rng f by SPRECT_2:40;
then A435: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A436: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A431, SPRECT_2:9
.= (N-max (L~ f)) `2 by A434, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
A437: M1 is_in_the_area_of f by A431, A435, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A431, A435, SPRECT_2:8
.= (S-max (L~ f)) `2 by A430, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A438: M1 is_a_v.c._for f by A437, A436, SPRECT_2:def 3;
len M1 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ RB2 by A432, A438, A425, SPRECT_2:29;
then L~ M1 meets L~ Red2 by A299, A433, XBOOLE_1:70;
then L~ M1 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A245, A431, A435, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose that A439: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A440: N-min (L~ f) <> W-max (L~ f) ; :: thesis: contradiction
set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
(W-max (L~ f)) .. f <= (len f) -' 1 by A1, NAT_D:49, SPRECT_2:77;
then A441: (W-min (L~ f)) .. f < (len f) -' 1 by A1, A440, SPRECT_2:75, XXREAL_0:2;
A442: W-min (L~ f) in rng f by SPRECT_2:43;
then A443: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A444: 1 <= (W-min (L~ f)) .. f by FINSEQ_3:25;
then reconsider M3 = mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A441, JORDAN4:39;
L~ M3 misses L~ Red by A60, A245, A443, SPRECT_3:18, XBOOLE_1:63;
then A445: L~ M3 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A441, A444;
then A446: L~ RB2 misses L~ M3 by A299, A445, XBOOLE_1:70;
A447: M3 /. (len M3) = f /. ((len f) -' 1) by A60, A443, SPRECT_2:9;
then (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M3) = {(M3 /. (len M3))} by A126, A441, A444;
then reconsider M2 = M3 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A447, A446, SPRECT_3:21;
mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A443, SPRECT_2:23;
then A448: M2 is_in_the_area_of f by A301, SPRECT_2:24;
A449: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
A450: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
(N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A451: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
A452: S-max (L~ f) in rng f by SPRECT_2:42;
then A453: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A450, A451, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A449;
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A454: (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then A455: L~ M1 misses L~ M3 by A62, A450, A451, A441, SPRECT_2:50;
(W-min (L~ f)) .. f < len f by A61, A441, NAT_1:13;
then (S-max (L~ f)) .. f < len f by A454, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A450, A451;
then A456: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A449, SPPOL_2:22;
A457: len M1 >= 2 by TOPREAL1:def 8;
A458: N-max (L~ f) in rng f by SPRECT_2:40;
then A459: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A460: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A453, SPRECT_2:9
.= (N-max (L~ f)) `2 by A458, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
(S-max (L~ f)) .. f < (len f) -' 1 by A454, A441, XXREAL_0:2;
then L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A450, A451;
then A461: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A449, SPPOL_2:22;
A462: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A463: (NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A464: (M2 /. (len M2)) `1 = (RB2 /. (len RB2)) `1 by SPRECT_3:1
.= E-bound (L~ f) by A297, A439, A463, A462, GOBOARD7:5 ;
not mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A443, SPRECT_2:7;
then 1 in dom (mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M2 /. 1) `1 = ((mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) /. 1) `1 by FINSEQ_4:68
.= (f /. ((W-min (L~ f)) .. f)) `1 by A60, A443, SPRECT_2:8
.= (W-min (L~ f)) `1 by A442, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
then A465: M2 is_a_h.c._for f by A448, A464, SPRECT_2:def 2;
A466: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M3) \/ ((LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
A467: M1 is_in_the_area_of f by A453, A459, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A453, A459, SPRECT_2:8
.= (S-max (L~ f)) `2 by A452, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A468: M1 is_a_v.c._for f by A467, A460, SPRECT_2:def 3;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A457, A468, A465, SPRECT_2:29;
then L~ M1 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3)))) by A466, A455, XBOOLE_1:70;
then L~ M1 meets L~ RB2 by A447, A461, XBOOLE_1:70;
then L~ M1 meets L~ Red2 by A299, A456, XBOOLE_1:70;
then L~ M1 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A245, A453, A459, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose A469: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) ; :: thesis: contradiction
A470: (SW-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
(SE-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
then (RB1 /. 1) `2 = S-bound (L~ f) by A302, A469, A470, GOBOARD7:6;
then A471: RB1 is_a_v.c._for f by A170, A303, A306, SPRECT_2:def 3;
A472: len RB1 >= 2 by TOPREAL1:def 8;
set i1 = (E-min (L~ f)) .. f;
set i2 = (W-min (L~ f)) .. f;
A473: mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) = Rev (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) by JORDAN4:18;
(E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A474: (E-min (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then A475: 1 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A476: W-min (L~ f) in rng f by SPRECT_2:43;
then A477: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A478: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f)) is S-Sequence_in_R2 by A475, A474, JORDAN4:40;
then reconsider M2 = mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A473;
L~ (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A475, A474, A478;
then A479: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A473, SPPOL_2:22;
A480: E-min (L~ f) in rng f by SPRECT_2:45;
then A481: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A482: M2 is_in_the_area_of f by A477, SPRECT_2:23;
A483: (M2 /. 1) `1 = (f /. ((W-min (L~ f)) .. f)) `1 by A481, A477, SPRECT_2:8
.= (W-min (L~ f)) `1 by A476, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
(M2 /. (len M2)) `1 = (f /. ((E-min (L~ f)) .. f)) `1 by A481, A477, SPRECT_2:9
.= (E-min (L~ f)) `1 by A480, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A484: M2 is_a_h.c._for f by A482, A483, SPRECT_2:def 2;
len M2 >= 2 by TOPREAL1:def 8;
then L~ RB1 meets L~ M2 by A472, A471, A484, SPRECT_2:29;
then L~ M2 meets L~ Red1 by A304, A479, XBOOLE_1:70;
then L~ M2 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A245, A481, A477, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
suppose A485: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ; :: thesis: contradiction
A486: (SW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
set i1 = (S-min (L~ f)) .. f;
set i3 = (E-min (L~ f)) .. f;
A487: (NW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
(N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then (E-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then A488: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A489: E-min (L~ f) in rng f by SPRECT_2:45;
then A490: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A491: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M3 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A488, JORDAN4:40;
L~ M3 misses L~ Red by A57, A245, A490, SPRECT_3:18, XBOOLE_1:63;
then A492: L~ M3 misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A488, A491;
then A493: L~ RB1 misses L~ M3 by A304, A492, XBOOLE_1:70;
A494: M3 /. 1 = f /. 2 by A57, A490, SPRECT_2:8;
then (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) /\ (L~ M3) = {(M3 /. 1)} by A191, A488, A491;
then reconsider M2 = RB1 ^ M3 as S-Sequence_in_R2 by A80, A170, A303, A305, A494, A493, SPRECT_3:21;
A495: (M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A490, SPRECT_2:9
.= (E-min (L~ f)) `1 by A489, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A490, SPRECT_2:23;
then A496: M2 is_in_the_area_of f by A306, SPRECT_2:24;
1 in dom RB1 by FINSEQ_5:6;
then (M2 /. 1) `1 = (RB1 /. 1) `1 by FINSEQ_4:68
.= W-bound (L~ f) by A302, A485, A487, A486, GOBOARD7:5 ;
then A497: M2 is_a_h.c._for f by A496, A495, SPRECT_2:def 2;
A498: L~ M2 = ((L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1)))) \/ (L~ M3) by A303, SPPOL_2:23;
(W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A499: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
(E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then A500: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A501: 2 < (S-min (L~ f)) .. f by A488, XXREAL_0:2;
then A502: 1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A499, JORDAN4:40;
A503: L~ M1 misses L~ M3 by A500, A499, A488, SPRECT_2:47;
A504: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A173, A499, A501;
A505: S-min (L~ f) in rng f by SPRECT_2:41;
then A506: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A507: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A508: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A506, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def 1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A506, SPRECT_2:8
.= (S-min (L~ f)) `2 by A505, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A509: M1 is_a_v.c._for f by A507, A508, SPRECT_2:def 3;
A510: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A499, A502;
A511: len M1 >= 2 by TOPREAL1:def 8;
len M2 >= 2 by TOPREAL1:def 8;
then L~ M1 meets L~ M2 by A511, A509, A497, SPRECT_2:29;
then L~ M1 meets (L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) by A498, A503, XBOOLE_1:70;
then L~ M1 meets L~ RB1 by A494, A504, XBOOLE_1:70;
then L~ M1 meets L~ Red1 by A304, A510, XBOOLE_1:70;
then L~ M1 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence contradiction by A58, A245, A506, SPRECT_3:18, XBOOLE_1:63; :: thesis: verum
end;
end;