let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Element of 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 Element of 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 Element of 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

per cases ( ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & i = 1 ) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) <> NE-corner (L~ (Cage (C,n))) & i > 1 ) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) = NE-corner (L~ (Cage (C,n))) & i > 1 ) or (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) or ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) ) ) by A1, A4, A6, XBOOLE_0:def 3, XXREAL_0:1;

suppose A14: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & i = 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))

set G11 = (Gauge (C,n)) * (1,1);
A15: W-min (L~ (Cage (C,n))) in L~ (Cage (C,n)) by SPRECT_1:13;
S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (1,1)) `2 by A2, A14, JORDAN1A:72;
then A16: ( (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) & ((Gauge (C,n)) * (1,1)) `2 <= (W-min (L~ (Cage (C,n)))) `2 ) by A15, EUCLID:52, PSCOMP_1:24;
A17: rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by A10, SPPOL_2:18, XXREAL_0:2;
A18: ((Gauge (C,n)) * (i,j)) `1 = W-bound (L~ (Cage (C,n))) by A3, A12, A14, JORDAN1A:73;
then (Gauge (C,n)) * (i,j) in W-most (L~ (Cage (C,n))) by A4, SPRECT_2:12;
then A19: (W-min (L~ (Cage (C,n)))) `2 <= ((Gauge (C,n)) * (i,j)) `2 by PSCOMP_1:31;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) by JORDAN1F:8;
then A20: W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by REVROT_1:3;
((Gauge (C,n)) * (1,1)) `1 = W-bound (L~ (Cage (C,n))) by A2, A14, JORDAN1A:73;
then W-min (L~ (Cage (C,n))) in LSeg (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,j))) by A14, A16, A18, A19, GOBOARD7:7;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by A14, A17, A20, XBOOLE_0:3; :: thesis: verum

end;

suppose A21: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) <> NE-corner (L~ (Cage (C,n))) & i > 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))

len (Cage (C,n)) > 4 by GOBOARD7:34;
then A22: rng (Cage (C,n)) c= L~ (Cage (C,n)) by SPPOL_2:18, XXREAL_0:2;
A23: not NE-corner (L~ (Cage (C,n))) in rng (Cage (C,n))

proof

A24: (NE-corner (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
then ( (NE-corner (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) & (NE-corner (L~ (Cage (C,n)))) `2 >= S-bound (L~ (Cage (C,n))) ) by EUCLID:52, SPRECT_1:22;
then NE-corner (L~ (Cage (C,n))) in { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ (Cage (C,n))) & p `2 <= N-bound (L~ (Cage (C,n))) & p `2 >= S-bound (L~ (Cage (C,n))) ) } by A24;
then A25: NE-corner (L~ (Cage (C,n))) in LSeg ((SE-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n))))) by SPRECT_1:23;
assume NE-corner (L~ (Cage (C,n))) in rng (Cage (C,n)) ; :: thesis: contradiction
then NE-corner (L~ (Cage (C,n))) in (LSeg ((SE-corner (L~ (Cage (C,n)))),(NE-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n))) by A22, A25, XBOOLE_0:def 4;
then A26: (NE-corner (L~ (Cage (C,n)))) `2 <= (E-max (L~ (Cage (C,n)))) `2 by PSCOMP_1:47;
A27: (E-max (L~ (Cage (C,n)))) `1 = (NE-corner (L~ (Cage (C,n)))) `1 by PSCOMP_1:45;
(E-max (L~ (Cage (C,n)))) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by PSCOMP_1:46;
then (E-max (L~ (Cage (C,n)))) `2 = (NE-corner (L~ (Cage (C,n)))) `2 by A26, XXREAL_0:1;
hence contradiction by A21, A27, TOPREAL3:6; :: thesis: verum

end;

A28: now

per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;

suppose (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))

then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = <*((Gauge (C,n)) * (i,j))*> ^ (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:31;
then A29: rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = {((Gauge (C,n)) * (i,j))} \/ (rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))))) by FINSEQ_1:38;
not NE-corner (L~ (Cage (C,n))) in L~ (Cage (C,n))

proof

assume NE-corner (L~ (Cage (C,n))) in L~ (Cage (C,n)) ; :: thesis: contradiction
then consider i being Element of NAT such that
A30: 1 <= i and
A31: i + 1 <= len (Cage (C,n)) and
A32: NE-corner (L~ (Cage (C,n))) in LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by SPPOL_2:14;

per cases ( ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 ) by A30, A31, TOPREAL1:def 5;

suppose A33: ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis: contradiction

( ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 ) ;
then A34: ( (NE-corner (L~ (Cage (C,n)))) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or (NE-corner (L~ (Cage (C,n)))) `2 <= ((Cage (C,n)) /. i) `2 ) by A32, TOPREAL1:4;
A35: (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1 by A32, A33, GOBOARD7:5;
A36: 1 <= i + 1 by NAT_1:11;
then A37: i + 1 in dom (Cage (C,n)) by A31, FINSEQ_3:25;
A38: (NE-corner (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
then A39: ((Cage (C,n)) /. (i + 1)) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by A31, A36, JORDAN5D:11;
A40: i < len (Cage (C,n)) by A31, NAT_1:13;
then ((Cage (C,n)) /. i) `2 <= (NE-corner (L~ (Cage (C,n)))) `2 by A30, A38, JORDAN5D:11;
then ( (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. (i + 1)) `2 or (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2 ) by A39, A34, XXREAL_0:1;
then A41: ( NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i ) by A33, A35, TOPREAL3:6;
i in dom (Cage (C,n)) by A30, A40, FINSEQ_3:25;
hence contradiction by A23, A37, A41, PARTFUN2:2; :: thesis: verum

end;

suppose A42: ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 ; :: thesis: contradiction

( ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 ) ;
then A43: ( (NE-corner (L~ (Cage (C,n)))) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or (NE-corner (L~ (Cage (C,n)))) `1 <= ((Cage (C,n)) /. i) `1 ) by A32, TOPREAL1:3;
A44: (NE-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2 by A32, A42, GOBOARD7:6;
A45: 1 <= i + 1 by NAT_1:11;
then A46: i + 1 in dom (Cage (C,n)) by A31, FINSEQ_3:25;
A47: (NE-corner (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) by EUCLID:52;
then A48: ((Cage (C,n)) /. (i + 1)) `1 <= (NE-corner (L~ (Cage (C,n)))) `1 by A31, A45, JORDAN5D:12;
A49: i < len (Cage (C,n)) by A31, NAT_1:13;
then ((Cage (C,n)) /. i) `1 <= (NE-corner (L~ (Cage (C,n)))) `1 by A30, A47, JORDAN5D:12;
then ( (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. (i + 1)) `1 or (NE-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1 ) by A48, A43, XXREAL_0:1;
then A50: ( NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or NE-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i ) by A42, A44, TOPREAL3:6;
i in dom (Cage (C,n)) by A30, A49, FINSEQ_3:25;
hence contradiction by A23, A46, A50, PARTFUN2:2; :: thesis: verum

end;

end;

end;

then A51: not NE-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,j))} by A4, TARSKI:def 1;
( rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) c= rng (Upper_Seq (C,n)) & rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) ) by Th47, 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)) by XBOOLE_1:1;
then not NE-corner (L~ (Cage (C,n))) in rng (mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n))))) by A23;
hence not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A29, A51, XBOOLE_0:def 3; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))

then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then A52: rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) by Th47;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Cage (C,n)) by A52, XBOOLE_1:1;
hence not NE-corner (L~ (Cage (C,n))) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A23; :: thesis: verum

end;

end;

end;

S-bound (L~ (Cage (C,n))) < N-bound (L~ (Cage (C,n))) by SPRECT_1:32;
then NE-corner (L~ (Cage (C,n))) <> (Gauge (C,n)) * (i,1) by A13, EUCLID:52;
then not NE-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,1))} by TARSKI:def 1;
then not NE-corner (L~ (Cage (C,n))) in rng <*((Gauge (C,n)) * (i,1))*> by FINSEQ_1:39;
then not NE-corner (L~ (Cage (C,n))) in (rng <*((Gauge (C,n)) * (i,1))*>) \/ (rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by A28, XBOOLE_0:def 3;
then not NE-corner (L~ (Cage (C,n))) in rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by FINSEQ_1:31;
then rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses {(NE-corner (L~ (Cage (C,n))))} by ZFMISC_1:50;
then A53: rng (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses rng <*(NE-corner (L~ (Cage (C,n))))*> by FINSEQ_1:38;
A54: len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) = (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_2:16
.= (1 + (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_5:8 ;
A55: not L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is empty by A21, JORDAN1E:3;
then A56: 0 + 1 <= len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by NAT_1:13;
then 1 in dom (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_3:25;
then A57: (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1 = (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . 1 by PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j) by A21, JORDAN3:23 ;
then A58: ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1 = (Gauge (C,n)) * (i,j) by A56, BOOLMARK:7;
1 + (len (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1 + 1 by A56, XREAL_1:7;
then A59: 2 < len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by A54, NAT_1:13;
A60: L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A21, JORDAN3:34;
(<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> = <*((Gauge (C,n)) * (i,1))*> ^ ((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) by FINSEQ_1:32;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1 = (Gauge (C,n)) * (i,1) by FINSEQ_5:15;
then A61: (((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1) `2 = S-bound (L~ (Cage (C,n))) by A1, A2, JORDAN1A:72;
len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) = (len (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1 by FINSEQ_2:16;
then ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>)) = NE-corner (L~ (Cage (C,n))) by FINSEQ_4:67;
then A62: (((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*>))) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52;
A63: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:70;
then A64: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A63, SPRECT_2:69, XXREAL_0:2;
(E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:72;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:71, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:73, XXREAL_0:2;
then A65: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A63, SPRECT_2:74, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A63, SPRECT_2:76, XXREAL_0:2;
then A66: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A67: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by FINSEQ_5:38;
then A68: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A64, A66, JORDAN1E:20;
A69: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A70: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = ((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A67, A65, SPRECT_5:9;

now

let m be Element of NAT ; :: thesis: ( m in dom <*((Gauge (C,n)) * (i,1))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )
assume A71: m in dom <*((Gauge (C,n)) * (i,1))*> ; :: thesis: ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 & (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
then m in Seg 1 by FINSEQ_1:38;
then m = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*((Gauge (C,n)) * (i,1))*> . m = (Gauge (C,n)) * (i,1) by FINSEQ_1:40;
then A72: <*((Gauge (C,n)) * (i,1))*> /. m = (Gauge (C,n)) * (i,1) by A71, PARTFUN1:def 6;
width (Gauge (C,n)) >= 4 by A12, JORDAN8:10;
then A73: 1 <= width (Gauge (C,n)) by XXREAL_0:2;
then ((Gauge (C,n)) * (1,1)) `1 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, SPRECT_3:13;
hence W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `1 by A12, A72, A73, JORDAN1A:73; :: thesis: ( (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A73, SPRECT_3:13;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A72, A73, JORDAN1A:71; :: thesis: ( S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 & (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
thus S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,1))*> /. m) `2 by A1, A2, A72, JORDAN1A:72; :: thesis: (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))
S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2 by A1, A2, JORDAN1A:72;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) by A72, SPRECT_1:22; :: thesis: verum

end;

then A74: <*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n) by SPRECT_2:def 1;
A75: <*(NE-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (C,n) by SPRECT_2:25;
3 <= len (Lower_Seq (C,n)) by JORDAN1E:15;
then 2 <= len (Lower_Seq (C,n)) by XXREAL_0:2;
then A76: 2 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (C,n) by A21, JORDAN1E:17, SPRECT_3:46;
then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is_in_the_area_of Cage (C,n) by A21, JORDAN1E:17, SPRECT_3:56;
then <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_in_the_area_of Cage (C,n) by A74, SPRECT_2:24;
then (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (C,n) by A75, SPRECT_2:24;
then A77: (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(NE-corner (L~ (Cage (C,n))))*> is_a_v.c._for Cage (C,n) by A61, A62, SPRECT_2:def 3;
A78: ((1 + (((len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) - (len (Cage (C,n))) = 1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) ;
A79: len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by FINSEQ_5:6;
then mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is_in_the_area_of Cage (C,n) by A76, JORDAN1E:18, SPRECT_2:22;
then A80: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_in_the_area_of Cage (C,n) by SPRECT_3:51;
1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A65, NAT_1:13;
then (1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 by XREAL_1:20;
then A81: (len (Cage (C,n))) + ((1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) <= (len (Cage (C,n))) + 0 by XREAL_1:6;
A82: len (Lower_Seq (C,n)) >= 2 + 1 by JORDAN1E:15;
then A83: len (Lower_Seq (C,n)) > 2 by NAT_1:13;
(len (Cage (C,n))) + 0 <= (len (Cage (C,n))) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:6;
then (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A70, XREAL_1:9;
then ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
then A84: len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) <= 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A69, FINSEQ_5:50;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A85: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A86: L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Upper_Seq (C,n)) by A21, JORDAN3:42;
A88: len (Lower_Seq (C,n)) > 1 by A82, XXREAL_0:2;
then A89: not mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is empty by A83, JORDAN1B:2;
A90: 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, REVROT_1:17
.= (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 A89, FINSEQ_5:65;
then A91: ((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, A90, 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 A89, FINSEQ_5:65;
then A92: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_a_h.c._for Cage (C,n) by A80, A91, SPRECT_2:def 2;
A93: 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 A95: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A2, A21, Th52;
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n)) by A2, A21, Th52;
then not (Gauge (C,n)) * (i,1) in {((Gauge (C,n)) * (i,j))} by A21, TARSKI:def 1;
then A96: not (Gauge (C,n)) * (i,1) in rng <*((Gauge (C,n)) * (i,j))*> by FINSEQ_1:38;

now

per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;

suppose A97: (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 A95;
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 A96, 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 A97, JORDAN3:def 3; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))

then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A95; :: thesis: verum

end;

end;

end;

then {((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by ZFMISC_1:50;
then A98: rng <*((Gauge (C,n)) * (i,1))*> misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_1:38;
A99: <*(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 A100: 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 A98, A60, FINSEQ_3:91;
then A101: (<*((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, A99, FINSEQ_3:91;
A102: 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 A103: <*((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 A104: (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 A93, 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 A105: (<*((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 A103, GOBOARD2:8;
mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is S-Sequence_in_R2 by A83, A88, JORDAN3:6;
then A106: 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, A101, A105, A106, A92, 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 set such that
A107: x in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) and
A108: 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;
A109: 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 A110: ( 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 A108, XBOOLE_0:def 3;

now

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 A110, XBOOLE_0:def 3;

suppose x in LSeg (((Gauge (C,n)) * (i,1)),(((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(NE-corner (L~ (Cage (C,n))))*>) /. 1)) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>

then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A58, SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A107, A102, XBOOLE_0:3; :: thesis: verum

end;

suppose A111: 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 A107, A102, A86, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
then A112: x = W-min (L~ (Cage (C,n))) by A107, A100, 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 A109, FINSEQ_6:92 ;
then x = (Gauge (C,n)) * (i,j) by A21, A111, A112, 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 A107, A102, XBOOLE_0:3; :: thesis: verum

end;

suppose A113: 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, A107, A102, 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 A104, A113, 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 A107, A100, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose A114: ( (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) & E-max (L~ (Cage (C,n))) = NE-corner (L~ (Cage (C,n))) & i > 1 ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))

now

let m be Element of 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 A115: 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 A116: <*((Gauge (C,n)) * (i,1))*> /. m = (Gauge (C,n)) * (i,1) by A115, PARTFUN1:def 6;
width (Gauge (C,n)) >= 4 by A12, JORDAN8:10;
then A117: 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, A116, A117, 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, A117, SPRECT_3:13;
hence (<*((Gauge (C,n)) * (i,1))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A116, A117, 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, A116, 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 A116, SPRECT_1:22; :: thesis: verum

end;

then A118: <*((Gauge (C,n)) * (i,1))*> is_in_the_area_of Cage (C,n) by SPRECT_2:def 1;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (C,n) by A114, 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 A114, JORDAN1E:17, SPRECT_3:56;
then A119: <*((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 A118, SPRECT_2:24;
A121: 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 A122: 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;
A123: not L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is empty by A114, JORDAN1E:3;
then A124: 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 A125: (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 A114, 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 A124, 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 A114, JORDAN1B:4
.= (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) by A121, 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, A122, FINSEQ_5:42
.= E-max (L~ (Cage (C,n))) by A122, 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 A123, SPRECT_3:1;
then A126: ((<*((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 A114, 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 A127: <*((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 A119, A126, SPRECT_2:def 3;
A128: (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 A129: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A128, 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 A128, SPRECT_2:72;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A128, 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 A128, SPRECT_2:73, XXREAL_0:2;
then A130: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A128, SPRECT_2:74, XXREAL_0:2;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A128, SPRECT_2:76, XXREAL_0:2;
then A131: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
A132: 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 A133: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A129, A131, JORDAN1E:20;
1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= 0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A130, 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 A134: (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;
A135: len (Lower_Seq (C,n)) >= 2 + 1 by JORDAN1E:15;
then A136: 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 A137: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A2, A114, Th52;
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n)) by A2, A114, Th52;
then not (Gauge (C,n)) * (i,1) in {((Gauge (C,n)) * (i,j))} by A114, TARSKI:def 1;
then A138: not (Gauge (C,n)) * (i,1) in rng <*((Gauge (C,n)) * (i,j))*> by FINSEQ_1:38;

now

per cases ( (Gauge (C,n)) * (i,j) <> (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ) ;

suppose A139: (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 A137;
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 A138, 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 A139, JORDAN3:def 3; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Upper_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1) ; :: thesis: not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))

then L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) = mid ((Upper_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Upper_Seq (C,n)))) + 1),(len (Upper_Seq (C,n)))) by JORDAN3:def 3;
then rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Upper_Seq (C,n)) by FINSEQ_6:119;
hence not (Gauge (C,n)) * (i,1) in rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A137; :: thesis: verum

end;

end;

end;

then {((Gauge (C,n)) * (i,1))} misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by ZFMISC_1:50;
then A140: rng <*((Gauge (C,n)) * (i,1))*> misses rng (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_1:38;
A141: ((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 A124, XREAL_1:7;
then A142: 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 A143: 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 A144: not E-max (L~ (Cage (C,n))) in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) by A136, JORDAN5B:16;
A145: L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A114, 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, A125, GOBOARD5:2 ;
then A146: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is special by A145, GOBOARD2:8;
A147: 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 A123, SPPOL_2:20;
A148: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A149: (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 A132, A130, 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 A149, 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 A150: 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 A148, FINSEQ_5:50;
A151: len (Lower_Seq (C,n)) > 1 by A135, XXREAL_0:2;
then A152: not mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n)))) is empty by A136, JORDAN1B:2;
A153: 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 A143, JORDAN1E:18, SPRECT_2:22;
then A154: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_in_the_area_of Cage (C,n) by SPRECT_3:51;
A155: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A132, 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, A143, 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 A148, A149, A150, A134, REVROT_1:17
.= (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) by A149, A141, 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 A143, A153, A133, 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 A152, FINSEQ_5:65;
then A156: ((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, A155, 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 A148, 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 A143, A153, 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 A152, FINSEQ_5:65;
then A157: Rev (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) is_a_h.c._for Cage (C,n) by A154, A156, SPRECT_2:def 2;
<*((Gauge (C,n)) * (i,1))*> is one-to-one by FINSEQ_3:93;
then A158: <*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is one-to-one by A140, A145, FINSEQ_3:91;
A159: 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 A136, A151, JORDAN3:6;
then A160: 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 A142, A158, A146, A160, A157, A127, 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 set such that
A161: x in L~ (mid ((Lower_Seq (C,n)),2,(len (Lower_Seq (C,n))))) and
A162: x in L~ (<*((Gauge (C,n)) * (i,1))*> ^ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j))))) by XBOOLE_0:3;
A163: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
A164: L~ (L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Upper_Seq (C,n)) by A114, JORDAN3:42;

now

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 A162, A147, XBOOLE_0:def 3;

suppose x in LSeg (((Gauge (C,n)) * (i,1)),((L_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1)) ; :: thesis: L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*>

then x in L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A125, SPPOL_2:21;
hence L~ (Lower_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))*> by A161, A159, XBOOLE_0:3; :: thesis: verum

end;

suppose A165: 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 A161, A159, A164, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
then A166: x = W-min (L~ (Cage (C,n))) by A161, A144, 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, A122, FINSEQ_5:44
.= W-min (L~ (Cage (C,n))) by A163, FINSEQ_6:92 ;
then x = (Gauge (C,n)) * (i,j) by A114, A165, A166, 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 A161, A159, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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

end;

suppose A167: (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 A167, XBOOLE_0:3; :: thesis: verum

end;

suppose A168: ( (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))

A169: (Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
A170: ( 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 A171: 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, A171, FINSEQ_5:42
.= E-max (L~ (Cage (C,n))) by A171, FINSEQ_5:45 ;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n)) by A168, A170, A169, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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