let n be Element of NAT ; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let i, j be Element of NAT ; :: thesis:
set Gij = (Gauge C,n) * i,j;
assume that
A1: ( 1 <= i & i <= len (Gauge C,n) ) and
A2: ( 1 <= j & j <= width (Gauge C,n) ) and
A3: (Gauge C,n) * i,j in L~ (Cage C,n) ; :: thesis:
set NE = NE-corner (L~ (Cage C,n));
set v1 = L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j);
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)))*>;
set h = mid (Lower_Seq C,n),2,(len (Lower_Seq C,n));
A4: L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by JORDAN1E:17;
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;
A6: Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) by JORDAN1E:def 1;
A7: ( len (Lower_Seq C,n) >= 3 & len (Upper_Seq C,n) >= 3 ) by JORDAN1E:19;
then A8: ( len (Lower_Seq C,n) >= 2 & len (Lower_Seq C,n) >= 1 & len (Upper_Seq C,n) >= 2 & len (Upper_Seq C,n) >= 1 ) by XXREAL_0:2;
A9: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A10: ((Gauge C,n) * i,1) `2 = S-bound (L~ (Cage C,n)) by A1, JORDAN1A:93;
set Wmi = W-min (L~ (Cage C,n));

now

per cases ) * 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, A3, A4, XBOOLE_0:def 3, XXREAL_0:1;

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

set G11 = (Gauge C,n) * 1,1;
A12: ((Gauge C,n) * 1,1) `1 = W-bound (L~ (Cage C,n)) by A1, A11, JORDAN1A:94;
A13: (W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
A14: S-bound (L~ (Cage C,n)) = ((Gauge C,n) * 1,1) `2 by A1, A11, JORDAN1A:93;
W-min (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:15;
then A15: ((Gauge C,n) * 1,1) `2 <= (W-min (L~ (Cage C,n))) `2 by A14, PSCOMP_1:71;
A16: ((Gauge C,n) * i,j) `1 = W-bound (L~ (Cage C,n)) by A2, A9, A11, JORDAN1A:94;
then (Gauge C,n) * i,j in W-most (L~ (Cage C,n)) by A3, SPRECT_2:16;
then (W-min (L~ (Cage C,n))) `2 <= ((Gauge C,n) * i,j) `2 by PSCOMP_1:88;
then A17: W-min (L~ (Cage C,n)) in LSeg ((Gauge C,n) * 1,1),((Gauge C,n) * 1,j) by A11, A12, A13, A15, A16, GOBOARD7:8;
A18: rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = W-min (L~ (Cage C,n)) by JORDAN1F:8;
then W-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) by REVROT_1:3;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n) by A11, A17, A18, XBOOLE_0:3; :: thesis:

end;

suppose A19: ( (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:

then A20: not L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) <> 0 ;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) > 0 ;
then A21: 0 + 1 <= len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A22: 1 in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
A23: ( 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)) & len (Upper_Seq C,n) in dom (Upper_Seq C,n) ) by A8, A21, FINSEQ_3:27;
A24: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A25: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A26: (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 A23, PARTFUN1:def 8
.= (Upper_Seq C,n) . (len (Upper_Seq C,n)) by A19, JORDAN1B:5
.= (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by A23, PARTFUN1:def 8
.= ((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 A6, A25, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A25, FINSEQ_5:48 ;
then A27: (<*((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 A20, SPRECT_3:11;
A28: (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 A22, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A19, JORDAN3:58 ;
then A29: ((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1 = (Gauge C,n) * i,j by A21, BOOLMARK:8;
A30: 1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A21, XREAL_1:9;
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:19
.= (1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_5:8 ;
then A31: 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 A30, NAT_1:13;
S-bound (L~ (Cage C,n)) < N-bound (L~ (Cage C,n)) by SPRECT_1:34;
then NE-corner (L~ (Cage C,n)) <> (Gauge C,n) * i,1 by A10, EUCLID:56;
then not NE-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,1)} by TARSKI:def 1;
then A32: not NE-corner (L~ (Cage C,n)) in rng <*((Gauge C,n) * i,1)*> by FINSEQ_1:56;
len (Cage C,n) > 4 by GOBOARD7:36;
then A33: rng (Cage C,n) c= L~ (Cage C,n) by SPPOL_2:18, XXREAL_0:2;
A34: not NE-corner (L~ (Cage C,n)) in rng (Cage C,n)

proof

assume A35: NE-corner (L~ (Cage C,n)) in rng (Cage C,n) ; :: thesis:
A36: ( (NE-corner (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) & (NE-corner (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) ) by EUCLID:56;
then (NE-corner (L~ (Cage C,n))) `2 >= S-bound (L~ (Cage C,n)) by SPRECT_1:24;
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 A36;
then NE-corner (L~ (Cage C,n)) in LSeg (SE-corner (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n))) by SPRECT_1:25;
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 A33, A35, XBOOLE_0:def 4;
then A37: (NE-corner (L~ (Cage C,n))) `2 <= (E-max (L~ (Cage C,n))) `2 by PSCOMP_1:108;
(E-max (L~ (Cage C,n))) `2 <= (NE-corner (L~ (Cage C,n))) `2 by PSCOMP_1:107;
then A38: (E-max (L~ (Cage C,n))) `2 = (NE-corner (L~ (Cage C,n))) `2 by A37, XXREAL_0:1;
(E-max (L~ (Cage C,n))) `1 = (NE-corner (L~ (Cage C,n))) `1 by PSCOMP_1:105;
hence contradiction by A19, A38, TOPREAL3:11; :: thesis:

end;

now

per cases ) * 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:

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 4;
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:44;
then A39: 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:55;
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:
then consider i being Element of NAT such that
A40: 1 <= i and
A41: i + 1 <= len (Cage C,n) and
A42: NE-corner (L~ (Cage C,n)) in LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by SPPOL_2:14;

per cases ) /. i) `1 = ((Cage C,n) /. (i + 1)) `1 or ((Cage C,n) /. i) `2 = ((Cage C,n) /. (i + 1)) `2 ) by A40, A41, TOPREAL1:def 7;

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

then A44: (NE-corner (L~ (Cage C,n))) `1 = ((Cage C,n) /. i) `1 by A42, GOBOARD7:5;
A45: (NE-corner (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
A46: i < len (Cage C,n) by A41, NAT_1:13;
then A47: ((Cage C,n) /. i) `2 <= (NE-corner (L~ (Cage C,n))) `2 by A40, A45, JORDAN5D:13;
A48: 1 <= i + 1 by NAT_1:11;
then A49: ((Cage C,n) /. (i + 1)) `2 <= (NE-corner (L~ (Cage C,n))) `2 by A41, A45, JORDAN5D:13;
A50: ( i in dom (Cage C,n) & i + 1 in dom (Cage C,n) ) by A40, A41, A46, A48, FINSEQ_3:27;
( ((Cage C,n) /. i) `2 <= ((Cage C,n) /. (i + 1)) `2 or ((Cage C,n) /. i) `2 >= ((Cage C,n) /. (i + 1)) `2 ) ;
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 A42, TOPREAL1:10;
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 A47, A49, XXREAL_0:1;
then ( NE-corner (L~ (Cage C,n)) = (Cage C,n) /. (i + 1) or NE-corner (L~ (Cage C,n)) = (Cage C,n) /. i ) by A43, A44, TOPREAL3:11;
hence contradiction by A34, A50, PARTFUN2:4; :: thesis:

end;

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

then A52: (NE-corner (L~ (Cage C,n))) `2 = ((Cage C,n) /. i) `2 by A42, GOBOARD7:6;
A53: (NE-corner (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
A54: i < len (Cage C,n) by A41, NAT_1:13;
then A55: ((Cage C,n) /. i) `1 <= (NE-corner (L~ (Cage C,n))) `1 by A40, A53, JORDAN5D:14;
A56: 1 <= i + 1 by NAT_1:11;
then A57: ((Cage C,n) /. (i + 1)) `1 <= (NE-corner (L~ (Cage C,n))) `1 by A41, A53, JORDAN5D:14;
A58: ( i in dom (Cage C,n) & i + 1 in dom (Cage C,n) ) by A40, A41, A54, A56, FINSEQ_3:27;
( ((Cage C,n) /. i) `1 <= ((Cage C,n) /. (i + 1)) `1 or ((Cage C,n) /. i) `1 >= ((Cage C,n) /. (i + 1)) `1 ) ;
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 A42, TOPREAL1:9;
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 A55, A57, XXREAL_0:1;
then ( NE-corner (L~ (Cage C,n)) = (Cage C,n) /. (i + 1) or NE-corner (L~ (Cage C,n)) = (Cage C,n) /. i ) by A51, A52, TOPREAL3:11;
hence contradiction by A34, A58, PARTFUN2:4; :: thesis:

end;

then A59: not NE-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,j)} by A3, TARSKI:def 1;
A60: 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 JORDAN3:28;
rng (Upper_Seq C,n) c= rng (Cage C,n) by Th47;
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 A60, 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 A34;
hence not NE-corner (L~ (Cage C,n)) in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A39, A59, XBOOLE_0:def 3; :: thesis:

end;

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

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 4;
then A61: rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) c= rng (Upper_Seq C,n) by JORDAN3:28;
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 A61, 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 A34; :: thesis:

end;

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 A32, 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:44;
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:56;
then A62: 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:55;
A63: not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) by A1, A19, Th52;
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
then A64: not (Gauge C,n) * i,1 in rng (Upper_Seq C,n) by A1, A19, Th52;
not (Gauge C,n) * i,1 in {((Gauge C,n) * i,j)} by A19, A63, TARSKI:def 1;
then A65: not (Gauge C,n) * i,1 in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;
set ci = mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n));

now

per cases ) * 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 A66: (Gauge C,n) * i,j <> (Upper_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1) ; :: thesis:

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 JORDAN3:28;
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 A64;
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 A65, 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:44;
hence not (Gauge C,n) * i,1 in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A66, JORDAN3:def 4; :: thesis:

end;

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

end;

then {((Gauge C,n) * i,1)} misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A67: rng <*((Gauge C,n) * i,1)*> misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A68: <*((Gauge C,n) * i,1)*> is one-to-one by FINSEQ_3:102;
A69: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A19, JORDAN3:69;
then L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is one-to-one ;
then A70: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A67, A68, FINSEQ_3:98;
<*(NE-corner (L~ (Cage C,n)))*> is one-to-one by FINSEQ_3:102;
then A71: (<*((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 A62, A70, FINSEQ_3:98;
A72: <*((Gauge C,n) * i,1)*> is special by SPPOL_2:39;
A73: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is special by A69;
(<*((Gauge C,n) * i,1)*> /. (len <*((Gauge C,n) * i,1)*>)) `1 = (<*((Gauge C,n) * i,1)*> /. 1) `1 by FINSEQ_1:56
.= ((Gauge C,n) * i,1) `1 by FINSEQ_4:25
.= ((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A28, GOBOARD5:3 ;
then A74: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is special by A72, A73, GOBOARD2:13;
A75: <*(NE-corner (L~ (Cage C,n)))*> is special by SPPOL_2:39;
((<*((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 A27, PSCOMP_1:105
.= (<*(NE-corner (L~ (Cage C,n)))*> /. 1) `1 by FINSEQ_4:25 ;
then A76: (<*((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 A74, A75, GOBOARD2:13;
A77: len (Lower_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A78: len (Lower_Seq C,n) > 2 by NAT_1:13;
A79: len (Lower_Seq C,n) > 1 by A77, XXREAL_0:2;
then mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is S-Sequence_in_R2 by A78, JORDAN3:39;
then Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is S-Sequence_in_R2 by SPPOL_2:47;
then A80: ( 2 <= len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) & Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is one-to-one & Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is special ) by TOPREAL1:def 10;
3 <= len (Lower_Seq C,n) by JORDAN1E:19;
then 2 <= len (Lower_Seq C,n) by XXREAL_0:2;
then A81: 2 in dom (Lower_Seq C,n) by FINSEQ_3:27;
A82: 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 A81, JORDAN1E:22, SPRECT_2:26;
then A83: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_in_the_area_of Cage C,n by SPRECT_3:68;
A84: not mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is empty by A78, A79, JORDAN1B:3;
A85: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A86: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A87: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
then (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, FINSEQ_5:57
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A85, FINSEQ_6:98 ;
then ((Lower_Seq C,n) /. (len (Lower_Seq C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
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 A81, A82, SPRECT_2:13;
then A88: ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A84, FINSEQ_5:68;
A89: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (E-min (L~ (Cage C,n))) .. (Cage C,n) <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:76;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A89, SPRECT_2:75, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A89, SPRECT_2:77, XXREAL_0:2;
then A90: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A89, SPRECT_2:78, XXREAL_0:2;
then A91: (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 A85, A86, SPRECT_5:10;
(len (Cage C,n)) + 0 <= (len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1:8;
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 A91, XREAL_1:11;
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:8;
then A92: 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 A85, FINSEQ_5:53;
1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) <= 0 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A90, 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:22;
then A93: (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:8;
A94: ((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)) ;
A95: (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, A81, A87, FINSEQ_5:55
.= (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 A85, A91, A92, A93, REVROT_1:17
.= (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) by A91, A94, XREAL_0:def 2 ;
(N-max (L~ (Cage C,n))) .. (Cage C,n) <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by A89, SPRECT_2:74;
then A96: (E-max (L~ (Cage C,n))) .. (Cage C,n) > 1 by A89, SPRECT_2:73, XXREAL_0:2;
(E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A89, A90, SPRECT_2:80, XXREAL_0:2;
then A97: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
(Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by A86, FINSEQ_5:41;
then ((Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = E-bound (L~ (Cage C,n)) by A96, A97, JORDAN1E:24;
then ((mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) /. 1) `1 = E-bound (L~ (Cage C,n)) by A81, A82, A95, SPRECT_2:12;
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 A84, FINSEQ_5:68;
then ((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;
then A98: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_a_h.c._for Cage C,n by A83, A88, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis:
assume A99: m in dom <*((Gauge C,n) * i,1)*> ; :: thesis:
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4, TARSKI:def 1;
then <*((Gauge C,n) * i,1)*> . m = (Gauge C,n) * i,1 by FINSEQ_1:57;
then A100: <*((Gauge C,n) * i,1)*> /. m = (Gauge C,n) * i,1 by A99, PARTFUN1:def 8;
width (Gauge C,n) >= 4 by A9, JORDAN8:13;
then A101: 1 <= width (Gauge C,n) by XXREAL_0:2;
then ((Gauge C,n) * 1,1) `1 <= ((Gauge C,n) * i,1) `1 by A1, SPRECT_3:25;
hence W-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,1)*> /. m) `1 by A9, A100, A101, JORDAN1A:94; :: thesis:
((Gauge C,n) * i,1) `1 <= ((Gauge C,n) * (len (Gauge C,n)),1) `1 by A1, A101, SPRECT_3:25;
hence (<*((Gauge C,n) * i,1)*> /. m) `1 <= E-bound (L~ (Cage C,n)) by A9, A100, A101, JORDAN1A:92; :: thesis:
thus S-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,1)*> /. m) `2 by A1, A100, JORDAN1A:93; :: thesis:
S-bound (L~ (Cage C,n)) = ((Gauge C,n) * i,1) `2 by A1, JORDAN1A:93;
hence (<*((Gauge C,n) * i,1)*> /. m) `2 <= N-bound (L~ (Cage C,n)) by A100, SPRECT_1:24; :: thesis:

end;

then A102: <*((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 A19, JORDAN1E:21, SPRECT_3:63;
then L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is_in_the_area_of Cage C,n by A19, JORDAN1E:21, SPRECT_3:73;
then A103: <*((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 A102, SPRECT_2:28;
<*(NE-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:29;
then A104: (<*((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 A103, SPRECT_2:28;
(<*((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:45;
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: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)))*>) /. 1) `2 = S-bound (L~ (Cage C,n)) by A1, JORDAN1A:93;
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:19;
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:82;
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)))*>))) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
then (<*((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 A104, A105, SPRECT_2:def 3;
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 A31, A71, A76, A80, A98, SPRECT_2:33;
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
A106: x in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) and
A107: 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;
A108: L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) c= L~ (Lower_Seq C,n) by A8, JORDAN4:47;
A109: L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Upper_Seq C,n) by A19, JORDAN3:77;
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:45
.= (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 A20, 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 A107, XBOOLE_0:def 3;
(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:56 ;
then A111: not E-max (L~ (Cage C,n)) in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) by A78, JORDAN5B:16;

now

per cases 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:

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

end;

suppose A112: x in L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ; :: thesis:

then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A106, A108, A109, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A113: x = W-min (L~ (Cage C,n)) by A106, A111, TARSKI:def 2;
1 in dom (Upper_Seq C,n) by A8, FINSEQ_3:27;
then (Upper_Seq C,n) . 1 = (Upper_Seq C,n) /. 1 by PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by A6, A25, FINSEQ_5:47
.= W-min (L~ (Cage C,n)) by A24, FINSEQ_6:98 ;
then x = (Gauge C,n) * i,j by A19, A112, A113, JORDAN1E:11;
then x in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) by RLTOPSP1:69;
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 A106, A108, XBOOLE_0:3; :: thesis:

end;

suppose A114: 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:

x in L~ (Cage C,n) by A4, A106, A108, 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 A26, A114, XBOOLE_0:def 4;
then x in {(E-max (L~ (Cage C,n)))} by PSCOMP_1:112;
hence L~ (Lower_Seq C,n) meets L~ <*((Gauge C,n) * i,1),((Gauge C,n) * i,j)*> by A106, A111, TARSKI:def 1; :: thesis:

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:

end;

suppose A115: ( (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:

then A116: not L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) <> 0 ;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) > 0 ;
then A117: 0 + 1 <= len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A118: 1 in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
A119: ( 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)) & len (Upper_Seq C,n) in dom (Upper_Seq C,n) ) by A8, A117, FINSEQ_3:27;
A120: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A121: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
(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 A119, PARTFUN1:def 8
.= (Upper_Seq C,n) . (len (Upper_Seq C,n)) by A115, JORDAN1B:5
.= (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by A119, PARTFUN1:def 8
.= ((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 A6, A121, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A121, FINSEQ_5:48 ;
then A122: (<*((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 A116, SPRECT_3:11;
A123: (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 A118, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A115, JORDAN3:58 ;
1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A117, XREAL_1:9;
then A124: len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 2 by FINSEQ_5:8;
A125: not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) by A1, A115, Th52;
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
then A126: not (Gauge C,n) * i,1 in rng (Upper_Seq C,n) by A1, A115, Th52;
not (Gauge C,n) * i,1 in {((Gauge C,n) * i,j)} by A115, A125, TARSKI:def 1;
then A127: not (Gauge C,n) * i,1 in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;
set ci = mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n));

now

per cases ) * 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 A128: (Gauge C,n) * i,j <> (Upper_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1) ; :: thesis:

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 JORDAN3:28;
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 A126;
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 A127, 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:44;
hence not (Gauge C,n) * i,1 in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A128, JORDAN3:def 4; :: thesis:

end;

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

end;

then {((Gauge C,n) * i,1)} misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A129: rng <*((Gauge C,n) * i,1)*> misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A130: <*((Gauge C,n) * i,1)*> is one-to-one by FINSEQ_3:102;
A131: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A115, JORDAN3:69;
then L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is one-to-one ;
then A132: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A129, A130, FINSEQ_3:98;
A133: <*((Gauge C,n) * i,1)*> is special by SPPOL_2:39;
A134: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is special by A131;
(<*((Gauge C,n) * i,1)*> /. (len <*((Gauge C,n) * i,1)*>)) `1 = (<*((Gauge C,n) * i,1)*> /. 1) `1 by FINSEQ_1:56
.= ((Gauge C,n) * i,1) `1 by FINSEQ_4:25
.= ((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A123, GOBOARD5:3 ;
then A135: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is special by A133, A134, GOBOARD2:13;
A136: len (Lower_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A137: len (Lower_Seq C,n) > 2 by NAT_1:13;
A138: len (Lower_Seq C,n) > 1 by A136, XXREAL_0:2;
then mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is S-Sequence_in_R2 by A137, JORDAN3:39;
then Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is S-Sequence_in_R2 by SPPOL_2:47;
then A139: ( 2 <= len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) & Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is one-to-one & Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is special ) by TOPREAL1:def 10;
3 <= len (Lower_Seq C,n) by JORDAN1E:19;
then 2 <= len (Lower_Seq C,n) by XXREAL_0:2;
then A140: 2 in dom (Lower_Seq C,n) by FINSEQ_3:27;
A141: 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:22, SPRECT_2:26;
then A142: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_in_the_area_of Cage C,n by SPRECT_3:68;
A143: not mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is empty by A137, A138, JORDAN1B:3;
A144: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A145: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A146: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
then (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, FINSEQ_5:57
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A144, FINSEQ_6:98 ;
then ((Lower_Seq C,n) /. (len (Lower_Seq C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
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, A141, SPRECT_2:13;
then A147: ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A143, FINSEQ_5:68;
A148: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (E-min (L~ (Cage C,n))) .. (Cage C,n) <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:76;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A148, SPRECT_2:75, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A148, SPRECT_2:77, XXREAL_0:2;
then A149: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A148, SPRECT_2:78, XXREAL_0:2;
then A150: (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 A144, A145, SPRECT_5:10;
(len (Cage C,n)) + 0 <= (len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1:8;
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 A150, XREAL_1:11;
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:8;
then A151: 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 A144, FINSEQ_5:53;
1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) <= 0 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A149, 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:22;
then A152: (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:8;
A153: ((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)) ;
A154: (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, A146, FINSEQ_5:55
.= (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 A144, A150, A151, A152, REVROT_1:17
.= (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) by A150, A153, XREAL_0:def 2 ;
(N-max (L~ (Cage C,n))) .. (Cage C,n) <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by A148, SPRECT_2:74;
then A155: (E-max (L~ (Cage C,n))) .. (Cage C,n) > 1 by A148, SPRECT_2:73, XXREAL_0:2;
(E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A148, A149, SPRECT_2:80, XXREAL_0:2;
then A156: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
(Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by A145, FINSEQ_5:41;
then ((Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = E-bound (L~ (Cage C,n)) by A155, A156, JORDAN1E:24;
then ((mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) /. 1) `1 = E-bound (L~ (Cage C,n)) by A140, A141, A154, SPRECT_2:12;
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 A143, FINSEQ_5:68;
then ((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;
then A157: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_a_h.c._for Cage C,n by A142, A147, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis:
assume A158: m in dom <*((Gauge C,n) * i,1)*> ; :: thesis:
then m in Seg 1 by FINSEQ_1:55;
then m = 1 by FINSEQ_1:4, TARSKI:def 1;
then <*((Gauge C,n) * i,1)*> . m = (Gauge C,n) * i,1 by FINSEQ_1:57;
then A159: <*((Gauge C,n) * i,1)*> /. m = (Gauge C,n) * i,1 by A158, PARTFUN1:def 8;
width (Gauge C,n) >= 4 by A9, JORDAN8:13;
then A160: 1 <= width (Gauge C,n) by XXREAL_0:2;
then ((Gauge C,n) * 1,1) `1 <= ((Gauge C,n) * i,1) `1 by A1, SPRECT_3:25;
hence W-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,1)*> /. m) `1 by A9, A159, A160, JORDAN1A:94; :: thesis:
((Gauge C,n) * i,1) `1 <= ((Gauge C,n) * (len (Gauge C,n)),1) `1 by A1, A160, SPRECT_3:25;
hence (<*((Gauge C,n) * i,1)*> /. m) `1 <= E-bound (L~ (Cage C,n)) by A9, A159, A160, JORDAN1A:92; :: thesis:
thus S-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,1)*> /. m) `2 by A1, A159, JORDAN1A:93; :: thesis:
S-bound (L~ (Cage C,n)) = ((Gauge C,n) * i,1) `2 by A1, JORDAN1A:93;
hence (<*((Gauge C,n) * i,1)*> /. m) `2 <= N-bound (L~ (Cage C,n)) by A159, SPRECT_1:24; :: thesis:

end;

then A161: <*((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 A115, JORDAN1E:21, SPRECT_3:63;
then L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is_in_the_area_of Cage C,n by A115, JORDAN1E:21, SPRECT_3:73;
then A162: <*((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 A161, SPRECT_2:28;
(<*((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:16;
then A163: ((<*((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, JORDAN1A:93;
((<*((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 A115, A122, EUCLID:56;
then <*((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 A162, A163, SPRECT_2:def 3;
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 A124, A132, A135, A139, A157, SPRECT_2:33;
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
A164: x in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) and
A165: x in L~ (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by XBOOLE_0:3;
A166: L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) c= L~ (Lower_Seq C,n) by A8, JORDAN4:47;
A167: L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Upper_Seq C,n) by A115, JORDAN3:77;
A168: 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 A116, SPPOL_2:20;
(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:56 ;
then A169: not E-max (L~ (Cage C,n)) in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) by A137, JORDAN5B:16;

now

per cases by A165, A168, 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:

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

end;

suppose A170: x in L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ; :: thesis:

then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A164, A166, A167, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A171: x = W-min (L~ (Cage C,n)) by A164, A169, TARSKI:def 2;
1 in dom (Upper_Seq C,n) by A8, FINSEQ_3:27;
then (Upper_Seq C,n) . 1 = (Upper_Seq C,n) /. 1 by PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by A6, A121, FINSEQ_5:47
.= W-min (L~ (Cage C,n)) by A120, FINSEQ_6:98 ;
then x = (Gauge C,n) * i,j by A115, A170, A171, JORDAN1E:11;
then x in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) by RLTOPSP1:69;
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 A164, A166, XBOOLE_0:3; :: thesis:

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:

end;

suppose A172: (Gauge C,n) * i,j in L~ (Lower_Seq C,n) ; :: thesis:

(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) by RLTOPSP1:69;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n) by A172, XBOOLE_0:3; :: thesis:

end;

suppose A173: ( (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:

then not L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) <> 0 ;
then len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) > 0 ;
then 0 + 1 <= len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A174: ( 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)) & len (Upper_Seq C,n) in dom (Upper_Seq C,n) ) by A8, FINSEQ_3:27;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A175: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A176: (Upper_Seq C,n) . (len (Upper_Seq C,n)) = (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by A174, PARTFUN1:def 8
.= ((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 A6, A175, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A175, FINSEQ_5:48 ;
A177: rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
A178: E-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) by A5, FINSEQ_6:66;
(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) by RLTOPSP1:69;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n) by A173, A176, A177, A178, XBOOLE_0:3; :: thesis:

end;

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