let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
let i, j be Nat; :: thesis: ( 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) implies LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) )
set Gij = (Gauge (C,n)) * (i,j);
assume that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) and
A3: ( 1 <= j & j <= width (Gauge (C,n)) ) and
A4: (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
A5: Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) by JORDAN1E:def 2;
set Wmi = W-min (L~ (Cage (C,n)));
set h = mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))));
set v1 = L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)));
set NE = NE-corner (L~ (Cage (C,n)));
set Gv1 = <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))));
set v = (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>;
A6: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:13;
A7: Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) by JORDAN1E:def 1;
A8: len (Upper_Seq (C,n)) >= 3 by JORDAN1E:15;
then A9: len (Upper_Seq (C,n)) >= 1 by XXREAL_0:2;
A10: len (Lower_Seq (C,n)) >= 3 by JORDAN1E:15;
then A11: ( len (Lower_Seq (C,n)) >= 2 & len (Lower_Seq (C,n)) >= 1 ) by XXREAL_0:2;
A12: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A13: ((Gauge (C,n)) * (i,1)) `2 = S-bound (L~ (Cage (C,n))) by A1, A2, JORDAN1A:72;
now :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
per cases ( ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & i = 1 ) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) <> NE-corner (L~ (Cage (C,n))) & i > 1 ) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) = NE-corner (L~ (Cage (C,n))) & i > 1 ) or (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) ) ) by A1, A4, A6, XBOOLE_0:def 3, XXREAL_0:1;
suppose A14: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & i = 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
set G11 = (Gauge (C,n)) * (1,1);
A15: W-min (L~ (Cage (C,n))) in L~ (Cage (C,n)) by SPRECT_1:13;
S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (1,1)) `2 by A2, A14, JORDAN1A:72;
then A16: ( (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) & ((Gauge (C,n)) * (1,1)) `2 <= (W-min (L~ (Cage (C,n)))) `2 ) by A15, EUCLID:52, PSCOMP_1:24;
A17: rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by A10, SPPOL_2:18, XXREAL_0:2;
A18: ((Gauge (C,n)) * (i,j)) `1 = W-bound (L~ (Cage (C,n))) by A3, A12, A14, JORDAN1A:73;
then (Gauge (C,n)) * (i,j) in W-most (L~ (Cage (C,n))) by A4, SPRECT_2:12;
then A19: (W-min (L~ (Cage (C,n)))) `2 <= ((Gauge (C,n)) * (i,j)) `2 by PSCOMP_1:31;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) by JORDAN1F:8;
then A20: W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by FINSEQ_6:168;
((Gauge (C,n)) * (1,1)) `1 = W-bound (L~ (Cage (C,n))) by A2, A14, JORDAN1A:73;
then W-min (L~ (Cage (C,n))) in LSeg (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,j))) by A14, A16, A18, A19, GOBOARD7:7;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by A14, A17, A20, XBOOLE_0:3; :: thesis: verum
end;
suppose A21: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) <> NE-corner (L~ (Cage (C,n))) & i > 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
len (Cage (C,n)) > 4 by GOBOARD7:34;
then A22: rng (Cage (C,n)) c= L~ (Cage (C,n)) by SPPOL_2:18, XXREAL_0:2;
A23: not NE-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
proof
A24: (NE-corner (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
then ( (NE-corner (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) & (NE-corner (L~ (Cage (C,n)))) `2 >= S-bound (L~ (Cage (C,n))) ) by EUCLID:52, SPRECT_1:22;
then NE-corner (L~ (Cage (C,n))) in { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ (Cage (C,n))) & p `2 <= N-bound (L~ (Cage (C,n))) & p `2 >= S-bound (L~ (Cage (C,n))) ) } by A24;
then A25: NE-corner (L~ (Cage (C,n))) in LSeg ((SE-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n))))) by SPRECT_1:23;
assume NE-corner (L~ (Cage (C,n))) in rng (Cage (C,n)) ; :: thesis: contradiction
then NE-corner (L~ (Cage (C,n))) in (LSeg ((SE-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n))) by A22, A25, XBOOLE_0:def 4;
then A26: (NE-corner (L~ (Cage (C,n)))) `2 <= (E-max (L~ (Cage (C,n)))) `2 by PSCOMP_1:47;
A27: (E-max (L~ (Cage (C,n)))) `1 = (NE-corner (L~ (Cage (C,n)))) `1 by PSCOMP_1:45;
(E-max (L~ (Cage (C,n)))) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by PSCOMP_1:46;
then (E-max (L~ (Cage (C,n)))) `2 = (NE-corner (L~ (Cage (C,n)))) `2 by A26, XXREAL_0:1;
hence contradiction by A21, A27, TOPREAL3:6; :: thesis: verum
end;
A28: now :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;
suppose (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = <*((Gauge (C,n)) * (i,j))*> ^ (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:31;
then A29: rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = {((Gauge (C,n)) * (i,j))} \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:38;
not NE-corner (L~ (Cage (C,n))) in L~ (Cage (C,n))
proof
assume NE-corner (L~ (Cage (C,n))) in L~ (Cage (C,n)) ; :: thesis: contradiction
then consider i being Nat such that
A30: 1 <= i and
A31: i + 1 <= len (Cage (C,n)) and
A32: NE-corner (L~ (Cage (C,n))) in LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by SPPOL_2:14;
per cases ( ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 ) by A30, A31, TOPREAL1:def 5;
suppose A33: ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis: contradiction
( ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 ) ;
then A34: ( (NE-corner (L~ (Cage (C,n)))) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or (NE-corner (L~ (Cage (C,n)))) `2 <= ((Cage (C,n)) /. i) `2 ) by A32, TOPREAL1:4;
A35: (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1 by A32, A33, GOBOARD7:5;
A36: 1 <= i + 1 by NAT_1:11;
then A37: i + 1 in dom (Cage (C,n)) by A31, FINSEQ_3:25;
A38: (NE-corner (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
then A39: ((Cage (C,n)) /. (i + 1)) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by A31, A36, JORDAN5D:11;
A40: i < len (Cage (C,n)) by A31, NAT_1:13;
then ((Cage (C,n)) /. i) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by A30, A38, JORDAN5D:11;
then ( (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. (i + 1)) `2 or (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2 ) by A39, A34, XXREAL_0:1;
then A41: ( NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i ) by A33, A35, TOPREAL3:6;
i in dom (Cage (C,n)) by A30, A40, FINSEQ_3:25;
hence contradiction by A23, A37, A41, PARTFUN2:2; :: thesis: verum
end;
suppose A42: ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 ; :: thesis: contradiction
( ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 ) ;
then A43: ( (NE-corner (L~ (Cage (C,n)))) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or (NE-corner (L~ (Cage (C,n)))) `1 <= ((Cage (C,n)) /. i) `1 ) by A32, TOPREAL1:3;
A44: (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2 by A32, A42, GOBOARD7:6;
A45: 1 <= i + 1 by NAT_1:11;
then A46: i + 1 in dom (Cage (C,n)) by A31, FINSEQ_3:25;
A47: (NE-corner (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) by EUCLID:52;
then A48: ((Cage (C,n)) /. (i + 1)) `1 <= (NE-corner (L~ (Cage (C,n)))) `1 by A31, A45, JORDAN5D:12;
A49: i < len (Cage (C,n)) by A31, NAT_1:13;
then ((Cage (C,n)) /. i) `1 <= (NE-corner (L~ (Cage (C,n)))) `1 by A30, A47, JORDAN5D:12;
then ( (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. (i + 1)) `1 or (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1 ) by A48, A43, XXREAL_0:1;
then A50: ( NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i ) by A42, A44, TOPREAL3:6;
i in dom (Cage (C,n)) by A30, A49, FINSEQ_3:25;
hence contradiction by A23, A46, A50, PARTFUN2:2; :: thesis: verum
end;
end;
end;
then A51: not NE-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,j))} by A4, TARSKI:def 1;
( rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) c= rng (Upper_Seq (C,n)) & rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) ) by Th39, FINSEQ_6:119;
then rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) c= rng (Cage (C,n)) ;
then not NE-corner (L~ (Cage (C,n))) in rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by A23;
hence not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A29, A51, XBOOLE_0:def 3; :: thesis: verum
end;
suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then A52: rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) by Th39;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Cage (C,n)) by A52;
hence not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A23; :: thesis: verum
end;
end;
end;
S-bound (L~ (Cage (C,n))) < N-bound (L~ (Cage (C,n))) by SPRECT_1:32;
then NE-corner (L~ (Cage (C,n))) <> (Gauge (C,n)) * (i,1) by A13, EUCLID:52;
then not NE-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,1))} by TARSKI:def 1;
then not NE-corner (L~ (Cage (C,n))) in rng <*((Gauge (C,n)) * (i,1))*> by FINSEQ_1:39;
then not NE-corner (L~ (Cage (C,n))) in (rng <*((Gauge (C,n)) * (i,1))*>) \/ (rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by A28, XBOOLE_0:def 3;
then not NE-corner (L~ (Cage (C,n))) in rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by FINSEQ_1:31;
then rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses {(NE-corner (L~ (Cage (C,n))))} by ZFMISC_1:50;
then A53: rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses rng <*(NE-corner (L~ (Cage (C,n))))*> by FINSEQ_1:38;
A54: len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) = (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_2:16
.= (1 + (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_5:8 ;
A55: not L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is empty by A21, JORDAN1E:3;
then A56: 0 + 1 <= len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by NAT_1:13;
then 1 in dom (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_3:25;
then A57: (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1 = (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . 1 by PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j) by A21, JORDAN3:23 ;
then A58: ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1 = (Gauge (C,n)) * (i,j) by A56, BOOLMARK:7;
1 + (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1 + 1 by A56, XREAL_1:7;
then A59: 2 < len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by A54, NAT_1:13;
A60: L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A21, JORDAN3:34;
(<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> = <*((Gauge (C,n)) * (i,1))*> ^ ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by FINSEQ_1:32;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1 = (Gauge (C,n)) * (i,1) by FINSEQ_5:15;
then A61: (((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1) `2 = S-bound (L~ (Cage (C,n))) by A1, A2, JORDAN1A:72;
len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) = (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_2:16;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>)) = NE-corner (L~ (Cage (C,n))) by FINSEQ_4:67;
then A62: (((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
A63: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:70;
then A64: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A63, SPRECT_2:69, XXREAL_0:2;
(E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:72;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:71, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:73, XXREAL_0:2;
then A65: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:74, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A63, SPRECT_2:76, XXREAL_0:2;
then A66: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A67: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by FINSEQ_5:38;
then A68: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A64, A66, JORDAN1E:20;
A69: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A70: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = ((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A67, A65, SPRECT_5:9;
now :: thesis: for m being Nat st m in dom <*((Gauge (C,n)) * (i,1))*> holds
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
let m be Nat; :: thesis: ( m in dom <*((Gauge (C,n)) * (i,1))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )
assume A71: m in dom <*((Gauge (C,n)) * (i,1))*> ; :: thesis: ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*((Gauge (C,n)) * (i,1))*> . m = (Gauge (C,n)) * (i,1) by FINSEQ_1:40;
then A72: <*((Gauge (C,n)) * (i,1))*> /. m = (Gauge (C,n)) * (i,1) by A71, PARTFUN1:def 6;
width (Gauge (C,n)) >= 4 by A12, JORDAN8:10;
then A73: 1 <= width (Gauge (C,n)) by XXREAL_0:2;
then ((Gauge (C,n)) * (1,1)) `1 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, SPRECT_3:13;
hence W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 by A12, A72, A73, JORDAN1A:73; :: thesis: ( (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A73, SPRECT_3:13;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A72, A73, JORDAN1A:71; :: thesis: ( S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
thus S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 by A1, A2, A72, JORDAN1A:72; :: thesis: (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))
S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2 by A1, A2, JORDAN1A:72;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) by A72, SPRECT_1:22; :: thesis: verum
end;
then A74: <*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n) by SPRECT_2:def 1;
A75: <*(NE-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (C,n) by SPRECT_2:25;
3 <= len (Lower_Seq (C,n)) by JORDAN1E:15;
then 2 <= len (Lower_Seq (C,n)) by XXREAL_0:2;
then A76: 2 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (C,n) by A21, JORDAN1E:17, SPRECT_3:46;
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is_in_the_area_of Cage (C,n) by A21, JORDAN1E:17, SPRECT_3:56;
then <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_in_the_area_of Cage (C,n) by A74, SPRECT_2:24;
then (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (C,n) by A75, SPRECT_2:24;
then A77: (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is_a_v.c._for Cage (C,n) by A61, A62, SPRECT_2:def 3;
A78: ((1 + (((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) - (len (Cage (C,n))) = 1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) ;
A79: len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by FINSEQ_5:6;
then mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is_in_the_area_of Cage (C,n) by A76, JORDAN1E:18, SPRECT_2:22;
then A80: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_in_the_area_of Cage (C,n) by SPRECT_3:51;
1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A65, NAT_1:13;
then (1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 by XREAL_1:20;
then A81: (len (Cage (C,n))) + ((1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) <= (len (Cage (C,n))) + 0 by XREAL_1:6;
A82: len (Lower_Seq (C,n)) >= 2 + 1 by JORDAN1E:15;
then A83: len (Lower_Seq (C,n)) > 2 by NAT_1:13;
(len (Cage (C,n))) + 0 <= (len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:6;
then (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A70, XREAL_1:9;
then ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
then A84: len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A69, FINSEQ_5:50;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A85: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A86: L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Upper_Seq (C,n)) by A21, JORDAN3:42;
A87: len (Lower_Seq (C,n)) > 1 by A82, XXREAL_0:2;
then A88: not mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is empty by A83, JORDAN1B:2;
A89: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A67, FINSEQ_6:90, SPRECT_2:43;
then (Lower_Seq (C,n)) /. (1 + 1) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A5, A76, FINSEQ_5:52
.= (Cage (C,n)) /. (((1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) -' (len (Cage (C,n)))) by A69, A70, A84, A81, FINSEQ_6:182
.= (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A70, A78, XREAL_0:def 2 ;
then ((mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) /. 1) `1 = E-bound (L~ (Cage (C,n))) by A76, A79, A68, SPRECT_2:8;
then ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. (len (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))))) `1 = E-bound (L~ (Cage (C,n))) by A88, FINSEQ_5:65;
then A90: ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. (len (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))))) `1 = E-bound (L~ (Cage (C,n))) by FINSEQ_5:def 3;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A5, A89, FINSEQ_5:54
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage (C,n))) by A69, FINSEQ_6:92 ;
then ((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;
then ((mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) /. (len (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))))) `1 = W-bound (L~ (Cage (C,n))) by A76, A79, SPRECT_2:9;
then ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. 1) `1 = W-bound (L~ (Cage (C,n))) by A88, FINSEQ_5:65;
then A91: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_a_h.c._for Cage (C,n) by A80, A90, SPRECT_2:def 2;
A92: len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;
set ci = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))));
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by A8, SPPOL_2:18, XXREAL_0:2;
then A93: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A2, A21, Th44;
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n)) by A2, A21, Th44;
then not (Gauge (C,n)) * (i,1) in {((Gauge (C,n)) * (i,j))} by A21, TARSKI:def 1;
then A94: not (Gauge (C,n)) * (i,1) in rng <*((Gauge (C,n)) * (i,j))*> by FINSEQ_1:38;
now :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;
suppose A95: (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
then not (Gauge (C,n)) * (i,1) in rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by A93;
then not (Gauge (C,n)) * (i,1) in (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by A94, XBOOLE_0:def 3;
then not (Gauge (C,n)) * (i,1) in rng (<*((Gauge (C,n)) * (i,j))*> ^ (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:31;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A95, JORDAN3:def 3; :: thesis: verum
end;
suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A93; :: thesis: verum
end;
end;
end;
then {((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by ZFMISC_1:50;
then A96: rng <*((Gauge (C,n)) * (i,1))*> misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_1:38;
A97: <*(NE-corner (L~ (Cage (C,n))))*> is one-to-one by FINSEQ_3:93;
(Lower_Seq (C,n)) /. 1 = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) /. 1 by JORDAN1E:def 2
.= E-max (L~ (Cage (C,n))) by FINSEQ_5:53 ;
then A98: not E-max (L~ (Cage (C,n))) in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) by A83, JORDAN5B:16;
<*((Gauge (C,n)) * (i,1))*> is one-to-one by FINSEQ_3:93;
then <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is one-to-one by A96, A60, FINSEQ_3:91;
then A99: (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is one-to-one by A53, A97, FINSEQ_3:91;
A100: L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) c= L~ (Lower_Seq (C,n)) by A11, JORDAN4:35;
(<*((Gauge (C,n)) * (i,1))*> /. (len <*((Gauge (C,n)) * (i,1))*>)) `1 = (<*((Gauge (C,n)) * (i,1))*> /. 1) `1 by FINSEQ_1:39
.= ((Gauge (C,n)) * (i,1)) `1 by FINSEQ_4:16
.= ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1 by A1, A2, A3, A57, GOBOARD5:2 ;
then A101: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is special by A60, GOBOARD2:8;
len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) in dom (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A56, FINSEQ_3:25;
then A102: (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) = (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by PARTFUN1:def 6
.= (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) by A21, JORDAN1B:4
.= (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) by A92, PARTFUN1:def 6
.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A7, A85, FINSEQ_5:42
.= E-max (L~ (Cage (C,n))) by A85, FINSEQ_5:45 ;
then (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) = E-max (L~ (Cage (C,n))) by A55, SPRECT_3:1;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))))) `1 = (NE-corner (L~ (Cage (C,n)))) `1 by PSCOMP_1:45
.= (<*(NE-corner (L~ (Cage (C,n))))*> /. 1) `1 by FINSEQ_4:16 ;
then A103: (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is special by A101, GOBOARD2:8;
mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is S-Sequence_in_R2 by A83, A87, JORDAN3:6;
then A104: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is S-Sequence_in_R2 ;
then 2 <= len (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) by TOPREAL1:def 8;
then L~ (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) meets L~ ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by A59, A99, A103, A104, A91, A77, SPRECT_2:29;
then L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) meets L~ ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by SPPOL_2:22;
then consider x being object such that
A105: x in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) and
A106: x in L~ ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by XBOOLE_0:3;
A107: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
L~ ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) = L~ (<*((Gauge (C,n)) * (i,1))*> ^ ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>)) by FINSEQ_1:32
.= (LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1))) \/ (L~ ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>)) by SPPOL_2:20
.= (LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1))) \/ ((L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) \/ (LSeg (((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(NE-corner (L~ (Cage (C,n))))))) by A55, SPPOL_2:19 ;
then A108: ( x in LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1)) or x in (L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) \/ (LSeg (((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(NE-corner (L~ (Cage (C,n)))))) ) by A106, XBOOLE_0:def 3;
now :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
per cases ( x in LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1)) or x in L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) or x in LSeg (((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(NE-corner (L~ (Cage (C,n))))) ) by A108, XBOOLE_0:def 3;
suppose x in LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1)) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A58, SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A105, A100, XBOOLE_0:3; :: thesis: verum
end;
suppose A109: x in L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A105, A100, A86, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
then A110: x = W-min (L~ (Cage (C,n))) by A105, A98, TARSKI:def 2;
1 in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;
then (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A7, A85, FINSEQ_5:44
.= W-min (L~ (Cage (C,n))) by A107, FINSEQ_6:92 ;
then x = (Gauge (C,n)) * (i,j) by A21, A109, A110, JORDAN1E:7;
then x in LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A105, A100, XBOOLE_0:3; :: thesis: verum
end;
suppose A111: x in LSeg (((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(NE-corner (L~ (Cage (C,n))))) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
x in L~ (Cage (C,n)) by A6, A105, A100, XBOOLE_0:def 3;
then x in (LSeg ((E-max (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n))) by A102, A111, XBOOLE_0:def 4;
then x in {(E-max (L~ (Cage (C,n))))} by PSCOMP_1:51;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A105, A98, TARSKI:def 1; :: thesis: verum
end;
end;
end;
then L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> meets L~ (Lower_Seq (C,n)) ;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by SPPOL_2:21; :: thesis: verum
end;
suppose A112: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) = NE-corner (L~ (Cage (C,n))) & i > 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
now :: thesis: for m being Nat st m in dom <*((Gauge (C,n)) * (i,1))*> holds
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
let m be Nat; :: thesis: ( m in dom <*((Gauge (C,n)) * (i,1))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )
assume A113: m in dom <*((Gauge (C,n)) * (i,1))*> ; :: thesis: ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*((Gauge (C,n)) * (i,1))*> . m = (Gauge (C,n)) * (i,1) by FINSEQ_1:40;
then A114: <*((Gauge (C,n)) * (i,1))*> /. m = (Gauge (C,n)) * (i,1) by A113, PARTFUN1:def 6;
width (Gauge (C,n)) >= 4 by A12, JORDAN8:10;
then A115: 1 <= width (Gauge (C,n)) by XXREAL_0:2;
then ((Gauge (C,n)) * (1,1)) `1 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, SPRECT_3:13;
hence W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 by A12, A114, A115, JORDAN1A:73; :: thesis: ( (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A115, SPRECT_3:13;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A114, A115, JORDAN1A:71; :: thesis: ( S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
thus S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 by A1, A2, A114, JORDAN1A:72; :: thesis: (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))
S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2 by A1, A2, JORDAN1A:72;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) by A114, SPRECT_1:22; :: thesis: verum
end;
then A116: <*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n) by SPRECT_2:def 1;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (C,n) by A112, JORDAN1E:17, SPRECT_3:46;
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is_in_the_area_of Cage (C,n) by A112, JORDAN1E:17, SPRECT_3:56;
then A117: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_in_the_area_of Cage (C,n) by A116, SPRECT_2:24;
A118: len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A119: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A120: not L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is empty by A112, JORDAN1E:3;
then A121: 0 + 1 <= len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by NAT_1:13;
then 1 in dom (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_3:25;
then A122: (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1 = (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . 1 by PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j) by A112, JORDAN3:23 ;
len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) in dom (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A121, FINSEQ_3:25;
then (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) = (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by PARTFUN1:def 6
.= (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) by A112, JORDAN1B:4
.= (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) by A118, PARTFUN1:def 6
.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A7, A119, FINSEQ_5:42
.= E-max (L~ (Cage (C,n))) by A119, FINSEQ_5:45 ;
then (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) = E-max (L~ (Cage (C,n))) by A120, SPRECT_3:1;
then A123: ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))))) `2 = N-bound (L~ (Cage (C,n))) by A112, EUCLID:52;
(<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. 1 = (Gauge (C,n)) * (i,1) by FINSEQ_5:15;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. 1) `2 = S-bound (L~ (Cage (C,n))) by A1, A2, JORDAN1A:72;
then A124: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_a_v.c._for Cage (C,n) by A117, A123, SPRECT_2:def 3;
A125: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:70;
then A126: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A125, SPRECT_2:69, XXREAL_0:2;
(E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A125, SPRECT_2:72;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A125, SPRECT_2:71, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A125, SPRECT_2:73, XXREAL_0:2;
then A127: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A125, SPRECT_2:74, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A125, SPRECT_2:76, XXREAL_0:2;
then A128: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A129: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by FINSEQ_5:38;
then A130: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A126, A128, JORDAN1E:20;
1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A127, NAT_1:13;
then (1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 by XREAL_1:20;
then A131: (len (Cage (C,n))) + ((1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) <= (len (Cage (C,n))) + 0 by XREAL_1:6;
A132: len (Lower_Seq (C,n)) >= 2 + 1 by JORDAN1E:15;
then A133: len (Lower_Seq (C,n)) > 2 by NAT_1:13;
set ci = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))));
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by A8, SPPOL_2:18, XXREAL_0:2;
then A134: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A2, A112, Th44;
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n)) by A2, A112, Th44;
then not (Gauge (C,n)) * (i,1) in {((Gauge (C,n)) * (i,j))} by A112, TARSKI:def 1;
then A135: not (Gauge (C,n)) * (i,1) in rng <*((Gauge (C,n)) * (i,j))*> by FINSEQ_1:38;
now :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;
suppose A136: (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
then not (Gauge (C,n)) * (i,1) in rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by A134;
then not (Gauge (C,n)) * (i,1) in (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by A135, XBOOLE_0:def 3;
then not (Gauge (C,n)) * (i,1) in rng (<*((Gauge (C,n)) * (i,j))*> ^ (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:31;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A136, JORDAN3:def 3; :: thesis: verum
end;
suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A134; :: thesis: verum
end;
end;
end;
then {((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by ZFMISC_1:50;
then A137: rng <*((Gauge (C,n)) * (i,1))*> misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_1:38;
A138: ((1 + (((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) - (len (Cage (C,n))) = 1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) ;
1 + (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1 + 1 by A121, XREAL_1:7;
then A139: len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 2 by FINSEQ_5:8;
3 <= len (Lower_Seq (C,n)) by JORDAN1E:15;
then 2 <= len (Lower_Seq (C,n)) by XXREAL_0:2;
then A140: 2 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;
(Lower_Seq (C,n)) /. 1 = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) /. 1 by JORDAN1E:def 2
.= E-max (L~ (Cage (C,n))) by FINSEQ_5:53 ;
then A141: not E-max (L~ (Cage (C,n))) in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) by A133, JORDAN5B:16;
A142: L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A112, JORDAN3:34;
(<*((Gauge (C,n)) * (i,1))*> /. (len <*((Gauge (C,n)) * (i,1))*>)) `1 = (<*((Gauge (C,n)) * (i,1))*> /. 1) `1 by FINSEQ_1:39
.= ((Gauge (C,n)) * (i,1)) `1 by FINSEQ_4:16
.= ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1 by A1, A2, A3, A122, GOBOARD5:2 ;
then A143: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is special by A142, GOBOARD2:8;
A144: L~ (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) = (LSeg (((Gauge (C,n)) * (i,1)),((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1))) \/ (L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by A120, SPPOL_2:20;
A145: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A146: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = ((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A129, A127, SPRECT_5:9;
(len (Cage (C,n))) + 0 <= (len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:6;
then (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A146, XREAL_1:9;
then ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
then A147: len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A145, FINSEQ_5:50;
A148: len (Lower_Seq (C,n)) > 1 by A132, XXREAL_0:2;
then A149: not mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is empty by A133, JORDAN1B:2;
A150: len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by FINSEQ_5:6;
then mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is_in_the_area_of Cage (C,n) by A140, JORDAN1E:18, SPRECT_2:22;
then A151: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_in_the_area_of Cage (C,n) by SPRECT_3:51;
A152: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A129, FINSEQ_6:90, SPRECT_2:43;
then (Lower_Seq (C,n)) /. (1 + 1) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A5, A140, FINSEQ_5:52
.= (Cage (C,n)) /. (((1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) -' (len (Cage (C,n)))) by A145, A146, A147, A131, FINSEQ_6:182
.= (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A146, A138, XREAL_0:def 2 ;
then ((mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) /. 1) `1 = E-bound (L~ (Cage (C,n))) by A140, A150, A130, SPRECT_2:8;
then ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. (len (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))))) `1 = E-bound (L~ (Cage (C,n))) by A149, FINSEQ_5:65;
then A153: ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. (len (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))))) `1 = E-bound (L~ (Cage (C,n))) by FINSEQ_5:def 3;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A5, A152, FINSEQ_5:54
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage (C,n))) by A145, FINSEQ_6:92 ;
then ((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;
then ((mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) /. (len (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))))) `1 = W-bound (L~ (Cage (C,n))) by A140, A150, SPRECT_2:9;
then ((Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) /. 1) `1 = W-bound (L~ (Cage (C,n))) by A149, FINSEQ_5:65;
then A154: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_a_h.c._for Cage (C,n) by A151, A153, SPRECT_2:def 2;
<*((Gauge (C,n)) * (i,1))*> is one-to-one by FINSEQ_3:93;
then A155: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is one-to-one by A137, A142, FINSEQ_3:91;
A156: L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) c= L~ (Lower_Seq (C,n)) by A11, JORDAN4:35;
mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is S-Sequence_in_R2 by A133, A148, JORDAN3:6;
then A157: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is S-Sequence_in_R2 ;
then 2 <= len (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) by TOPREAL1:def 8;
then L~ (Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))))) meets L~ (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by A139, A155, A143, A157, A154, A124, SPRECT_2:29;
then L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) meets L~ (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by SPPOL_2:22;
then consider x being object such that
A158: x in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) and
A159: x in L~ (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by XBOOLE_0:3;
A160: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
A161: L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Upper_Seq (C,n)) by A112, JORDAN3:42;
now :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
per cases ( x in LSeg (((Gauge (C,n)) * (i,1)),((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1)) or x in L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ) by A159, A144, XBOOLE_0:def 3;
suppose x in LSeg (((Gauge (C,n)) * (i,1)),((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1)) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A122, SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A158, A156, XBOOLE_0:3; :: thesis: verum
end;
suppose A162: x in L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>
then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A158, A156, A161, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
then A163: x = W-min (L~ (Cage (C,n))) by A158, A141, TARSKI:def 2;
1 in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;
then (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A7, A119, FINSEQ_5:44
.= W-min (L~ (Cage (C,n))) by A160, FINSEQ_6:92 ;
then x = (Gauge (C,n)) * (i,j) by A112, A162, A163, JORDAN1E:7;
then x in LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A158, A156, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
then L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> meets L~ (Lower_Seq (C,n)) ;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by SPPOL_2:21; :: thesis: verum
end;
suppose A164: (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
(Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by A164, XBOOLE_0:3; :: thesis: verum
end;
suppose A165: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
A166: (Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
A167: ( rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) ) by A5, A10, FINSEQ_6:61, SPPOL_2:18, XXREAL_0:2;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A168: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by A9, FINSEQ_3:25;
then (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) by PARTFUN1:def 6
.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A7, A168, FINSEQ_5:42
.= E-max (L~ (Cage (C,n))) by A168, FINSEQ_5:45 ;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by A165, A167, A166, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) ; :: thesis: verum