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