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,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j being 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,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_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,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n) )
set Gij = (Gauge C,n) * i,j;
assume that
A1: 1 <= i and
A2: i <= len (Gauge C,n) and
A3: 1 <= j and
A4: j <= width (Gauge C,n) and
A5: (Gauge C,n) * i,j in L~ (Cage C,n) ; :: thesis: LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n)
set NE = SW-corner (L~ (Cage C,n));
set v1 = L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j);
set wG = width (Gauge C,n);
set lG = len (Gauge C,n);
set Gv1 = <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j));
set v = (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>;
set h = mid (Upper_Seq C,n),2,(len (Upper_Seq C,n));
A6: L~ (Cage C,n) = (L~ (Lower_Seq C,n)) \/ (L~ (Upper_Seq C,n)) by JORDAN1E:17;
A7: len (Upper_Seq C,n) >= 3 by JORDAN1E:19;
A8: len (Lower_Seq C,n) >= 3 by JORDAN1E:19;
A9: len (Upper_Seq C,n) >= 2 by A7, XXREAL_0:2;
A10: len (Upper_Seq C,n) >= 1 by A7, XXREAL_0:2;
A11: len (Lower_Seq C,n) >= 1 by A8, XXREAL_0:2;
A12: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then width (Gauge C,n) >= 4 by JORDAN8:13;
then A13: 1 <= width (Gauge C,n) by XXREAL_0:2;
A14: ((Gauge C,n) * i,(width (Gauge C,n))) `2 = N-bound (L~ (Cage C,n)) by A1, A2, A12, JORDAN1A:91;
set Ema = E-max (L~ (Cage C,n));

now

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

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

set G11 = (Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n));
A16: ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `1 = E-bound (L~ (Cage C,n)) by A1, A12, A15, JORDAN1A:92;
A17: (E-max (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
A18: N-bound (L~ (Cage C,n)) = ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `2 by A1, A12, A15, JORDAN1A:91;
E-max (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:16;
then A19: ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))) `2 >= (E-max (L~ (Cage C,n))) `2 by A18, PSCOMP_1:71;
A20: ((Gauge C,n) * i,j) `1 = E-bound (L~ (Cage C,n)) by A3, A4, A12, A15, JORDAN1A:92;
then (Gauge C,n) * i,j in E-most (L~ (Cage C,n)) by A5, SPRECT_2:17;
then (E-max (L~ (Cage C,n))) `2 >= ((Gauge C,n) * i,j) `2 by PSCOMP_1:108;
then A21: E-max (L~ (Cage C,n)) in LSeg ((Gauge C,n) * (len (Gauge C,n)),(width (Gauge C,n))),((Gauge C,n) * (len (Gauge C,n)),j) by A15, A16, A17, A19, A20, GOBOARD7:8;
A22: rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n)) by JORDAN1F:7;
then E-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) by 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 A15, A21, A22, XBOOLE_0:3; :: thesis: verum

end;

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

then A24: not L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then A25: 0 + 1 <= len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A26: 1 in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
A27: len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A25, FINSEQ_3:27;
A28: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by A11, FINSEQ_3:27;
A29: (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by A27, PARTFUN1:def 8
.= (Lower_Seq C,n) . (len (Lower_Seq C,n)) by A23, JORDAN1B:5
.= (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by A28, PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
then A30: (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))) = W-min (L~ (Cage C,n)) by A24, SPRECT_3:11;
A31: (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1 = (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) . 1 by A26, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A23, JORDAN3:58 ;
then A32: ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1 = (Gauge C,n) * i,j by A25, BOOLMARK:8;
A33: 1 + (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A25, 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 A33, NAT_1:13;
then A34: 2 < len (Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by FINSEQ_5:def 3;
S-bound (L~ (Cage C,n)) < N-bound (L~ (Cage C,n)) by SPRECT_1:34;
then SW-corner (L~ (Cage C,n)) <> (Gauge C,n) * i,(width (Gauge C,n)) by A14, EUCLID:56;
then not SW-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,(width (Gauge C,n)))} by TARSKI:def 1;
then A35: not SW-corner (L~ (Cage C,n)) in rng <*((Gauge C,n) * i,(width (Gauge C,n)))*> by FINSEQ_1:56;
len (Cage C,n) > 4 by GOBOARD7:36;
then A36: rng (Cage C,n) c= L~ (Cage C,n) by SPPOL_2:18, XXREAL_0:2;
A37: not SW-corner (L~ (Cage C,n)) in rng (Cage C,n)

proof

assume A38: SW-corner (L~ (Cage C,n)) in rng (Cage C,n) ; :: thesis: contradiction
A39: (SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
A40: (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 A39, A40;
then SW-corner (L~ (Cage C,n)) in LSeg (SW-corner (L~ (Cage C,n))),(NW-corner (L~ (Cage C,n))) by SPRECT_1: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 A36, A38, XBOOLE_0:def 4;
then A41: (SW-corner (L~ (Cage C,n))) `2 >= (W-min (L~ (Cage C,n))) `2 by PSCOMP_1:88;
(W-min (L~ (Cage C,n))) `2 >= (SW-corner (L~ (Cage C,n))) `2 by PSCOMP_1:87;
then A42: (W-min (L~ (Cage C,n))) `2 = (SW-corner (L~ (Cage C,n))) `2 by A41, XXREAL_0:1;
(W-min (L~ (Cage C,n))) `1 = (SW-corner (L~ (Cage C,n))) `1 by PSCOMP_1:85;
hence contradiction by A23, A42, TOPREAL3:11; :: thesis: verum

end;

now

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

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

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = <*((Gauge C,n) * i,j)*> ^ (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by JORDAN3:def 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 A43: rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) = {((Gauge C,n) * i,j)} \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1: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: contradiction
then consider i being Element of NAT such that
A44: 1 <= i and
A45: i + 1 <= len (Cage C,n) and
A46: SW-corner (L~ (Cage C,n)) in LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by SPPOL_2:14;

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

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

then A48: (SW-corner (L~ (Cage C,n))) `1 = ((Cage C,n) /. i) `1 by A46, GOBOARD7:5;
A49: (SW-corner (L~ (Cage C,n))) `2 = S-bound (L~ (Cage C,n)) by EUCLID:56;
A50: i < len (Cage C,n) by A45, NAT_1:13;
then A51: ((Cage C,n) /. i) `2 >= (SW-corner (L~ (Cage C,n))) `2 by A44, A49, JORDAN5D:13;
A52: 1 <= i + 1 by NAT_1:11;
then A53: ((Cage C,n) /. (i + 1)) `2 >= (SW-corner (L~ (Cage C,n))) `2 by A45, A49, JORDAN5D:13;
A54: i in dom (Cage C,n) by A44, A50, FINSEQ_3:27;
A55: i + 1 in dom (Cage C,n) by A45, A52, 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 A46, 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 A51, A53, XXREAL_0:1;
then ( SW-corner (L~ (Cage C,n)) = (Cage C,n) /. (i + 1) or SW-corner (L~ (Cage C,n)) = (Cage C,n) /. i ) by A47, A48, TOPREAL3:11;
hence contradiction by A37, A54, A55, PARTFUN2:4; :: thesis: verum

end;

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

then A57: (SW-corner (L~ (Cage C,n))) `2 = ((Cage C,n) /. i) `2 by A46, GOBOARD7:6;
A58: (SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
A59: i < len (Cage C,n) by A45, NAT_1:13;
then A60: ((Cage C,n) /. i) `1 >= (SW-corner (L~ (Cage C,n))) `1 by A44, A58, JORDAN5D:14;
A61: 1 <= i + 1 by NAT_1:11;
then A62: ((Cage C,n) /. (i + 1)) `1 >= (SW-corner (L~ (Cage C,n))) `1 by A45, A58, JORDAN5D:14;
A63: i in dom (Cage C,n) by A44, A59, FINSEQ_3:27;
A64: i + 1 in dom (Cage C,n) by A45, A61, 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 A46, 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 A60, A62, XXREAL_0:1;
then ( SW-corner (L~ (Cage C,n)) = (Cage C,n) /. (i + 1) or SW-corner (L~ (Cage C,n)) = (Cage C,n) /. i ) by A56, A57, TOPREAL3:11;
hence contradiction by A37, A63, A64, PARTFUN2:4; :: thesis: verum

end;

end;

end;

then A65: not SW-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,j)} by A5, TARSKI:def 1;
A66: rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by FINSEQ_6:125;
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 A66, 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 A37;
hence not SW-corner (L~ (Cage C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A43, A65, XBOOLE_0:def 3; :: thesis: verum

end;

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

then L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) = mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)) by JORDAN3:def 4;
then A67: rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= rng (Lower_Seq C,n) by FINSEQ_6:125;
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 A67, 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 A37; :: thesis: verum

end;

end;

end;

then not SW-corner (L~ (Cage C,n)) in (rng <*((Gauge C,n) * i,(width (Gauge C,n)))*>) \/ (rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by A35, XBOOLE_0:def 3;
then not SW-corner (L~ (Cage C,n)) in rng (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) by FINSEQ_1: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 A68: rng (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) misses rng <*(SW-corner (L~ (Cage C,n)))*> by FINSEQ_1:55;
A69: not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) by A1, A23, JORDAN1G:53;
rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A8, SPPOL_2:18, XXREAL_0:2;
then A70: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) by A1, A23, JORDAN1G:53;
not (Gauge C,n) * i,(width (Gauge C,n)) in {((Gauge C,n) * i,j)} by A23, A69, TARSKI:def 1;
then A71: not (Gauge C,n) * i,(width (Gauge C,n)) in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1: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 ( (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) or (Gauge C,n) * i,j = (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ) ;

suppose A72: (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ; :: thesis: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))

rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by FINSEQ_6:125;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) by A70;
then not (Gauge C,n) * i,(width (Gauge C,n)) in (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by A71, XBOOLE_0:def 3;
then not (Gauge C,n) * i,(width (Gauge C,n)) in rng (<*((Gauge C,n) * i,j)*> ^ (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n)))) by FINSEQ_1: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 A72, JORDAN3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

then {((Gauge C,n) * i,(width (Gauge C,n)))} misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A73: rng <*((Gauge C,n) * i,(width (Gauge C,n)))*> misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A74: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is one-to-one by FINSEQ_3:102;
A75: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A23, JORDAN3:69;
then A76: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A73, A74, FINSEQ_3:98;
<*(SW-corner (L~ (Cage C,n)))*> is one-to-one by FINSEQ_3:102;
then A77: (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*> is one-to-one by A68, A76, FINSEQ_3:98;
A78: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is special ;
(<*((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, A2, A13, GOBOARD5:3
.= ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A3, A4, A31, GOBOARD5:3 ;
then A79: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is special by A75, A78, GOBOARD2:13;
A80: <*(SW-corner (L~ (Cage C,n)))*> is special ;
((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))))) `1 = (SW-corner (L~ (Cage C,n))) `1 by A30, PSCOMP_1: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 A79, A80, GOBOARD2:13;
then A81: 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;
A82: len (Upper_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A83: len (Upper_Seq C,n) > 2 by NAT_1:13;
len (Upper_Seq C,n) > 1 by A82, XXREAL_0:2;
then A84: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is S-Sequence_in_R2 by A83, JORDAN3:39;
then A85: 2 <= len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) 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 A86: 2 in dom (Upper_Seq C,n) by FINSEQ_3:27;
A87: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A88: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_in_the_area_of Cage C,n by A86, 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 A89: ((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 A86, A87, 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 A86, A87, SPRECT_2:12;
then A90: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_a_h.c._for Cage C,n by A88, A89, SPRECT_2:def 2;

now

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

end;

then A93: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:def 1;
<*((Gauge C,n) * i,j)*> is_in_the_area_of Cage C,n by A23, JORDAN1E: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 A23, JORDAN1E:22, SPRECT_3:73;
then A94: <*((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 A93, 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 A94, SPRECT_2:28;
then A95: 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, A2, A12, 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 A96: ((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 A95, A96, SPRECT_2:def 3;
then L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) meets L~ (Rev ((<*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) ^ <*(SW-corner (L~ (Cage C,n)))*>)) by A34, A77, A81, A84, A85, A90, 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
A97: x in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) and
A98: 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;
A99: L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) c= L~ (Upper_Seq C,n) by A9, A10, JORDAN4:47;
A100: L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Lower_Seq C,n) by A23, 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 A24, SPPOL_2:19 ;
then A101: ( 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 A98, XBOOLE_0:def 3;
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by JORDAN1F:5;
then A102: not W-min (L~ (Cage C,n)) in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) by A83, JORDAN5B:16;

now

per cases ( x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),(((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ^ <*(SW-corner (L~ (Cage C,n)))*>) /. 1) or x in L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) or x in LSeg ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)))),(SW-corner (L~ (Cage C,n))) ) by A101, XBOOLE_0:def 3;

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

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

end;

suppose A103: x in L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ; :: thesis: L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*>

then x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n)) by A97, A99, A100, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A104: x = E-max (L~ (Cage C,n)) by A97, A102, TARSKI:def 2;
1 in dom (Lower_Seq C,n) by A11, 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 A23, A103, A104, 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 A97, A99, XBOOLE_0:3; :: thesis: verum

end;

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

x in L~ (Cage C,n) by A6, A97, A99, XBOOLE_0:def 3;
then x in (LSeg (W-min (L~ (Cage C,n))),(SW-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A29, A105, 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 A97, A102, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then A107: not L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is empty by JORDAN1E:7;
then A108: 0 + 1 <= len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then A109: 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));
A110: len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by A108, FINSEQ_3:27;
A111: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by A11, FINSEQ_3:27;
(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 A110, PARTFUN1:def 8
.= (Lower_Seq C,n) . (len (Lower_Seq C,n)) by A106, JORDAN1B:5
.= (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by A111, PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
then A112: (<*((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 A107, SPRECT_3:11;
A113: (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 A109, PARTFUN1:def 8
.= (Gauge C,n) * i,j by A106, JORDAN3:58 ;
1 + (len (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A108, 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 A114: 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;
A115: not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) by A1, A106, JORDAN1G:53;
rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by A8, SPPOL_2:18, XXREAL_0:2;
then A116: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) by A1, A106, JORDAN1G:53;
not (Gauge C,n) * i,(width (Gauge C,n)) in {((Gauge C,n) * i,j)} by A106, A115, TARSKI:def 1;
then A117: 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 ( (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) or (Gauge C,n) * i,j = (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ) ;

suppose A118: (Gauge C,n) * i,j <> (Lower_Seq C,n) . ((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1) ; :: thesis: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j))

rng (mid (Lower_Seq C,n),((Index ((Gauge C,n) * i,j),(Lower_Seq C,n)) + 1),(len (Lower_Seq C,n))) c= rng (Lower_Seq C,n) by FINSEQ_6:125;
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 A116;
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 A117, 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 A118, JORDAN3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

then {((Gauge C,n) * i,(width (Gauge C,n)))} misses rng (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A119: 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;
A120: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is one-to-one by FINSEQ_3:102;
A121: L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A106, JORDAN3:69;
then A122: <*((Gauge C,n) * i,(width (Gauge C,n)))*> ^ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A119, A120, FINSEQ_3:98;
A123: <*((Gauge C,n) * i,(width (Gauge C,n)))*> is special ;
(<*((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, A2, A13, GOBOARD5:3
.= ((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) `1 by A1, A2, A3, A4, A113, 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 A121, A123, GOBOARD2:13;
then A124: 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;
A125: len (Upper_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A126: len (Upper_Seq C,n) > 2 by NAT_1:13;
len (Upper_Seq C,n) > 1 by A125, XXREAL_0:2;
then A127: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is S-Sequence_in_R2 by A126, JORDAN3:39;
then A128: 2 <= len (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) 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 A129: 2 in dom (Upper_Seq C,n) by FINSEQ_3:27;
A130: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A131: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_in_the_area_of Cage C,n by A129, 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 A132: ((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 A129, A130, 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 A129, A130, SPRECT_2:12;
then A133: mid (Upper_Seq C,n),2,(len (Upper_Seq C,n)) is_a_h.c._for Cage C,n by A131, A132, SPRECT_2:def 2;

now

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

end;

then A136: <*((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 A106, 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 A106, 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 A136, SPRECT_2:28;
then A137: 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, A2, A12, 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 A138: ((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 A106, A112, 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 A137, A138, 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 A114, A122, A124, A127, A128, A133, 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
A139: x in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) and
A140: 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;
A141: L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) c= L~ (Upper_Seq C,n) by A9, A10, JORDAN4:47;
A142: L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Lower_Seq C,n) by A106, JORDAN3:77;
A143: 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 A107, SPPOL_2:20;
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by JORDAN1F:5;
then A144: not W-min (L~ (Cage C,n)) in L~ (mid (Upper_Seq C,n),2,(len (Upper_Seq C,n))) by A126, JORDAN5B:16;

now

per cases ( x in LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) /. 1) or x in L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ) by A140, A143, XBOOLE_0:def 3;

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

then x in L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*> by A113, 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 A139, A141, XBOOLE_0:3; :: thesis: verum

end;

suppose A145: x in L~ (L_Cut (Lower_Seq C,n),((Gauge C,n) * i,j)) ; :: thesis: L~ (Upper_Seq C,n) meets L~ <*((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j)*>

then x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n)) by A139, A141, A142, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A146: x = E-max (L~ (Cage C,n)) by A139, A144, TARSKI:def 2;
1 in dom (Lower_Seq C,n) by A11, 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 A106, A145, A146, 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 A139, A141, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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

end;

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

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

end;

suppose A148: ( (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & (Gauge C,n) * i,j = (Lower_Seq C,n) . (len (Lower_Seq C,n)) ) ; :: thesis: LSeg ((Gauge C,n) * i,(width (Gauge C,n))),((Gauge C,n) * i,j) meets L~ (Upper_Seq C,n)

len (Lower_Seq C,n) in dom (Lower_Seq C,n) by A11, FINSEQ_3:27;
then A149: (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 ;
A150: rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A7, SPPOL_2:18, XXREAL_0:2;
A151: 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 A148, A149, A150, A151, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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