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

now

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

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

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

end;

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

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

proof

A24: (NE-corner (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
then ( (NE-corner (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) & (NE-corner (L~ (Cage C,n))) `2 >= S-bound (L~ (Cage C,n)) ) by EUCLID:56, 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 A24;
then A25: NE-corner (L~ (Cage C,n)) in LSeg (SE-corner (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n))) by SPRECT_1:25;
assume NE-corner (L~ (Cage C,n)) in rng (Cage C,n) ; :: thesis: contradiction
then NE-corner (L~ (Cage C,n)) in (LSeg (SE-corner (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A22, A25, XBOOLE_0:def 4;
then A26: (NE-corner (L~ (Cage C,n))) `2 <= (E-max (L~ (Cage C,n))) `2 by PSCOMP_1:108;
A27: (E-max (L~ (Cage C,n))) `1 = (NE-corner (L~ (Cage C,n))) `1 by PSCOMP_1:105;
(E-max (L~ (Cage C,n))) `2 <= (NE-corner (L~ (Cage C,n))) `2 by PSCOMP_1:107;
then (E-max (L~ (Cage C,n))) `2 = (NE-corner (L~ (Cage C,n))) `2 by A26, XXREAL_0:1;
hence contradiction by A21, A27, TOPREAL3:11; :: thesis: verum

end;

A28: now

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

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

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

then L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) = mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n)) by JORDAN3:def 4;
then A52: 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 A52, XBOOLE_1:1;
hence not NE-corner (L~ (Cage C,n)) in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A23; :: thesis: verum

end;

end;

end;

S-bound (L~ (Cage C,n)) < N-bound (L~ (Cage C,n)) by SPRECT_1:34;
then NE-corner (L~ (Cage C,n)) <> (Gauge C,n) * i,1 by A13, EUCLID:56;
then not NE-corner (L~ (Cage C,n)) in {((Gauge C,n) * i,1)} by TARSKI:def 1;
then not NE-corner (L~ (Cage C,n)) in rng <*((Gauge C,n) * i,1)*> by FINSEQ_1:56;
then not NE-corner (L~ (Cage C,n)) in (rng <*((Gauge C,n) * i,1)*>) \/ (rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by A28, XBOOLE_0:def 3;
then not NE-corner (L~ (Cage C,n)) in rng (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by FINSEQ_1: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 A53: rng (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) misses rng <*(NE-corner (L~ (Cage C,n)))*> by FINSEQ_1:55;
A54: len ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) = (len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_2:19
.= (1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))) + 1 by FINSEQ_5:8 ;
A55: not L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is empty by A21, JORDAN1E:7;
then A56: 0 + 1 <= len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then 1 in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
then A57: (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1 = (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) . 1 by PARTFUN1:def 8
.= (Gauge C,n) * i,j by A21, JORDAN3:58 ;
then A58: ((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1 = (Gauge C,n) * i,j by A56, BOOLMARK:8;
1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A56, XREAL_1:9;
then A59: 2 < len ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) by A54, NAT_1:13;
A60: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A21, JORDAN3:69;
(<*((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 A61: (((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1) `2 = S-bound (L~ (Cage C,n)) by A1, A2, JORDAN1A: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 A62: (((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. (len ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>))) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
A63: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (N-max (L~ (Cage C,n))) .. (Cage C,n) <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:74;
then A64: (E-max (L~ (Cage C,n))) .. (Cage C,n) > 1 by A63, SPRECT_2:73, XXREAL_0:2;
(E-min (L~ (Cage C,n))) .. (Cage C,n) <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by A63, SPRECT_2:76;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A63, 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 A63, SPRECT_2:77, XXREAL_0:2;
then A65: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A63, SPRECT_2:78, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A63, SPRECT_2:80, XXREAL_0:2;
then A66: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
A67: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by FINSEQ_5:41;
then A68: ((Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = E-bound (L~ (Cage C,n)) by A64, A66, JORDAN1E:24;
A69: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A70: (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = ((len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A67, A65, SPRECT_5:10;

now

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

end;

then A74: <*((Gauge C,n) * i,1)*> is_in_the_area_of Cage C,n by SPRECT_2:def 1;
A75: <*(NE-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:29;
3 <= len (Lower_Seq C,n) by JORDAN1E:19;
then 2 <= len (Lower_Seq C,n) by XXREAL_0:2;
then A76: 2 in dom (Lower_Seq C,n) by FINSEQ_3:27;
<*((Gauge C,n) * i,j)*> is_in_the_area_of Cage C,n by A21, 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 A21, JORDAN1E:21, SPRECT_3:73;
then <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is_in_the_area_of Cage C,n by A74, SPRECT_2:28;
then (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by A75, SPRECT_2:28;
then A77: (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*> is_a_v.c._for Cage C,n by A61, A62, SPRECT_2:def 3;
A78: ((1 + (((len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) - (len (Cage C,n)) = 1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) ;
A79: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by FINSEQ_5:6;
then mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is_in_the_area_of Cage C,n by A76, JORDAN1E:22, SPRECT_2:26;
then A80: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_in_the_area_of Cage C,n by SPRECT_3:68;
1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) <= 0 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A65, NAT_1:13;
then (1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) <= 0 by XREAL_1:22;
then A81: (len (Cage C,n)) + ((1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) <= (len (Cage C,n)) + 0 by XREAL_1:8;
A82: len (Lower_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A83: len (Lower_Seq C,n) > 2 by NAT_1:13;
(len (Cage C,n)) + 0 <= (len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1: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 A70, 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 A84: len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) <= 1 + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A69, FINSEQ_5:53;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A85: 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;
A86: L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Upper_Seq C,n) by A21, JORDAN3:77;
A87: <*(NE-corner (L~ (Cage C,n)))*> is special by SPPOL_2:39;
A88: len (Lower_Seq C,n) > 1 by A82, XXREAL_0:2;
then A89: not mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is empty by A83, JORDAN1B:3;
A90: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A67, FINSEQ_6:96, SPRECT_2:47;
then (Lower_Seq C,n) /. (1 + 1) = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (1 + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) by A5, A76, FINSEQ_5: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 A69, A70, A84, A81, REVROT_1:17
.= (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) by A70, A78, XREAL_0:def 2 ;
then ((mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) /. 1) `1 = E-bound (L~ (Cage C,n)) by A76, A79, A68, SPRECT_2: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 A89, FINSEQ_5:68;
then A91: ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. (len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))))) `1 = E-bound (L~ (Cage C,n)) by FINSEQ_5:def 3;
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A5, A90, FINSEQ_5:57
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A69, FINSEQ_6: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 A76, A79, SPRECT_2:13;
then ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A89, FINSEQ_5:68;
then A92: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_a_h.c._for Cage C,n by A80, A91, SPRECT_2:def 2;
A93: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by A9, FINSEQ_3:27;
A94: <*((Gauge C,n) * i,1)*> is special by SPPOL_2:39;
set ci = mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n));
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A8, SPPOL_2:18, XXREAL_0:2;
then A95: not (Gauge C,n) * i,1 in rng (Upper_Seq C,n) by A2, A21, Th52;
not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) by A2, A21, Th52;
then not (Gauge C,n) * i,1 in {((Gauge C,n) * i,j)} by A21, TARSKI:def 1;
then A96: not (Gauge C,n) * i,1 in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;

now

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

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

rng (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n))) c= rng (Upper_Seq C,n) by 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 A95;
then not (Gauge C,n) * i,1 in (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n)))) by A96, XBOOLE_0:def 3;
then not (Gauge C,n) * i,1 in rng (<*((Gauge C,n) * i,j)*> ^ (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n)))) by FINSEQ_1:44;
hence not (Gauge C,n) * i,1 in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A97, JORDAN3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

then {((Gauge C,n) * i,1)} misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A98: rng <*((Gauge C,n) * i,1)*> misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A99: <*(NE-corner (L~ (Cage C,n)))*> is one-to-one by FINSEQ_3:102;
(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 A100: not E-max (L~ (Cage C,n)) in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) by A83, JORDAN5B:16;
<*((Gauge C,n) * i,1)*> is one-to-one by FINSEQ_3:102;
then <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A98, A60, FINSEQ_3:98;
then A101: (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*> is one-to-one by A53, A99, FINSEQ_3:98;
A102: L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) c= L~ (Lower_Seq C,n) by A11, JORDAN4:47;
(<*((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, A3, A57, GOBOARD5:3 ;
then A103: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is special by A60, A94, GOBOARD2:13;
len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A56, FINSEQ_3:27;
then A104: (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) = (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) . (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by PARTFUN1:def 8
.= (Upper_Seq C,n) . (len (Upper_Seq C,n)) by A21, JORDAN1B:5
.= (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by A93, 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 A7, A85, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A85, FINSEQ_5:48 ;
then (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))) = E-max (L~ (Cage C,n)) by A55, SPRECT_3:11;
then ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))))) `1 = (NE-corner (L~ (Cage C,n))) `1 by PSCOMP_1:105
.= (<*(NE-corner (L~ (Cage C,n)))*> /. 1) `1 by FINSEQ_4:25 ;
then A105: (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*> is special by A103, A87, GOBOARD2:13;
mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is S-Sequence_in_R2 by A83, A88, JORDAN3:39;
then A106: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is S-Sequence_in_R2 by SPPOL_2:47;
then 2 <= len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) by TOPREAL1:def 10;
then L~ (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) meets L~ ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) by A59, A101, A105, A106, A92, A77, SPRECT_2: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
A107: x in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) and
A108: x in L~ ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) ^ <*(NE-corner (L~ (Cage C,n)))*>) by XBOOLE_0:3;
A109: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
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 A55, SPPOL_2:19 ;
then A110: ( x in LSeg ((Gauge C,n) * i,1),(((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1) or x in (L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) \/ (LSeg ((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))),(NE-corner (L~ (Cage C,n)))) ) by A108, XBOOLE_0:def 3;

now

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

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

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

end;

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

then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A107, A102, A86, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A112: x = W-min (L~ (Cage C,n)) by A107, A100, TARSKI:def 2;
1 in dom (Upper_Seq C,n) by A9, FINSEQ_3: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 A7, A85, FINSEQ_5:47
.= W-min (L~ (Cage C,n)) by A109, FINSEQ_6:98 ;
then x = (Gauge C,n) * i,j by A21, A111, A112, 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 A107, A102, XBOOLE_0:3; :: thesis: verum

end;

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

x in L~ (Cage C,n) by A6, A107, A102, XBOOLE_0:def 3;
then x in (LSeg (E-max (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A104, A113, XBOOLE_0:def 4;
then x in {(E-max (L~ (Cage C,n)))} by PSCOMP_1:112;
hence L~ (Lower_Seq C,n) meets L~ <*((Gauge C,n) * i,1),((Gauge C,n) * i,j)*> by A107, A100, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

end;

then A118: <*((Gauge C,n) * i,1)*> is_in_the_area_of Cage C,n by SPRECT_2:def 1;
<*((Gauge C,n) * i,j)*> is_in_the_area_of Cage C,n by A114, JORDAN1E: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 A114, JORDAN1E:21, SPRECT_3:73;
then A119: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is_in_the_area_of Cage C,n by A118, SPRECT_2:28;
A120: <*((Gauge C,n) * i,1)*> is special by SPPOL_2:39;
A121: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by A9, FINSEQ_3:27;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A122: 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;
A123: not L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is empty by A114, JORDAN1E:7;
then A124: 0 + 1 <= len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by NAT_1:13;
then 1 in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_3:27;
then A125: (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1 = (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) . 1 by PARTFUN1:def 8
.= (Gauge C,n) * i,j by A114, JORDAN3:58 ;
len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) in dom (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A124, FINSEQ_3:27;
then (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) = (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) . (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by PARTFUN1:def 8
.= (Upper_Seq C,n) . (len (Upper_Seq C,n)) by A114, JORDAN1B:5
.= (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by A121, 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 A7, A122, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A122, FINSEQ_5:48 ;
then (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)))) = E-max (L~ (Cage C,n)) by A123, SPRECT_3:11;
then A126: ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) /. (len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))))) `2 = N-bound (L~ (Cage C,n)) by A114, EUCLID:56;
(<*((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 ((<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) /. 1) `2 = S-bound (L~ (Cage C,n)) by A1, A2, JORDAN1A:93;
then A127: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is_a_v.c._for Cage C,n by A119, A126, SPRECT_2:def 3;
A128: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (N-max (L~ (Cage C,n))) .. (Cage C,n) <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:74;
then A129: (E-max (L~ (Cage C,n))) .. (Cage C,n) > 1 by A128, SPRECT_2:73, XXREAL_0:2;
(E-min (L~ (Cage C,n))) .. (Cage C,n) <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by A128, SPRECT_2:76;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A128, 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 A128, SPRECT_2:77, XXREAL_0:2;
then A130: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A128, SPRECT_2:78, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A128, SPRECT_2:80, XXREAL_0:2;
then A131: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
A132: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by FINSEQ_5:41;
then A133: ((Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = E-bound (L~ (Cage C,n)) by A129, A131, JORDAN1E:24;
1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) <= 0 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A130, NAT_1:13;
then (1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) <= 0 by XREAL_1:22;
then A134: (len (Cage C,n)) + ((1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) <= (len (Cage C,n)) + 0 by XREAL_1:8;
A135: len (Lower_Seq C,n) >= 2 + 1 by JORDAN1E:19;
then A136: len (Lower_Seq C,n) > 2 by NAT_1:13;
set ci = mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n));
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by A8, SPPOL_2:18, XXREAL_0:2;
then A137: not (Gauge C,n) * i,1 in rng (Upper_Seq C,n) by A2, A114, Th52;
not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) by A2, A114, Th52;
then not (Gauge C,n) * i,1 in {((Gauge C,n) * i,j)} by A114, TARSKI:def 1;
then A138: not (Gauge C,n) * i,1 in rng <*((Gauge C,n) * i,j)*> by FINSEQ_1:55;

now

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

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

rng (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n))) c= rng (Upper_Seq C,n) by 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 A137;
then not (Gauge C,n) * i,1 in (rng <*((Gauge C,n) * i,j)*>) \/ (rng (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n)))) by A138, XBOOLE_0:def 3;
then not (Gauge C,n) * i,1 in rng (<*((Gauge C,n) * i,j)*> ^ (mid (Upper_Seq C,n),((Index ((Gauge C,n) * i,j),(Upper_Seq C,n)) + 1),(len (Upper_Seq C,n)))) by FINSEQ_1:44;
hence not (Gauge C,n) * i,1 in rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by A139, JORDAN3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

then {((Gauge C,n) * i,1)} misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by ZFMISC_1:56;
then A140: rng <*((Gauge C,n) * i,1)*> misses rng (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) by FINSEQ_1:55;
A141: ((1 + (((len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) - (len (Cage C,n)) = 1 + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) ;
1 + (len (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 1 + 1 by A124, XREAL_1:9;
then A142: len (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) >= 2 by FINSEQ_5:8;
3 <= len (Lower_Seq C,n) by JORDAN1E:19;
then 2 <= len (Lower_Seq C,n) by XXREAL_0:2;
then A143: 2 in dom (Lower_Seq C,n) by FINSEQ_3:27;
(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 A144: not E-max (L~ (Cage C,n)) in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) by A136, JORDAN5B:16;
A145: L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j) is being_S-Seq by A114, JORDAN3:69;
(<*((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, A3, A125, GOBOARD5:3 ;
then A146: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is special by A145, A120, GOBOARD2:13;
A147: L~ (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) = (LSeg ((Gauge C,n) * i,1),((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1)) \/ (L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by A123, SPPOL_2:20;
A148: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A149: (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = ((len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A132, A130, SPRECT_5: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 A149, 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 A150: len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) <= 1 + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A148, FINSEQ_5:53;
A151: len (Lower_Seq C,n) > 1 by A135, XXREAL_0:2;
then A152: not mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is empty by A136, JORDAN1B:3;
A153: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by FINSEQ_5:6;
then mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is_in_the_area_of Cage C,n by A143, JORDAN1E:22, SPRECT_2:26;
then A154: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_in_the_area_of Cage C,n by SPRECT_3:68;
A155: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A132, FINSEQ_6:96, SPRECT_2:47;
then (Lower_Seq C,n) /. (1 + 1) = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (1 + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) by A5, A143, FINSEQ_5: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 A148, A149, A150, A134, REVROT_1:17
.= (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) by A149, A141, XREAL_0:def 2 ;
then ((mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) /. 1) `1 = E-bound (L~ (Cage C,n)) by A143, A153, A133, SPRECT_2: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 A152, FINSEQ_5:68;
then A156: ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. (len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))))) `1 = E-bound (L~ (Cage C,n)) by FINSEQ_5:def 3;
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A5, A155, FINSEQ_5:57
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A148, FINSEQ_6: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 A143, A153, SPRECT_2:13;
then ((Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) /. 1) `1 = W-bound (L~ (Cage C,n)) by A152, FINSEQ_5:68;
then A157: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is_a_h.c._for Cage C,n by A154, A156, SPRECT_2:def 2;
<*((Gauge C,n) * i,1)*> is one-to-one by FINSEQ_3:102;
then A158: <*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) is one-to-one by A140, A145, FINSEQ_3:98;
A159: L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) c= L~ (Lower_Seq C,n) by A11, JORDAN4:47;
mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)) is S-Sequence_in_R2 by A136, A151, JORDAN3:39;
then A160: Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) is S-Sequence_in_R2 by SPPOL_2:47;
then 2 <= len (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) by TOPREAL1:def 10;
then L~ (Rev (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n)))) meets L~ (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by A142, A158, A146, A160, A157, A127, SPRECT_2: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
A161: x in L~ (mid (Lower_Seq C,n),2,(len (Lower_Seq C,n))) and
A162: x in L~ (<*((Gauge C,n) * i,1)*> ^ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j))) by XBOOLE_0:3;
A163: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A164: L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) c= L~ (Upper_Seq C,n) by A114, JORDAN3:77;

now

per cases ( x in LSeg ((Gauge C,n) * i,1),((L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) /. 1) or x in L~ (L_Cut (Upper_Seq C,n),((Gauge C,n) * i,j)) ) by A162, A147, XBOOLE_0:def 3;

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

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

end;

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

then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A161, A159, A164, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A166: x = W-min (L~ (Cage C,n)) by A161, A144, TARSKI:def 2;
1 in dom (Upper_Seq C,n) by A9, FINSEQ_3: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 A7, A122, FINSEQ_5:47
.= W-min (L~ (Cage C,n)) by A163, FINSEQ_6:98 ;
then x = (Gauge C,n) * i,j by A114, A165, A166, 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 A161, A159, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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

end;

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

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

end;

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

A169: (Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) by RLTOPSP1:69;
A170: ( rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) & E-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) ) by A5, A10, FINSEQ_6:66, SPPOL_2:18, XXREAL_0:2;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A171: 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;
len (Upper_Seq C,n) in dom (Upper_Seq C,n) by A9, FINSEQ_3:27;
then (Upper_Seq C,n) . (len (Upper_Seq C,n)) = (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by 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 A7, A171, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A171, FINSEQ_5:48 ;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n) by A168, A170, A169, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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