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;

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

hence
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
; :: thesis: verumper 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;

end;

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

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

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;

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;

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;

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

A28: now :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))end;

S-bound (L~ (Cage (C,n))) < N-bound (L~ (Cage (C,n)))
by SPRECT_1:32;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) )
;

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))) = <*((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))

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

then A51:
not NE-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,j))}
by A4, TARSKI:def 1;
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;

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

end;

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

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

( 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

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

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

then A74:
<*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n)
by SPRECT_2:def 1;( 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;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

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

then
{((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by ZFMISC_1:50;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) )
;

end;

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

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

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

then
L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> meets L~ (Lower_Seq (C,n))
;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;

end;

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

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

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

hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by SPPOL_2:21; :: thesis: verum

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

<*((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;

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;

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;

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

then A116:
<*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n)
by SPRECT_2:def 1;( 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;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

<*((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))))end;

then
{((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by ZFMISC_1:50;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) )
;

end;

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

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

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

then
L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> meets L~ (Lower_Seq (C,n))
;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;

end;

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

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

hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by SPPOL_2:21; :: thesis: verum

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

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