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 ;
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 ;
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 ;
A12: 1 <= i + 1 by NAT_1:11;
A13: i + 1 <= len (GoB f) by ;
then A14: [(i + 1),(width (GoB f))] in Indices (GoB f) by ;
A15: 1 in dom f by FINSEQ_5:6;
A16: i in dom (GoB f) by ;
then A17: f /. (1 + 1) = (GoB f) * ((i + 1),(width (GoB f))) by ;
then A18: right_cell (f,1) = cell ((GoB f),i,((width (GoB f)) -' 1)) by ;
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 ;
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 ;
A21: Int (right_cell (f,1)) c= RightComp f by ;
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 ;
A27: 1 <= len (GoB f) by ;
A28: (width (GoB f)) -' 1 < width (GoB f) by ;
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 ;
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
.= (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 ;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > ((GoB f) * (1,((width (GoB f)) -' 1))) `1 by ;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > W-bound (L~ f) by ;
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 ;
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 ;
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 ;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 by ;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= E-bound (L~ f) by ;
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 ;
A42: (1 / 2) * (N-bound (L~ f)) > (1 / 2) * (S-bound (L~ f)) by ;
A43: ((GoB f) * ((i + 1),1)) `2 = ((GoB f) * (1,1)) `2 by ;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= ((GoB f) * ((i + 1),1)) `2 by ;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= S-bound (L~ f) by ;
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 ;
A45: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by ;
((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < ((GoB f) * ((i + 1),(width (GoB f)))) `2 by ;
then ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < N-bound (L~ f) by ;
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 ;
RightComp (SpStSeq (L~ f)) = { q where q is Point of () : ( 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 ;
reconsider z1 = z1 as Point of () by A48;
consider P being Subset of () 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 ;
consider Red9 being FinSequence of () 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 ;
A56: L~ (SpStSeq (L~ f)) meets L~ Red9 by ;
A57: 2 in dom f by ;
A58: len f in dom f by FINSEQ_5:6;
A59: (len f) -' 1 >= 1 by ;
(len f) -' 1 <= len f by NAT_D:44;
then A60: (len f) -' 1 in dom f by ;
1 <= len f by ;
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 ;
then Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ (SpStSeq (L~ f)) by ;
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 ;
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 ;
A71: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) is horizontal by ;
1 + 2 <= len f by ;
then A72: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def 6;
len f >= 2 + 1 by ;
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 ;
((len f) -' 2) + 2 = len f by ;
then A75: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) = {(f /. ((len f) -' 1))} by ;
A76: f /. 2 in N-most (L~ f) by ;
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 ;
A78: ((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by
.= (N-min (L~ f)) `1 by ;
A79: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by
.= (N-min (L~ f)) `2 by ;
then A80: (f /. 2) `2 = N-bound (L~ f) by ;
A81: <*((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by ;
<*((GoB f) * (i,((width (GoB f)) -' 1)))*> is_in_the_area_of f by ;
then <*((GoB f) * (i,((width (GoB f)) -' 1))),((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by ;
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 ;
then LSeg ((N-min (L~ f)),(f /. ((len f) -' 1))) is vertical by ;
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 ;
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 ;
then N-min (L~ f) in LSeg ((NW-corner (L~ f)),(f /. 2)) by ;
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
.= ((GoB f) * ((i + 1),(width (GoB f)))) `2 by ;
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 ;
(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 ;
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 ;
LSeg ((f /. ((len f) -' 1)),(f /. (len f))) = LSeg (f,((len f) -' 1)) by ;
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 ;
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 ;
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
.= (1 / 2) * (((N-min (L~ f)) `1) + ((N-min (L~ f)) `1)) by
.= (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 ;
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 ;
hence contradiction by A58, A60, A61, GOBOARD7:29; :: thesis: verum
end;
(1 + 1) + 1 <= len f by ;
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 ;
A104: (((len f) -' 1) -' 1) + 2 = ((len f) -' 2) + 2 by NAT_D:45
.= len f by ;
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 () 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 ;
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 ;
then (len f) -' 1 > 1 by ;
then A113: (len f) -' 1 < len f by NAT_D:51;
then A114: j < len f by ;
then len (mid (f,l,j)) = (j -' l) + 1 by ;
then A115: ii < (j -' l) + 1 by ;
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 ;
per cases ( l = j or l < j ) by ;
suppose AB: l = j ; :: thesis: contradiction
end;
suppose A117: l < j ; :: thesis: contradiction
A118: ii + 1 >= 1 + 1 by ;
ii + l >= ii + 1 by ;
then A119: ii + l >= 1 + 1 by ;
then A120: (ii + l) -' 1 >= 1 by NAT_D:49;
A121: ii + l >= 1 by ;
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 ;
ii + l < ((j -' l) + 1) + l by ;
then ii + l < ((j -' l) + l) + 1 ;
then ii + l < j + 1 by ;
then (len f) -' 1 < j + 1 by ;
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 ;
LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by ;
then A125: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by ;
then LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
then (ii + l) -' 1 <= 1 by ;
then (ii + l) -' 1 = 1 by ;
then p = f /. 1 by ;
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 ;
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 ;
j <= (len f) -' 2 by ;
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 ;
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
.= {(f /. ((len f) -' 1))} by ;
:: 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 () 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 ;
p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by ;
then p in {(N-min (L~ f))} by ;
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 ;
set G = GoB f;
A136: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by ;
(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
.= (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 ;
(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 ;
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 ;
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 () 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 ;
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 ;
then ii < (j -' l) + 1 by ;
then A149: p in LSeg (f,((ii + l) -' 1)) by ;
set k = (ii + l) -' 1;
A150: ii + 1 >= 1 + 1 by ;
(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 ;
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 ;
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 ;
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 ;
then p = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by ;
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 ;
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 ;
then A153: LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
ii + l >= ii + 1 by ;
then ii + l >= 1 + 1 by ;
then A154: (ii + l) -' 1 >= 1 by NAT_D:49;
per cases ) -' 1 <= 1 or ((ii + l) -' 1) + 1 >= (len f) -' 1 ) by ;
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 ;
(ii + l) -' 1 = 1 by ;
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 ;
then ii + l <= j by ;
then A158: ii + l < len f by ;
ii + l >= l by NAT_1:11;
then ii + l >= 1 by ;
then (ii + l) -' 1 < (len f) -' 1 by ;
then A159: (ii + l) -' 1 <= ((len f) -' 1) -' 1 by NAT_D:49;
(ii + l) -' 1 >= ((len f) -' 1) -' 1 by ;
then (ii + l) -' 1 = ((len f) -' 1) -' 1 by ;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in {(f /. ((len f) -' 1))} by ;
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 ;
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 ;
((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by
.= ((GoB f) * (i,(width (GoB f)))) `1 by ;
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 ;
A167: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by ;
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 ;
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
.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-min (L~ f)) `2)) by
.= 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 ;
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 () 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 ;
p in L~ (mid (f,l,j)) by ;
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 ;
then A183: len (mid (f,l,j)) = (j -' l) + 1 by ;
then A184: ii < (j -' l) + 1 by ;
set k = (ii + l) -' 1;
A185: ii + 2 >= 1 + 2 by ;
ii + l > ii + 2 by ;
then ii + l > 1 + 2 by ;
then A186: (ii + l) -' 1 > 1 + 1 by NAT_D:52;
per cases ( l = j or l < j ) by ;
suppose AB: l = j ; :: thesis: contradiction
end;
suppose A187: l < j ; :: thesis: contradiction
A188: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by ;
ii <= j -' l by ;
then ii + l <= j by ;
then ii + l <= len f by ;
then A189: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by ;
then A190: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by ;
then LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;
then ((ii + l) -' 1) + 1 >= len f by ;
then (ii + l) -' 1 >= (len f) -' 1 by NAT_D:53;
then (ii + l) -' 1 = (len f) -' 1 by ;
then p = f /. 1 by ;
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 ;
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 ;
L~ (mid (f,2,j)) = (LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),j))) by ;
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
.= {(f /. 2)} by ;
:: 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 () 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 ;
p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by ;
then p in {(N-min (L~ f))} by ;
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 () 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 ;
A202: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by ;
(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 ;
then p in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by ;
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 ;
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 ;
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 ;
A205: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by ;
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 () 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 ;
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 ;
then ii < (j -' l) + 1 by ;
then A215: p in LSeg (f,((ii + l) -' 1)) by ;
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 ;
(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
.= (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 ;
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 ;
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 ;
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 ;
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 ;
then p = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by ;
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 ;
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 ;
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 ;
ii + l > ii + 1 by ;
then ii + l > 1 + 1 by ;
then A221: (ii + l) -' 1 > 1 by NAT_D:52;
per cases ) -' 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 ;
then A223: (ii + l) -' 1 = 2 by ;
1 + 2 <= len f by ;
then (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in {(f /. (1 + 1))} by ;
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 ;
ii <= j -' l by ;
then ii + l <= j by ;
then ii + l <= len f by ;
then A226: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
(ii + l) -' 1 >= (len f) -' 1 by ;
then (ii + l) -' 1 = (len f) -' 1 by ;
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 ;
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 ;
A228: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) is horizontal by ;
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 ;
A232: L~ f misses L~ Red9 by ;
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 ;
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 ;
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 ;
(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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
then A242: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red by ;
Red is_in_the_area_of SpStSeq (L~ f) by ;
then A243: Red is_in_the_area_of f by SPRECT_3:53;
A244: L~ Red c= L~ Red9 by ;
A245: L~ f misses L~ Red by ;
(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 ;
(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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ; :: 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 ;
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 ;
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~ (