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 = SW-corner (L~ (Cage C,n));
set v1 = L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j);
set wG = width (Gauge C,n);
set lG = len (Gauge C,n);
set Gv1 = <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j));
set v = (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>;
set h = mid (Upper_Seq C,n),2,(len (Upper_Seq C,n));
A4: L~ (Cage C,n) = (L~ (Lower_Seq C,n)) \/ (L~ (Upper_Seq C,n)) by JORDAN1E:17;
A5: ( len (Upper_Seq C,n) >= 3 & len (Lower_Seq C,n) >= 3 ) by JORDAN1E:19;
then A6: ( len (Upper_Seq C,n) >= 2 & len (Upper_Seq C,n) >= 1 & len (Lower_Seq C,n) >= 2 & len (Lower_Seq C,n) >= 1 ) by XXREAL_0:2;
A7: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then width (Gauge C,n) >= 4 by JORDAN8:13;
then A8: 1 <= width (Gauge C,n) by XXREAL_0:2;
A9: ((Gauge C,n) * i,(width (Gauge C,n))) `2 = N-bound (L~ (Cage C,n)) by A1, A7, JORDAN1A:91;
set Ema = E-max (L~ (Cage C,n));

now

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

suppose A10: ( (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & i = len (Gauge C,n) ) ; :: thesis:

set G11 = (Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n));
A11: ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `1 = E-bound (L~ (Cage C,n)) by A1, A7, A10, JORDAN1A:92;
A12: (E-max (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
A13: N-bound (L~ (Cage C,n)) = ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `2 by A1, A7, A10, JORDAN1A:91;
E-max (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:16;
then A14: ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `2 >= (E-max (L~ (Cage C,n))) `2 by A13, PSCOMP_1:71;
A15: ((Gauge C,n) * i,j) `1 = E-bound (L~ (Cage C,n)) by A2, A7, A10, JORDAN1A:92;
then (Gauge C,n) * i,j in E-most (L~ (Cage C,n)) by A3, SPRECT_2:17;
then (E-max (L~ (Cage C,n))) `2 >= ((Gauge C,n) * i,j) `2 by PSCOMP_1:108;
then A16: E-max (L~ (Cage C,n)) in LSeg ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))),((Gauge C,n) * (len (Gauge C,n)),j) by A10, A11, A12, A14, A15, GOBOARD7:8;
A17: rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A5, SPPOL_2:18, XXREAL_0:2;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n)) by JORDAN1F:7;
then E-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) by REVROT_1:3;
hence LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n) by A10, A16, A17, XBOOLE_0:3; :: thesis:

end;

suppose A18: ( (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j <> (Lower_Seq C,n) . (len (Lower_Seq C,n)) & W-min (L~ (Cage C,n)) <> SW-corner (L~ (Cage C,n)) & i < len (Gauge C,n) ) ; :: thesis:

then A19: not L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) <> 0 ;
then len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) > 0 ;
then A20: 0 + 1 <= len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A21: 1 in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
A22: ( len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) & len (Lower_Seq C,n) in dom (Lower_Seq C,n) ) by A6, A20, FINSEQ_3:27;
then A23: (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by PARTFUN1:def 8
.= (Lower_Seq C,n) . (len (Lower_Seq C,n)) by A18, JORDAN1B:5
.= (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by A22, PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
then A24: (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) = W-min (L~ (Cage C,n)) by A19, SPRECT_3:11;
A25: (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1 = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . 1 by A21, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A18, JORDAN3:58 ;
then A26: ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1 = (Gauge C,n) * i,j by A20, BOOLMARK:8;
A27: 1 + (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A20, XREAL_1:9;
len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) = (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_2:19
.= (1 + (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_5:8 ;
then 2 < len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) by A27, NAT_1:13;
then A28: 2 < len (Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by FINSEQ_5:def 3;
S-bound (L~ (Cage C,n)) < N-bound (L~ (Cage C,n)) by SPRECT_1:34;
then SW-corner (L~ (Cage C,n)) <> (Gauge C,n) * i,(width (Gauge C,n)) by A9, EUCLID:56;
then not SW-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,(width (Gauge C,n)))} by TARSKI:def 1;
then A29: not SW-corner (L~ (Cage C,n)) in rng <*((Gauge C,n) * i,(width (Gauge C,n)))*> by FINSEQ_1:56;
len (Cage C,n) > 4 by GOBOARD7:36;
then A30: rng (Cage C,n) c= L~ (Cage C,n) by SPPOL_2:18, XXREAL_0:2;
A31: not SW-corner (L~ (Cage C,n)) in rng (Cage C,n)

proof

assume A32: SW-corner (L~ (Cage C,n)) in rng (Cage C,n) ; :: thesis:
A33: ( (SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) & (SW-corner (L~ (Cage C,n))) `2 = S-bound (L~ (Cage C,n)) ) by EUCLID:56;
then (SW-corner (L~ (Cage C,n))) `2 <= N-bound (L~ (Cage C,n)) by SPRECT_1:24;
then SW-corner (L~ (Cage C,n)) in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ (Cage C,n)) & p `2 <= N-bound (L~ (Cage C,n)) & p `2 >= S-bound (L~ (Cage C,n)) ) } by A33;
then SW-corner (L~ (Cage C,n)) in LSeg (SW-corner (L~ (Cage C,n))),(NW-corner (L~ (Cage C,n))) by SPRECT_1:28;
then SW-corner (L~ (Cage C,n)) in (LSeg (SW-corner (L~ (Cage C,n))),(NW-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A30, A32, XBOOLE_0:def 4;
then A34: (SW-corner (L~ (Cage C,n))) `2 >= (W-min (L~ (Cage C,n))) `2 by PSCOMP_1:88;
(W-min (L~ (Cage C,n))) `2 >= (SW-corner (L~ (Cage C,n))) `2 by PSCOMP_1:87;
then A35: (W-min (L~ (Cage C,n))) `2 = (SW-corner (L~ (Cage C,n))) `2 by A34, XXREAL_0:1;
(W-min (L~ (Cage C,n))) `1 = (SW-corner (L~ (Cage C,n))) `1 by PSCOMP_1:85;
hence contradiction by A18, A35, TOPREAL3:11; :: thesis:

end;

now

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

suppose (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ; :: thesis:

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = <*((Gauge C,n) * i,j)*> ^ (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by JORDAN3:def 4;
then rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) = (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1:44;
then A36: rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) = {((Gauge C,n) * i,j)} \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1:55;
not SW-corner (L~ (Cage C,n)) in L~ (Cage C,n)

proof

assume SW-corner (L~ (Cage C,n)) in L~ (Cage C,n) ; :: thesis:
then consider i being Element of NAT such that
A37: 1 <= i and
A38: i + 1 <= len (Cage C,n) and
A39: SW-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 A37, A38, TOPREAL1:def 7;

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

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

end;

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

then A49: (SW-corner (L~ (Cage C,n))) `2 = ((Cage C,n) /. i) `2 by A39, GOBOARD7:6;
A50: (SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
A51: i < len (Cage C,n) by A38, NAT_1:13;
then A52: ((Cage C,n) /. i) `1 >= (SW-corner (L~ (Cage C,n))) `1 by A37, A50, JORDAN5D:14;
A53: 1 <= i + 1 by NAT_1:11;
then A54: ((Cage C,n) /. (i + 1)) `1 >= (SW-corner (L~ (Cage C,n))) `1 by A38, A50, JORDAN5D:14;
A55: ( i in dom (Cage C,n) & i + 1 in dom (Cage C,n) ) by A37, A38, A51, A53, 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 ( (SW-corner (L~ (Cage C,n))) `1 >= ((Cage C,n) /. (i + 1)) `1 or (SW-corner (L~ (Cage C,n))) `1 >= ((Cage C,n) /. i) `1 ) by A39, TOPREAL1:9;
then ( (SW-corner (L~ (Cage C,n))) `1 = ((Cage C,n) /. (i + 1)) `1 or (SW-corner (L~ (Cage C,n))) `1 = ((Cage C,n) /. i) `1 ) by A52, A54, XXREAL_0:1;
then ( SW-corner (L~ (Cage C,n)) = (Cage C,n) /. (i + 1) or SW-corner (L~ (Cage C,n)) = (Cage C,n) /. i ) by A48, A49, TOPREAL3:11;
hence contradiction by A31, A55, PARTFUN2:4; :: thesis:

end;

then A56: not SW-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,j)} by A3, TARSKI:def 1;
A57: rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by JORDAN3:28;
rng (Lower_Seq C,n) c= rng (Cage C,n) by JORDAN1G:47;
then rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Cage C,n) by A57, XBOOLE_1:1;
then not SW-corner (L~ (Cage C,n)) in rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by A31;
hence not SW-corner (L~ (Cage C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A36, A56, XBOOLE_0:def 3; :: thesis:

end;

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

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)) by JORDAN3:def 4;
then A58: rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= rng (Lower_Seq C,n) by JORDAN3:28;
rng (Lower_Seq C,n) c= rng (Cage C,n) by JORDAN1G:47;
then rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= rng (Cage C,n) by A58, XBOOLE_1:1;
hence not SW-corner (L~ (Cage C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A31; :: thesis:

end;

then not SW-corner (L~ (Cage C,n)) in (rng <*((Gauge C,n) * i,(width (Gauge C,n)))*>) \/ (rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by A29, XBOOLE_0:def 3;
then not SW-corner (L~ (Cage C,n)) in rng (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by FINSEQ_1:44;
then rng (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) misses {(SW-corner (L~ (Cage C,n)))} by ZFMISC_1:56;
then A59: rng (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) misses rng <*(SW-corner (L~ (Cage C,n)))*> by FINSEQ_1:55;
A60: not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) by A1, A18, JORDAN1G:53;
rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A5, SPPOL_2:18, XXREAL_0:2;
then A61: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) by A1, A18, JORDAN1G:53;
not (Gauge C,n) * i,(width (Gauge C,n)) in {((Gauge C,n) * i,j)} by A18, A60, TARSKI:def 1;
then A62: not (Gauge C,n) * i,(width (Gauge C,n)) in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;
set ci = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n));

now

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

suppose A63: (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ; :: thesis:

rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by JORDAN3:28;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by A61;
then not (Gauge C,n) * i,(width (Gauge C,n)) in (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by A62, XBOOLE_0:def 3;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (<*((Gauge C,n) * i,j)*> ^ (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1:44;
hence not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A63, JORDAN3:def 4; :: thesis:

end;

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

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)) by JORDAN3:def 4;
then rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= rng (Lower_Seq C,n) by JORDAN3:28;
hence not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A61; :: thesis:

end;

then {((Gauge C,n) * i,(width (Gauge C,n)))} misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A64: rng <*((Gauge C,n) * i,(width (Gauge C,n)))*> misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A65: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is one-to-one by FINSEQ_3:102;
A66: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A18, JORDAN3:69;
then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is one-to-one ;
then A67: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A64, A65, FINSEQ_3:98;
<*(SW-corner (L~ (Cage C,n)))*> is one-to-one by FINSEQ_3:102;
then A68: (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*> is one-to-one by A59, A67, FINSEQ_3:98;
A69: Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) is one-to-one by A68;
A70: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is special by SPPOL_2:39;
A71: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is special by A66;
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. (len <*((Gauge C,n) * i,(width (Gauge C,n)))*>)) `1 = (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. 1) `1 by FINSEQ_1:56
.= ((Gauge C,n) * i,(width (Gauge C,n))) `1 by FINSEQ_4:25
.= ((Gauge C,n) * i,1) `1 by A1, A8, GOBOARD5:3
.= ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A25, GOBOARD5:3 ;
then A72: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is special by A70, A71, GOBOARD2:13;
A73: <*(SW-corner (L~ (Cage C,n)))*> is special by SPPOL_2:39;
((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))))) `1 = (SW-corner (L~ (Cage C,n))) `1 by A24, PSCOMP_1:85
.= (<*(SW-corner (L~ (Cage C,n)))*> /. 1) `1 by FINSEQ_4:25 ;
then (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*> is special by A72, A73, GOBOARD2:13;
then A74: Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) is special by SPPOL_2:42;
A75: len (Upper_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A76: len (Upper_Seq C,n) > 2 by NAT_1:13;
len (Upper_Seq C,n) > 1 by A75, XXREAL_0:2;
then mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is S-Sequence_in_R2 by A76, JORDAN3:39;
then A77: ( 2 <= len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) & mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is one-to-one & mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is special ) by TOPREAL1:def 10;
3 <= len (Upper_Seq C,n) by JORDAN1E:19;
then 2 <= len (Upper_Seq C,n) by XXREAL_0:2;
then A78: 2 in dom (Upper_Seq C,n) by FINSEQ_3:27;
A79: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A80: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_in_the_area_of Cage C,n by A78, JORDAN1E:21, SPRECT_2:26;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n)) by JORDAN1F:7;
then ((Upper_Seq C,n) /. (len (Upper_Seq C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
then A81: ((mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) /. (len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))))) `1 = E-bound (L~ (Cage C,n)) by A78, A79, SPRECT_2:13;
((Upper_Seq C,n) /. (1 + 1)) `1 = W-bound (L~ (Cage C,n)) by JORDAN1G:39;
then ((mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A78, A79, SPRECT_2:12;
then A82: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_a_h.c._for Cage C,n by A80, A81, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis:
assume A83: m in dom <*((Gauge C,n) * i,(width (Gauge C,n)))*> ; :: 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,(width (Gauge C,n)))*> . m = (Gauge C,n) * i,(width (Gauge C,n)) by FINSEQ_1:57;
then A84: <*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m = (Gauge C,n) * i,(width (Gauge C,n)) by A83, PARTFUN1:def 8;
((Gauge C,n) * 1,(width (Gauge C,n))) `1 <= ((Gauge C,n) * i,(width (Gauge C,n))) `1 by A1, A8, SPRECT_3:25;
hence W-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `1 by A7, A8, A84, JORDAN1A:94; :: thesis:
((Gauge C,n) * i,(width (Gauge C,n))) `1 <= ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `1 by A1, A8, SPRECT_3:25;
hence (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `1 <= E-bound (L~ (Cage C,n)) by A7, A8, A84, JORDAN1A:92; :: thesis:
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 = N-bound (L~ (Cage C,n)) by A1, A7, A84, JORDAN1A:91;
hence S-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 by SPRECT_1:24; :: thesis:
thus (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 <= N-bound (L~ (Cage C,n)) by A1, A7, A84, JORDAN1A:91; :: thesis:

end;

then A85: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:def 1;
<*((Gauge C,n) * i,j)*> is_in_the_area_of Cage C,n by A18, JORDAN1E:22, SPRECT_3:63;
then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is_in_the_area_of Cage C,n by A18, JORDAN1E:22, SPRECT_3:73;
then A86: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is_in_the_area_of Cage C,n by A85, SPRECT_2:28;
<*(SW-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:32;
then (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by A86, SPRECT_2:28;
then A87: Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) is_in_the_area_of Cage C,n by SPRECT_3:68;
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*> = <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) by FINSEQ_1:45;
then ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1 = (Gauge C,n) * i,(width (Gauge C,n)) by FINSEQ_5:16;
then (((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1) `2 = N-bound (L~ (Cage C,n)) by A1, A7, JORDAN1A:91;
then ((Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) /. (len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>))) `2 = N-bound (L~ (Cage C,n)) by FINSEQ_5:68;
then A88: ((Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) /. (len (Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)))) `2 = N-bound (L~ (Cage C,n)) by FINSEQ_5:def 3;
len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) = (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_2:19;
then ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. (len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) = SW-corner (L~ (Cage C,n)) by FINSEQ_4:82;
then (((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. (len ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>))) `2 = S-bound (L~ (Cage C,n)) by EUCLID:56;
then ((Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) /. 1) `2 = S-bound (L~ (Cage C,n)) by FINSEQ_5:68;
then Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) is_a_v.c._for Cage C,n by A87, A88, SPRECT_2:def 3;
then L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) meets L~ (Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by A28, A69, A74, A77, A82, SPRECT_2:33;
then L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) meets L~ ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) by SPPOL_2:22;
then consider x being set such that
A89: x in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) and
A90: x in L~ ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) by XBOOLE_0:3;
A91: L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) c= L~ (Upper_Seq C,n) by A6, JORDAN4:47;
A92: L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Lower_Seq C,n) by A18, JORDAN3:77;
L~ ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>) = L~ (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by FINSEQ_1:45
.= (LSeg ((Gauge C,n) * i,(width (Gauge C,n))),(((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1)) \/ (L~ ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by SPPOL_2:20
.= (LSeg ((Gauge C,n) * i,(width (Gauge C,n))),(((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1)) \/ ((L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) \/ (LSeg ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))),(SW-corner (L~ (Cage C,n))))) by A19, SPPOL_2:19 ;
then A93: ( x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),(((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1) or x in (L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) \/ (LSeg ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))),(SW-corner (L~ (Cage C,n)))) ) by A90, XBOOLE_0:def 3;
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by JORDAN1F:5;
then A94: not W-min (L~ (Cage C,n)) in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) by A76, JORDAN5B:16;

now

per cases by A93, XBOOLE_0:def 3;

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

then x in L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A26, SPPOL_2:21;
hence L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A89, A91, XBOOLE_0:3; :: thesis:

end;

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

then x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n)) by A89, A91, A92, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A96: x = E-max (L~ (Cage C,n)) by A89, A94, TARSKI:def 2;
1 in dom (Lower_Seq C,n) by A6, FINSEQ_3:27;
then (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
then x = (Gauge C,n) * i,j by A18, A95, A96, JORDAN1E:11;
then x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) by RLTOPSP1:69;
then x in L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by SPPOL_2:21;
hence L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A89, A91, XBOOLE_0:3; :: thesis:

end;

suppose A97: x in LSeg ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))),(SW-corner (L~ (Cage C,n))) ; :: thesis:

x in L~ (Cage C,n) by A4, A89, A91, XBOOLE_0:def 3;
then x in (LSeg (W-min (L~ (Cage C,n))),(SW-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A23, A97, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n)))} by PSCOMP_1:92;
hence L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A89, A94, TARSKI:def 1; :: thesis:

end;

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

end;

suppose A98: ( (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j <> (Lower_Seq C,n) . (len (Lower_Seq C,n)) & W-min (L~ (Cage C,n)) = SW-corner (L~ (Cage C,n)) & i < len (Gauge C,n) ) ; :: thesis:

then A99: not L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) <> 0 ;
then len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) > 0 ;
then A100: 0 + 1 <= len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A101: 1 in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
set v = <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j));
A102: ( len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) & len (Lower_Seq C,n) in dom (Lower_Seq C,n) ) by A6, A100, FINSEQ_3:27;
then (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by PARTFUN1:def 8
.= (Lower_Seq C,n) . (len (Lower_Seq C,n)) by A98, JORDAN1B:5
.= (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by A102, PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
then A103: (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) = W-min (L~ (Cage C,n)) by A99, SPRECT_3:11;
A104: (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1 = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . 1 by A101, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A98, JORDAN3:58 ;
1 + (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A100, XREAL_1:9;
then 2 <= len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by FINSEQ_5:8;
then A105: 2 <= len (Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) by FINSEQ_5:def 3;
A106: not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) by A1, A98, JORDAN1G:53;
rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A5, SPPOL_2:18, XXREAL_0:2;
then A107: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) by A1, A98, JORDAN1G:53;
not (Gauge C,n) * i,(width (Gauge C,n)) in {((Gauge C,n) * i,j)} by A98, A106, TARSKI:def 1;
then A108: not (Gauge C,n) * i,(width (Gauge C,n)) in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;
set ci = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n));

now

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

suppose A109: (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ; :: thesis:

rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by JORDAN3:28;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by A107;
then not (Gauge C,n) * i,(width (Gauge C,n)) in (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by A108, XBOOLE_0:def 3;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (<*((Gauge C,n) * i,j)*> ^ (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1:44;
hence not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A109, JORDAN3:def 4; :: thesis:

end;

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

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)) by JORDAN3:def 4;
then rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= rng (Lower_Seq C,n) by JORDAN3:28;
hence not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A107; :: thesis:

end;

then {((Gauge C,n) * i,(width (Gauge C,n)))} misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A110: rng <*((Gauge C,n) * i,(width (Gauge C,n)))*> misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A111: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is one-to-one by FINSEQ_3:102;
A112: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A98, JORDAN3:69;
then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is one-to-one ;
then A113: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A110, A111, FINSEQ_3:98;
A114: Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) is one-to-one by A113;
A115: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is special by SPPOL_2:39;
A116: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is special by A112;
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. (len <*((Gauge C,n) * i,(width (Gauge C,n)))*>)) `1 = (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. 1) `1 by FINSEQ_1:56
.= ((Gauge C,n) * i,(width (Gauge C,n))) `1 by FINSEQ_4:25
.= ((Gauge C,n) * i,1) `1 by A1, A8, GOBOARD5:3
.= ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A104, GOBOARD5:3 ;
then <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is special by A115, A116, GOBOARD2:13;
then A117: Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) is special by SPPOL_2:42;
A118: len (Upper_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A119: len (Upper_Seq C,n) > 2 by NAT_1:13;
len (Upper_Seq C,n) > 1 by A118, XXREAL_0:2;
then mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is S-Sequence_in_R2 by A119, JORDAN3:39;
then A120: ( 2 <= len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) & mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is one-to-one & mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is special ) by TOPREAL1:def 10;
3 <= len (Upper_Seq C,n) by JORDAN1E:19;
then 2 <= len (Upper_Seq C,n) by XXREAL_0:2;
then A121: 2 in dom (Upper_Seq C,n) by FINSEQ_3:27;
A122: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A123: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_in_the_area_of Cage C,n by A121, JORDAN1E:21, SPRECT_2:26;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n)) by JORDAN1F:7;
then ((Upper_Seq C,n) /. (len (Upper_Seq C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
then A124: ((mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) /. (len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))))) `1 = E-bound (L~ (Cage C,n)) by A121, A122, SPRECT_2:13;
((Upper_Seq C,n) /. (1 + 1)) `1 = W-bound (L~ (Cage C,n)) by JORDAN1G:39;
then ((mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A121, A122, SPRECT_2:12;
then A125: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_a_h.c._for Cage C,n by A123, A124, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis:
assume A126: m in dom <*((Gauge C,n) * i,(width (Gauge C,n)))*> ; :: 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,(width (Gauge C,n)))*> . m = (Gauge C,n) * i,(width (Gauge C,n)) by FINSEQ_1:57;
then A127: <*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m = (Gauge C,n) * i,(width (Gauge C,n)) by A126, PARTFUN1:def 8;
((Gauge C,n) * 1,(width (Gauge C,n))) `1 <= ((Gauge C,n) * i,(width (Gauge C,n))) `1 by A1, A8, SPRECT_3:25;
hence W-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `1 by A7, A8, A127, JORDAN1A:94; :: thesis:
((Gauge C,n) * i,(width (Gauge C,n))) `1 <= ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `1 by A1, A8, SPRECT_3:25;
hence (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `1 <= E-bound (L~ (Cage C,n)) by A7, A8, A127, JORDAN1A:92; :: thesis:
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 = N-bound (L~ (Cage C,n)) by A1, A7, A127, JORDAN1A:91;
hence S-bound (L~ (Cage C,n)) <= (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 by SPRECT_1:24; :: thesis:
thus (<*((Gauge C,n) * i,(width (Gauge C,n)))*> /. m) `2 <= N-bound (L~ (Cage C,n)) by A1, A7, A127, JORDAN1A:91; :: thesis:

end;

then A128: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:def 1;
<*((Gauge C,n) * i,j)*> is_in_the_area_of Cage C,n by A98, JORDAN1E:22, SPRECT_3:63;
then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is_in_the_area_of Cage C,n by A98, JORDAN1E:22, SPRECT_3:73;
then <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is_in_the_area_of Cage C,n by A128, SPRECT_2:28;
then A129: Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) is_in_the_area_of Cage C,n by SPRECT_3:68;
(<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. 1 = (Gauge C,n) * i,(width (Gauge C,n)) by FINSEQ_5:16;
then ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. 1) `2 = N-bound (L~ (Cage C,n)) by A1, A7, JORDAN1A:91;
then ((Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))))) `2 = N-bound (L~ (Cage C,n)) by FINSEQ_5:68;
then A130: ((Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) /. (len (Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))))) `2 = N-bound (L~ (Cage C,n)) by FINSEQ_5:def 3;
((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))))) `2 = S-bound (L~ (Cage C,n)) by A98, A103, EUCLID:56;
then ((Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) /. 1) `2 = S-bound (L~ (Cage C,n)) by FINSEQ_5:68;
then Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) is_a_v.c._for Cage C,n by A129, A130, SPRECT_2:def 3;
then L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) meets L~ (Rev (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) by A105, A114, A117, A120, A125, SPRECT_2:33;
then L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) meets L~ (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by SPPOL_2:22;
then consider x being set such that
A131: x in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) and
A132: x in L~ (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by XBOOLE_0:3;
A133: L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) c= L~ (Upper_Seq C,n) by A6, JORDAN4:47;
A134: L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Lower_Seq C,n) by A98, JORDAN3:77;
A135: L~ (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) = (LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1)) \/ (L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by A99, SPPOL_2:20;
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by JORDAN1F:5;
then A136: not W-min (L~ (Cage C,n)) in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) by A119, JORDAN5B:16;

now

per cases by A132, A135, XBOOLE_0:def 3;

suppose x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) ; :: thesis:

then x in L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A104, SPPOL_2:21;
hence L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A131, A133, XBOOLE_0:3; :: thesis:

end;

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

then x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n)) by A131, A133, A134, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A138: x = E-max (L~ (Cage C,n)) by A131, A136, TARSKI:def 2;
1 in dom (Lower_Seq C,n) by A6, FINSEQ_3:27;
then (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
then x = (Gauge C,n) * i,j by A98, A137, A138, JORDAN1E:11;
then x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) by RLTOPSP1:69;
then x in L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by SPPOL_2:21;
hence L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A131, A133, XBOOLE_0:3; :: thesis:

end;

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

(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) by RLTOPSP1:69;
hence LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n) by A139, XBOOLE_0:3; :: thesis:

end;

suppose A140: ( (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j = (Lower_Seq C,n) . (len (Lower_Seq C,n)) ) ; :: thesis:

len (Lower_Seq C,n) in dom (Lower_Seq C,n) by A6, FINSEQ_3:27;
then A141: (Lower_Seq C,n) . (len (Lower_Seq C,n)) = (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
A142: rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A5, SPPOL_2:18, XXREAL_0:2;
A143: W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) by JORDAN1J:5;
(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) by RLTOPSP1:69;
hence LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n) by A140, A141, A142, A143, XBOOLE_0:3; :: thesis:

end;

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