let n be Element of NAT ; :: thesis:
let C be Simple_closed_curve; :: thesis:
let i, j, k be Element of NAT ; :: thesis:
set Ga = Gauge C,n;
set US = Upper_Seq C,n;
set LS = Lower_Seq C,n;
set LA = Lower_Arc C;
set Wmin = W-min (L~ (Cage C,n));
set Emax = E-max (L~ (Cage C,n));
set Wbo = W-bound (L~ (Cage C,n));
set Ebo = E-bound (L~ (Cage C,n));
set Gij = (Gauge C,n) * j,i;
set Gik = (Gauge C,n) * k,i;
assume that
A1: ( 1 < j & j <= k & k < len (Gauge C,n) ) and
A2: ( 1 <= i & i <= width (Gauge C,n) ) and
A3: (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k,i)} and
A4: (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j,i)} and
A5: LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) misses Lower_Arc C ; :: thesis:
(Gauge C,n) * j,i in {((Gauge C,n) * j,i)} by TARSKI:def 1;
then A6: (Gauge C,n) * j,i in L~ (Lower_Seq C,n) by A4, XBOOLE_0:def 4;
(Gauge C,n) * k,i in {((Gauge C,n) * k,i)} by TARSKI:def 1;
then A7: (Gauge C,n) * k,i in L~ (Upper_Seq C,n) by A3, XBOOLE_0:def 4;
A8: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A9: j <> k by A1, A2, A6, A7, Th29;
A10: ( 1 <= j & j <= width (Gauge C,n) ) by A1, A8, XXREAL_0:2;
A11: ( 1 <= k & k <= width (Gauge C,n) ) by A1, JORDAN8:def 1, XXREAL_0:2;
A12: [j,i] in Indices (Gauge C,n) by A2, A8, A10, MATRIX_1:37;
A13: [k,i] in Indices (Gauge C,n) by A2, A8, A11, MATRIX_1:37;
set go = R_Cut (Upper_Seq C,n),((Gauge C,n) * k,i);
set do = L_Cut (Lower_Seq C,n),((Gauge C,n) * j,i);
A14: len (Upper_Seq C,n) >= 3 by JORDAN1E:19;
then len (Upper_Seq C,n) >= 1 by XXREAL_0:2;
then 1 in dom (Upper_Seq C,n) by FINSEQ_3:27;
then A15: (Upper_Seq C,n) . 1 = (Upper_Seq C,n) /. 1 by PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:5 ;
A16: (W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * 1,k) `1 by A8, A11, JORDAN1A:94 ;
len (Gauge C,n) >= 4 by JORDAN8:13;
then A17: len (Gauge C,n) >= 1 by XXREAL_0:2;
then A18: [1,k] in Indices (Gauge C,n) by A11, MATRIX_1:37;
then A19: (Gauge C,n) * k,i <> (Upper_Seq C,n) . 1 by A1, A13, A15, A16, JORDAN1G:7;
then reconsider go = R_Cut (Upper_Seq C,n),((Gauge C,n) * k,i) as being_S-Seq FinSequence of (TOP-REAL 2) by A7, JORDAN3:70;
A20: [1,j] in Indices (Gauge C,n) by A10, A17, MATRIX_1:37;
A21: len (Lower_Seq C,n) >= 1 + 2 by JORDAN1E:19;
then len (Lower_Seq C,n) >= 1 by XXREAL_0:2;
then A22: ( 1 in dom (Lower_Seq C,n) & len (Lower_Seq C,n) in dom (Lower_Seq C,n) ) by FINSEQ_3:27;
then A23: (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 ;
A24: (W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * 1,k) `1 by A8, A11, JORDAN1A:94 ;
A25: [j,i] in Indices (Gauge C,n) by A2, A8, A10, MATRIX_1:37;
then A26: (Gauge C,n) * j,i <> (Lower_Seq C,n) . (len (Lower_Seq C,n)) by A1, A18, A23, A24, JORDAN1G:7;
then reconsider do = L_Cut (Lower_Seq C,n),((Gauge C,n) * j,i) as being_S-Seq FinSequence of (TOP-REAL 2) by A6, JORDAN3:69;
A27: [(len (Gauge C,n)),k] in Indices (Gauge C,n) by A11, A17, MATRIX_1:37;
A28: (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by A22, PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
(E-max (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * (len (Gauge C,n)),k) `1 by A8, A11, JORDAN1A:92 ;
then A29: (Gauge C,n) * j,i <> (Lower_Seq C,n) . 1 by A1, A25, A27, A28, JORDAN1G:7;
A30: len go >= 1 + 1 by TOPREAL1:def 10;
A31: (Gauge C,n) * k,i in rng (Upper_Seq C,n) by A2, A7, A8, A11, JORDAN1G:4, JORDAN1J:40;
then A32: go is_sequence_on Gauge C,n by JORDAN1G:4, JORDAN1J:38;
A33: len do >= 1 + 1 by TOPREAL1:def 10;
A34: (Gauge C,n) * j,i in rng (Lower_Seq C,n) by A2, A6, A8, A10, JORDAN1G:5, JORDAN1J:40;
then A35: do is_sequence_on Gauge C,n by JORDAN1G:5, JORDAN1J:39;
reconsider go = go as non constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A30, A32, JGRAPH_1:16, JORDAN8:8;
reconsider do = do as non constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A33, A35, JGRAPH_1:16, JORDAN8:8;
A36: len go > 1 by A30, NAT_1:13;
then A37: len go in dom go by FINSEQ_3:27;
then A38: go /. (len go) = go . (len go) by PARTFUN1:def 8
.= (Gauge C,n) * k,i by A7, JORDAN3:59 ;
len do >= 1 by A33, XXREAL_0:2;
then 1 in dom do by FINSEQ_3:27;
then A39: do /. 1 = do . 1 by PARTFUN1:def 8
.= (Gauge C,n) * j,i by A6, JORDAN3:58 ;
reconsider m = (len go) - 1 as Element of NAT by A37, FINSEQ_3:28;
A40: m + 1 = len go ;
then A41: (len go) -' 1 = m by NAT_D:34;
A42: LSeg go,m c= L~ go by TOPREAL3:26;
A43: L~ go c= L~ (Upper_Seq C,n) by A7, JORDAN3:76;
then LSeg go,m c= L~ (Upper_Seq C,n) by A42, XBOOLE_1:1;
then A44: (LSeg go,m) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) c= {((Gauge C,n) * k,i)} by A3, XBOOLE_1:26;
m >= 1 by A30, XREAL_1:21;
then A45: LSeg go,m = LSeg (go /. m),((Gauge C,n) * k,i) by A38, A40, TOPREAL1:def 5;
{((Gauge C,n) * k,i)} c= (LSeg go,m) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,n) * k,i)} ; :: thesis:
then A46: x = (Gauge C,n) * k,i by TARSKI:def 1;
A47: (Gauge C,n) * k,i in LSeg go,m by A45, RLTOPSP1:69;
(Gauge C,n) * k,i in LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) by RLTOPSP1:69;
hence x in (LSeg go,m) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) by A46, A47, XBOOLE_0:def 4; :: thesis:

end;

then A48: (LSeg go,m) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) = {((Gauge C,n) * k,i)} by A44, XBOOLE_0:def 10;
A49: LSeg do,1 c= L~ do by TOPREAL3:26;
A50: L~ do c= L~ (Lower_Seq C,n) by A6, JORDAN3:77;
then LSeg do,1 c= L~ (Lower_Seq C,n) by A49, XBOOLE_1:1;
then A51: (LSeg do,1) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) c= {((Gauge C,n) * j,i)} by A4, XBOOLE_1:26;
A52: LSeg do,1 = LSeg ((Gauge C,n) * j,i),(do /. (1 + 1)) by A33, A39, TOPREAL1:def 5;
{((Gauge C,n) * j,i)} c= (LSeg do,1) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,n) * j,i)} ; :: thesis:
then A53: x = (Gauge C,n) * j,i by TARSKI:def 1;
A54: (Gauge C,n) * j,i in LSeg do,1 by A52, RLTOPSP1:69;
(Gauge C,n) * j,i in LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) by RLTOPSP1:69;
hence x in (LSeg do,1) /\ (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) by A53, A54, XBOOLE_0:def 4; :: thesis:

end;

then A55: (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) /\ (LSeg do,1) = {((Gauge C,n) * j,i)} by A51, XBOOLE_0:def 10;
A56: go /. 1 = (Upper_Seq C,n) /. 1 by A7, SPRECT_3:39
.= W-min (L~ (Cage C,n)) by JORDAN1F:5 ;
then A57: go /. 1 = (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by JORDAN1F:8
.= do /. (len do) by A6, JORDAN1J:35 ;
A58: ( rng go c= L~ go & rng do c= L~ do ) by A30, A33, SPPOL_2:18;
A59: {(go /. 1)} c= (L~ go) /\ (L~ do)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(go /. 1)} ; :: thesis:
then x = go /. 1 by TARSKI:def 1;
then ( x in rng go & x in rng do ) by A57, FINSEQ_6:46, REVROT_1:3;
hence x in (L~ go) /\ (L~ do) by A58, XBOOLE_0:def 4; :: thesis:

end;

A60: (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by A22, PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
A61: [(len (Gauge C,n)),j] in Indices (Gauge C,n) by A10, A17, MATRIX_1:37;
(L~ go) /\ (L~ do) c= {(go /. 1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (L~ go) /\ (L~ do) ; :: thesis:
then A62: ( x in L~ go & x in L~ do ) by XBOOLE_0:def 4;
then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A43, A50, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
then A63: ( x = W-min (L~ (Cage C,n)) or x = E-max (L~ (Cage C,n)) ) by TARSKI:def 2;

now

assume x = E-max (L~ (Cage C,n)) ; :: thesis:
then A64: E-max (L~ (Cage C,n)) = (Gauge C,n) * j,i by A6, A60, A62, JORDAN1E:11;
((Gauge C,n) * (len (Gauge C,n)),j) `1 = E-bound (L~ (Cage C,n)) by A8, A10, JORDAN1A:92;
then (E-max (L~ (Cage C,n))) `1 <> E-bound (L~ (Cage C,n)) by A1, A12, A61, A64, JORDAN1G:7;
hence contradiction by EUCLID:56; :: thesis:

end;

hence x in {(go /. 1)} by A56, A63, TARSKI:def 1; :: thesis:

end;

then A65: (L~ go) /\ (L~ do) = {(go /. 1)} by A59, XBOOLE_0:def 10;
set W2 = go /. 2;
A66: 2 in dom go by A30, FINSEQ_3:27;
A67: ((Gauge C,n) * k,i) .. (Upper_Seq C,n) >= 1 by A31, FINSEQ_4:31;

A68: now

assume ((Gauge C,n) * j,i) `1 = W-bound (L~ (Cage C,n)) ; :: thesis:
then ((Gauge C,n) * 1,j) `1 = ((Gauge C,n) * j,i) `1 by A8, A10, JORDAN1A:94;
hence contradiction by A1, A12, A20, JORDAN1G:7; :: thesis:

end;

go = mid (Upper_Seq C,n),1,(((Gauge C,n) * k,i) .. (Upper_Seq C,n)) by A31, JORDAN1G:57
.= (Upper_Seq C,n) | (((Gauge C,n) * k,i) .. (Upper_Seq C,n)) by A67, JORDAN3:25 ;
then A69: go /. 2 = (Upper_Seq C,n) /. 2 by A66, FINSEQ_4:85;
A70: W-min (L~ (Cage C,n)) in rng go by A56, FINSEQ_6:46;
set pion = <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*>;

A71: now

let n be Element of NAT ; :: thesis:
assume n in dom <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> ; :: thesis:
then n in {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then ( n = 1 or n = 2 ) by TARSKI:def 2;
then ( <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. n = (Gauge C,n) * k,i or <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. n = (Gauge C,n) * j,i ) by FINSEQ_4:26;
hence ex j, i being Element of NAT st
( [j,i] in Indices (Gauge C,n) & <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. n = (Gauge C,n) * j,i ) by A12, A13; :: thesis:

end;

A72: (Gauge C,n) * k,i <> (Gauge C,n) * j,i by A9, A12, A13, GOBOARD1:21;
((Gauge C,n) * k,i) `2 = ((Gauge C,n) * 1,i) `2 by A2, A8, A11, GOBOARD5:2
.= ((Gauge C,n) * j,i) `2 by A2, A8, A10, GOBOARD5:2 ;
then LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) is horizontal by SPPOL_1:36;
then <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> is being_S-Seq by A72, JORDAN1B:9;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A73: pion1 is_sequence_on Gauge C,n and
A74: pion1 is being_S-Seq and
A75: L~ <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> = L~ pion1 and
A76: <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. 1 = pion1 /. 1 and
A77: <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. (len <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*>) = pion1 /. (len pion1) and
A78: len <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> <= len pion1 by A71, GOBOARD3:2;
reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A74;
set godo = (go ^' pion1) ^' do;
A79: 1 + 1 <= len (Cage C,n) by GOBOARD7:36, XXREAL_0:2;
then A80: 1 + 1 <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by REVROT_1:14;
len (go ^' pion1) >= len go by TOPREAL8:7;
then A81: len (go ^' pion1) >= 1 + 1 by A30, XXREAL_0:2;
then A82: len (go ^' pion1) > 1 + 0 by NAT_1:13;
A83: len ((go ^' pion1) ^' do) >= len (go ^' pion1) by TOPREAL8:7;
then A84: 1 + 1 <= len ((go ^' pion1) ^' do) by A81, XXREAL_0:2;
A85: Upper_Seq C,n is_sequence_on Gauge C,n by JORDAN1G:4;
A86: go /. (len go) = pion1 /. 1 by A38, A76, FINSEQ_4:26;
then A87: go ^' pion1 is_sequence_on Gauge C,n by A32, A73, TOPREAL8:12;
A88: (go ^' pion1) /. (len (go ^' pion1)) = <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. (len <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*>) by A77, GRAPH_2:58
.= <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. 2 by FINSEQ_1:61
.= do /. 1 by A39, FINSEQ_4:26 ;
then A89: (go ^' pion1) ^' do is_sequence_on Gauge C,n by A35, A87, TOPREAL8:12;
LSeg pion1,1 c= L~ <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> by A75, TOPREAL3:26;
then LSeg pion1,1 c= LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) by SPPOL_2:21;
then A90: (LSeg go,((len go) -' 1)) /\ (LSeg pion1,1) c= {((Gauge C,n) * k,i)} by A41, A48, XBOOLE_1:27;
A91: len pion1 >= 1 + 1 by A78, FINSEQ_1:61;
{((Gauge C,n) * k,i)} c= (LSeg go,m) /\ (LSeg pion1,1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,n) * k,i)} ; :: thesis:
then A92: x = (Gauge C,n) * k,i by TARSKI:def 1;
A93: (Gauge C,n) * k,i in LSeg go,m by A45, RLTOPSP1:69;
(Gauge C,n) * k,i in LSeg pion1,1 by A38, A86, A91, TOPREAL1:27;
hence x in (LSeg go,m) /\ (LSeg pion1,1) by A92, A93, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg go,((len go) -' 1)) /\ (LSeg pion1,1) = {(go /. (len go))} by A38, A41, A90, XBOOLE_0:def 10;
then A94: go ^' pion1 is unfolded by A86, TOPREAL8:34;
len pion1 >= 2 + 0 by A78, FINSEQ_1:61;
then A95: (len pion1) - 2 >= 0 by XREAL_1:21;
((len (go ^' pion1)) + 1) - 1 = ((len go) + (len pion1)) - 1 by GRAPH_2:13;
then (len (go ^' pion1)) - 1 = (len go) + ((len pion1) - 2)
.= (len go) + ((len pion1) -' 2) by A95, XREAL_0:def 2 ;
then A96: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;
A97: (len pion1) - 1 >= 1 by A91, XREAL_1:21;
then A98: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;
A99: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A95, XREAL_0:def 2
.= (len pion1) -' 1 by A97, XREAL_0:def 2 ;
((len pion1) - 1) + 1 <= len pion1 ;
then A100: (len pion1) -' 1 < len pion1 by A98, NAT_1:13;
LSeg pion1,((len pion1) -' 1) c= L~ <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> by A75, TOPREAL3:26;
then LSeg pion1,((len pion1) -' 1) c= LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) by SPPOL_2:21;
then A101: (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) c= {((Gauge C,n) * j,i)} by A55, XBOOLE_1:27;
{((Gauge C,n) * j,i)} c= (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,n) * j,i)} ; :: thesis:
then A102: x = (Gauge C,n) * j,i by TARSKI:def 1;
A103: (Gauge C,n) * j,i in LSeg do,1 by A52, RLTOPSP1:69;
pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. 2 by A77, A98, FINSEQ_1:61
.= (Gauge C,n) * j,i by FINSEQ_4:26 ;
then (Gauge C,n) * j,i in LSeg pion1,((len pion1) -' 1) by A97, A98, TOPREAL1:27;
hence x in (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) by A102, A103, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) = {((Gauge C,n) * j,i)} by A101, XBOOLE_0:def 10;
then A104: (LSeg (go ^' pion1),((len go) + ((len pion1) -' 2))) /\ (LSeg do,1) = {((go ^' pion1) /. (len (go ^' pion1)))} by A39, A86, A88, A99, A100, TOPREAL8:31;
A105: not go ^' pion1 is trivial by A81, REALSET1:13;
A106: rng pion1 c= L~ pion1 by A91, SPPOL_2:18;
A107: {(pion1 /. 1)} c= (L~ go) /\ (L~ pion1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(pion1 /. 1)} ; :: thesis:
then x = pion1 /. 1 by TARSKI:def 1;
then ( x in rng go & x in rng pion1 ) by A86, FINSEQ_6:46, REVROT_1:3;
hence x in (L~ go) /\ (L~ pion1) by A58, A106, XBOOLE_0:def 4; :: thesis:

end;

(L~ go) /\ (L~ pion1) c= {(pion1 /. 1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (L~ go) /\ (L~ pion1) ; :: thesis:
then ( x in L~ go & x in L~ pion1 ) by XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Upper_Seq C,n)) by A43, XBOOLE_0:def 4;
hence x in {(pion1 /. 1)} by A3, A38, A75, A86, SPPOL_2:21; :: thesis:

end;

then A108: (L~ go) /\ (L~ pion1) = {(pion1 /. 1)} by A107, XBOOLE_0:def 10;
then A109: go ^' pion1 is s.n.c. by A86, JORDAN1J:54;
(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A58, A106, A108, XBOOLE_1:27;
then A110: go ^' pion1 is one-to-one by JORDAN1J:55;
A111: <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. (len <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*>) = <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> /. 2 by FINSEQ_1:61
.= do /. 1 by A39, FINSEQ_4:26 ;
A112: {(pion1 /. (len pion1))} c= (L~ do) /\ (L~ pion1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(pion1 /. (len pion1))} ; :: thesis:
then x = pion1 /. (len pion1) by TARSKI:def 1;
then ( x in rng do & x in rng pion1 ) by A77, A111, FINSEQ_6:46, REVROT_1:3;
hence x in (L~ do) /\ (L~ pion1) by A58, A106, XBOOLE_0:def 4; :: thesis:

end;

(L~ do) /\ (L~ pion1) c= {(pion1 /. (len pion1))}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (L~ do) /\ (L~ pion1) ; :: thesis:
then ( x in L~ do & x in L~ pion1 ) by XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Lower_Seq C,n)) by A50, XBOOLE_0:def 4;
hence x in {(pion1 /. (len pion1))} by A4, A39, A75, A77, A111, SPPOL_2:21; :: thesis:

end;

then A113: (L~ do) /\ (L~ pion1) = {(pion1 /. (len pion1))} by A112, XBOOLE_0:def 10;
A114: (L~ (go ^' pion1)) /\ (L~ do) = ((L~ go) \/ (L~ pion1)) /\ (L~ do) by A86, TOPREAL8:35
.= {(go /. 1)} \/ {(do /. 1)} by A65, A77, A111, A113, XBOOLE_1:23
.= {((go ^' pion1) /. 1)} \/ {(do /. 1)} by GRAPH_2:57
.= {((go ^' pion1) /. 1),(do /. 1)} by ENUMSET1:41 ;
do /. (len do) = (go ^' pion1) /. 1 by A57, GRAPH_2:57;
then reconsider godo = (go ^' pion1) ^' do as non constant standard special_circular_sequence by A84, A88, A89, A94, A96, A104, A105, A109, A110, A114, JORDAN8:7, JORDAN8:8, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;
A115: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def 9;
then A116: Lower_Arc C is connected by JORDAN6:11;
A117: ( W-min C in Lower_Arc C & E-max C in Lower_Arc C ) by A115, TOPREAL1:4;
set ff = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A118: (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_6:98;
A119: L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = L~ (Cage C,n) by REVROT_1:33;
then (W-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A118, SPRECT_5:23;
then (N-min (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A118, A119, SPRECT_5:24, XXREAL_0:2;
then (N-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A118, A119, SPRECT_5:25, XXREAL_0:2;
then A120: (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A118, A119, SPRECT_5:26, XXREAL_0:2;

A121: now

assume A122: ((Gauge C,n) * k,i) .. (Upper_Seq C,n) <= 1 ; :: thesis:
((Gauge C,n) * k,i) .. (Upper_Seq C,n) >= 1 by A31, FINSEQ_4:31;
then ((Gauge C,n) * k,i) .. (Upper_Seq C,n) = 1 by A122, XXREAL_0:1;
then (Gauge C,n) * k,i = (Upper_Seq C,n) /. 1 by A31, FINSEQ_5:41;
hence contradiction by A15, A19, JORDAN1F:5; :: thesis:

end;

A123: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then A124: Rotate (Cage C,n),(W-min (L~ (Cage C,n))) is_sequence_on Gauge C,n by REVROT_1:34;
A125: (right_cell godo,1,(Gauge C,n)) \ (L~ godo) c= RightComp godo by A84, A89, JORDAN9:29;
A126: L~ godo = (L~ (go ^' pion1)) \/ (L~ do) by A88, TOPREAL8:35
.= ((L~ go) \/ (L~ pion1)) \/ (L~ do) by A86, TOPREAL8:35 ;
L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by JORDAN1E:17;
then A127: ( L~ (Upper_Seq C,n) c= L~ (Cage C,n) & L~ (Lower_Seq C,n) c= L~ (Cage C,n) ) by XBOOLE_1:7;
then A128: ( L~ go c= L~ (Cage C,n) & L~ do c= L~ (Cage C,n) ) by A43, A50, XBOOLE_1:1;
A129: W-min C in C by SPRECT_1:15;
A130: L~ <*((Gauge C,n) * k,i),((Gauge C,n) * j,i)*> = LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i) by SPPOL_2:21;

A131: now

assume W-min C in L~ godo ; :: thesis:
then A132: ( W-min C in (L~ go) \/ (L~ pion1) or W-min C in L~ do ) by A126, XBOOLE_0:def 3;

per cases by A132, XBOOLE_0:def 3;

suppose W-min C in L~ go ; :: thesis:

then C meets L~ (Cage C,n) by A128, A129, XBOOLE_0:3;
hence contradiction by JORDAN10:5; :: thesis:

end;

suppose W-min C in L~ pion1 ; :: thesis:

hence contradiction by A5, A75, A117, A130, XBOOLE_0:3; :: thesis:

end;

suppose W-min C in L~ do ; :: thesis:

then C meets L~ (Cage C,n) by A128, A129, XBOOLE_0:3;
hence contradiction by JORDAN10:5; :: thesis:

end;

right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1 = right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1,(GoB (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A80, JORDAN1H:29
.= right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1,(GoB (Cage C,n)) by REVROT_1:28
.= right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1,(Gauge C,n) by JORDAN1H:52
.= right_cell ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))),1,(Gauge C,n) by A120, A124, JORDAN1J:53
.= right_cell (Upper_Seq C,n),1,(Gauge C,n) by JORDAN1E:def 1
.= right_cell (R_Cut (Upper_Seq C,n),((Gauge C,n) * k,i)),1,(Gauge C,n) by A31, A85, A121, JORDAN1J:52
.= right_cell (go ^' pion1),1,(Gauge C,n) by A36, A87, JORDAN1J:51
.= right_cell godo,1,(Gauge C,n) by A82, A89, JORDAN1J:51 ;
then W-min C in right_cell godo,1,(Gauge C,n) by JORDAN1I:8;
then A133: W-min C in (right_cell godo,1,(Gauge C,n)) \ (L~ godo) by A131, XBOOLE_0:def 5;
A134: godo /. 1 = (go ^' pion1) /. 1 by GRAPH_2:57
.= W-min (L~ (Cage C,n)) by A56, GRAPH_2:57 ;
A135: len (Upper_Seq C,n) >= 2 by A14, XXREAL_0:2;
A136: godo /. 2 = (go ^' pion1) /. 2 by A81, GRAPH_2:61
.= (Upper_Seq C,n) /. 2 by A30, A69, GRAPH_2:61
.= ((Upper_Seq C,n) ^' (Lower_Seq C,n)) /. 2 by A135, GRAPH_2:61
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 2 by JORDAN1E:15 ;
A137: (L~ go) \/ (L~ do) is compact by COMPTS_1:19;
W-min (L~ (Cage C,n)) in (L~ go) \/ (L~ do) by A58, A70, XBOOLE_0:def 3;
then A138: W-min ((L~ go) \/ (L~ do)) = W-min (L~ (Cage C,n)) by A128, A137, JORDAN1J:21, XBOOLE_1:8;
A139: ( (W-min ((L~ go) \/ (L~ do))) `1 = W-bound ((L~ go) \/ (L~ do)) & (W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) ) by EUCLID:56;
A140: ((Gauge C,n) * j,i) `1 <= ((Gauge C,n) * k,i) `1 by A1, A2, SPRECT_3:25;
then W-bound (LSeg ((Gauge C,n) * k,i),((Gauge C,n) * j,i)) = ((Gauge C,n) * j,i) `1 by SPRECT_1:62;
then A141: W-bound (L~ pion1) = ((Gauge C,n) * j,i) `1 by A75, SPPOL_2:21;
((Gauge C,n) * j,i) `1 >= W-bound (L~ (Cage C,n)) by A6, A127, PSCOMP_1:71;
then ((Gauge C,n) * j,i) `1 > W-bound (L~ (Cage C,n)) by A68, XXREAL_0:1;
then W-min (((L~ go) \/ (L~ do)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ do)) by A137, A138, A139, A141, JORDAN1J:33;
then A142: W-min (L~ godo) = W-min (L~ (Cage C,n)) by A126, A138, XBOOLE_1:4;
A143: rng godo c= L~ godo by A81, A83, SPPOL_2:18, XXREAL_0:2;
2 in dom godo by A84, FINSEQ_3:27;
then A144: godo /. 2 in rng godo by PARTFUN2:4;
godo /. 2 in W-most (L~ (Cage C,n)) by A136, JORDAN1I:27;
then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A142, PSCOMP_1:88
.= W-bound (L~ godo) by EUCLID:56 ;
then godo /. 2 in W-most (L~ godo) by A143, A144, SPRECT_2:16;
then (Rotate godo,(W-min (L~ godo))) /. 2 in W-most (L~ godo) by A134, A142, FINSEQ_6:95;
then reconsider godo = godo as non constant standard clockwise_oriented special_circular_sequence by JORDAN1I:27;
len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A145: (Upper_Seq C,n) . (len (Upper_Seq C,n)) = (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:7 ;
A146: E-max C in E-most C by PSCOMP_1:111;
A147: east_halfline (E-max C) misses L~ go

proof

assume east_halfline (E-max C) meets L~ go ; :: thesis:
then consider p being set such that
A148: p in east_halfline (E-max C) and
A149: p in L~ go by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A148;
p in L~ (Upper_Seq C,n) by A43, A149;
then p in (east_halfline (E-max C)) /\ (L~ (Cage C,n)) by A127, A148, XBOOLE_0:def 4;
then A150: p `1 = E-bound (L~ (Cage C,n)) by A146, JORDAN1A:104;
then A151: p = E-max (L~ (Cage C,n)) by A43, A149, JORDAN1J:46;
then E-max (L~ (Cage C,n)) = (Gauge C,n) * k,i by A7, A145, A149, JORDAN1J:43;
then ((Gauge C,n) * k,i) `1 = ((Gauge C,n) * (len (Gauge C,n)),k) `1 by A8, A11, A150, A151, JORDAN1A:92;
hence contradiction by A1, A13, A27, JORDAN1G:7; :: thesis:

end;

now

assume east_halfline (E-max C) meets L~ godo ; :: thesis:
then A152: ( east_halfline (E-max C) meets (L~ go) \/ (L~ pion1) or east_halfline (E-max C) meets L~ do ) by A126, XBOOLE_1:70;

per cases by A152, XBOOLE_1:70;

suppose east_halfline (E-max C) meets L~ go ; :: thesis:

hence contradiction by A147; :: thesis:

end;

suppose east_halfline (E-max C) meets L~ pion1 ; :: thesis:

then consider p being set such that
A153: p in east_halfline (E-max C) and
A154: p in L~ pion1 by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A153;
A155: p `1 <= ((Gauge C,n) * k,i) `1 by A75, A130, A140, A154, TOPREAL1:9;
k + 1 <= len (Gauge C,n) by A1, NAT_1:13;
then (k + 1) - 1 <= (len (Gauge C,n)) - 1 by XREAL_1:11;
then A156: k <= (len (Gauge C,n)) -' 1 by XREAL_0:def 2;
(len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:35;
then ((Gauge C,n) * k,i) `1 <= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),1) `1 by A2, A8, A11, A17, A156, JORDAN1A:39;
then p `1 <= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),1) `1 by A155, XXREAL_0:2;
then p `1 <= E-bound C by A17, JORDAN8:15;
then A157: p `1 <= (E-max C) `1 by EUCLID:56;
p `1 >= (E-max C) `1 by A153, TOPREAL1:def 13;
then A158: p `1 = (E-max C) `1 by A157, XXREAL_0:1;
p `2 = (E-max C) `2 by A153, TOPREAL1:def 13;
then p = E-max C by A158, TOPREAL3:11;
hence contradiction by A5, A75, A117, A130, A154, XBOOLE_0:3; :: thesis:

end;

suppose east_halfline (E-max C) meets L~ do ; :: thesis:

then consider p being set such that
A159: p in east_halfline (E-max C) and
A160: p in L~ do by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A159;
p in L~ (Lower_Seq C,n) by A50, A160;
then p in (east_halfline (E-max C)) /\ (L~ (Cage C,n)) by A127, A159, XBOOLE_0:def 4;
then A161: p `1 = E-bound (L~ (Cage C,n)) by A146, JORDAN1A:104;
A162: (E-max C) `2 = p `2 by A159, TOPREAL1:def 13;
set RC = Rotate (Cage C,n),(E-max (L~ (Cage C,n)));
A163: E-max C in right_cell (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))),1 by JORDAN1I:9;
A164: 1 + 1 <= len (Lower_Seq C,n) by A21, XXREAL_0:2;
Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n))) by JORDAN1G:26;
then A165: LSeg (Lower_Seq C,n),1 = LSeg (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))),1 by A164, SPPOL_2:9;
A166: L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = L~ (Cage C,n) by REVROT_1:33;
A167: len (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = len (Cage C,n) by REVROT_1:14;
A168: GoB (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = GoB (Cage C,n) by REVROT_1:28
.= Gauge C,n by JORDAN1H:52 ;
A169: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
A170: Rotate (Cage C,n),(E-max (L~ (Cage C,n))) is_sequence_on Gauge C,n by A123, REVROT_1:34;
A171: (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) by A166, A169, FINSEQ_6:98;
then consider ii, jj being Element of NAT such that
A172: [ii,(jj + 1)] in Indices (Gauge C,n) and
A173: [ii,jj] in Indices (Gauge C,n) and
A174: (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 = (Gauge C,n) * ii,(jj + 1) and
A175: (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. (1 + 1) = (Gauge C,n) * ii,jj by A79, A167, A170, JORDAN1I:25;
consider jj2 being Element of NAT such that
A176: ( 1 <= jj2 & jj2 <= width (Gauge C,n) ) and
A177: E-max (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),jj2 by JORDAN1D:29;
A178: len (Gauge C,n) >= 4 by JORDAN8:13;
then len (Gauge C,n) >= 1 by XXREAL_0:2;
then [(len (Gauge C,n)),jj2] in Indices (Gauge C,n) by A176, MATRIX_1:37;
then A179: ii = len (Gauge C,n) by A166, A171, A172, A174, A177, GOBOARD1:21;
A180: ( 1 <= ii & ii <= len (Gauge C,n) & 1 <= jj + 1 & jj + 1 <= width (Gauge C,n) ) by A172, MATRIX_1:39;
A181: ( 1 <= ii & ii <= len (Gauge C,n) & 1 <= jj & jj <= width (Gauge C,n) ) by A173, MATRIX_1:39;
A182: ii + 1 <> ii ;
(jj + 1) + 1 <> jj ;
then A183: right_cell (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))),1 = cell (Gauge C,n),(ii -' 1),jj by A79, A167, A168, A172, A173, A174, A175, A182, GOBOARD5:def 6;
A184: (ii -' 1) + 1 = ii by A180, XREAL_1:237;
ii - 1 >= 4 - 1 by A178, A179, XREAL_1:11;
then A185: ii - 1 >= 1 by XXREAL_0:2;
then A186: 1 <= ii -' 1 by XREAL_0:def 2;
A187: ( ((Gauge C,n) * (ii -' 1),jj) `2 <= p `2 & p `2 <= ((Gauge C,n) * (ii -' 1),(jj + 1)) `2 ) by A162, A163, A180, A181, A183, A184, A185, JORDAN9:19;
A188: ii -' 1 < len (Gauge C,n) by A180, A184, NAT_1:13;
then A189: ((Gauge C,n) * (ii -' 1),jj) `2 = ((Gauge C,n) * 1,jj) `2 by A181, A186, GOBOARD5:2
.= ((Gauge C,n) * ii,jj) `2 by A181, GOBOARD5:2 ;
A190: ((Gauge C,n) * (ii -' 1),(jj + 1)) `2 = ((Gauge C,n) * 1,(jj + 1)) `2 by A180, A186, A188, GOBOARD5:2
.= ((Gauge C,n) * ii,(jj + 1)) `2 by A180, GOBOARD5:2 ;
( ((Gauge C,n) * (len (Gauge C,n)),jj) `1 = E-bound (L~ (Cage C,n)) & E-bound (L~ (Cage C,n)) = ((Gauge C,n) * (len (Gauge C,n)),(jj + 1)) `1 ) by A8, A180, A181, JORDAN1A:92;
then p in LSeg ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1),((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. (1 + 1)) by A161, A174, A175, A179, A187, A189, A190, GOBOARD7:8;
then A191: p in LSeg (Lower_Seq C,n),1 by A79, A165, A167, TOPREAL1:def 5;
A192: p in LSeg do,(Index p,do) by A160, JORDAN3:42;
A193: do = mid (Lower_Seq C,n),(((Gauge C,n) * j,i) .. (Lower_Seq C,n)),(len (Lower_Seq C,n)) by A34, JORDAN1J:37;
A194: ( 1 <= ((Gauge C,n) * j,i) .. (Lower_Seq C,n) & ((Gauge C,n) * j,i) .. (Lower_Seq C,n) <= len (Lower_Seq C,n) ) by A34, FINSEQ_4:31;
((Gauge C,n) * j,i) .. (Lower_Seq C,n) <> len (Lower_Seq C,n) by A26, A34, FINSEQ_4:29;
then A195: ((Gauge C,n) * j,i) .. (Lower_Seq C,n) < len (Lower_Seq C,n) by A194, XXREAL_0:1;
A196: ( 1 <= Index p,do & Index p,do < len do ) by A160, JORDAN3:41;
A197: (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) + 1 = ((Gauge C,n) * j,i) .. (Lower_Seq C,n) by A29, A34, JORDAN1J:56;
consider t being Nat such that
A198: t in dom (Lower_Seq C,n) and
A199: (Lower_Seq C,n) . t = (Gauge C,n) * j,i by A34, FINSEQ_2:11;
A200: ( 1 <= t & t <= len (Lower_Seq C,n) ) by A198, FINSEQ_3:27;
then 1 < t by A29, A199, XXREAL_0:1;
then (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) + 1 = t by A199, A200, JORDAN3:45;
then A201: len (L_Cut (Lower_Seq C,n),((Gauge C,n) * j,i)) = (len (Lower_Seq C,n)) - (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) by A6, A199, JORDAN3:61;
set tt = ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1;
A202: ( 1 <= Index ((Gauge C,n) * j,i),(Lower_Seq C,n) & 0 + (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) < len (Lower_Seq C,n) ) by A6, JORDAN3:41;
then A203: (len (Lower_Seq C,n)) - (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) > 0 by XREAL_1:22;
Index p,do < (len (Lower_Seq C,n)) -' (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) by A196, A201, XREAL_0:def 2;
then (Index p,do) + 1 <= (len (Lower_Seq C,n)) -' (Index ((Gauge C,n) * j,i),(Lower_Seq C,n)) by NAT_1:13;
then Index p,do <= ((len (Lower_Seq C,n)) -' (Index ((Gauge C,n) * j,i),(Lower_Seq C,n))) - 1 by XREAL_1:21;
then Index p,do <= ((len (Lower_Seq C,n)) - (Index ((Gauge C,n) * j,i),(Lower_Seq C,n))) - 1 by A203, XREAL_0:def 2;
then Index p,do <= (len (Lower_Seq C,n)) - (((Gauge C,n) * j,i) .. (Lower_Seq C,n)) by A197;
then Index p,do <= (len (Lower_Seq C,n)) -' (((Gauge C,n) * j,i) .. (Lower_Seq C,n)) by XREAL_0:def 2;
then Index p,do < ((len (Lower_Seq C,n)) -' (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) + 1 by NAT_1:13;
then A204: LSeg (mid (Lower_Seq C,n),(((Gauge C,n) * j,i) .. (Lower_Seq C,n)),(len (Lower_Seq C,n))),(Index p,do) = LSeg (Lower_Seq C,n),(((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1) by A194, A195, A196, JORDAN4:31;
A205: 1 + 1 <= ((Gauge C,n) * j,i) .. (Lower_Seq C,n) by A197, A202, XREAL_1:9;
then (Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n)) >= (1 + 1) + 1 by A196, XREAL_1:9;
then ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) - 1 >= ((1 + 1) + 1) - 1 by XREAL_1:11;
then A206: ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1 >= 1 + 1 by XREAL_0:def 2;
A207: 2 in dom (Lower_Seq C,n) by A164, FINSEQ_3:27;

now

per cases ) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1 > 1 + 1 or ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1 = 1 + 1 ) by A206, XXREAL_0:1;

suppose ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1 > 1 + 1 ; :: thesis:

then LSeg (Lower_Seq C,n),1 misses LSeg (Lower_Seq C,n),(((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1) by TOPREAL1:def 9;
hence contradiction by A191, A192, A193, A204, XBOOLE_0:3; :: thesis:

end;

suppose A208: ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1 = 1 + 1 ; :: thesis:

then (LSeg (Lower_Seq C,n),1) /\ (LSeg (Lower_Seq C,n),(((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) -' 1)) = {((Lower_Seq C,n) /. 2)} by A21, TOPREAL1:def 8;
then p in {((Lower_Seq C,n) /. 2)} by A191, A192, A193, A204, XBOOLE_0:def 4;
then A209: p = (Lower_Seq C,n) /. 2 by TARSKI:def 1;
then A210: p .. (Lower_Seq C,n) = 2 by A207, FINSEQ_5:44;
1 + 1 = ((Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n))) - 1 by A208, XREAL_0:def 2;
then (1 + 1) + 1 = (Index p,do) + (((Gauge C,n) * j,i) .. (Lower_Seq C,n)) ;
then A211: ((Gauge C,n) * j,i) .. (Lower_Seq C,n) = 2 by A196, A205, JORDAN1E:10;
p in rng (Lower_Seq C,n) by A207, A209, PARTFUN2:4;
then p = (Gauge C,n) * j,i by A34, A210, A211, FINSEQ_5:10;
then ((Gauge C,n) * j,i) `1 = E-bound (L~ (Cage C,n)) by A209, JORDAN1G:40;
then ((Gauge C,n) * j,i) `1 = ((Gauge C,n) * (len (Gauge C,n)),j) `1 by A8, A10, JORDAN1A:92;
hence contradiction by A1, A12, A61, JORDAN1G:7; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then east_halfline (E-max C) c= (L~ godo) ` by SUBSET_1:43;
then consider W being Subset of (TOP-REAL 2) such that
A212: W is_a_component_of (L~ godo) ` and
A213: east_halfline (E-max C) c= W by GOBOARD9:5;
not W is Bounded by A213, JORDAN2C:16, JORDAN2C:129;
then W is_outside_component_of L~ godo by A212, JORDAN2C:def 4;
then W c= UBD (L~ godo) by JORDAN2C:27;
then A214: east_halfline (E-max C) c= UBD (L~ godo) by A213, XBOOLE_1:1;
E-max C in east_halfline (E-max C) by TOPREAL1:45;
then E-max C in UBD (L~ godo) by A214;
then E-max C in LeftComp godo by GOBRD14:46;
then Lower_Arc C meets L~ godo by A116, A117, A125, A133, JORDAN1J:36;
then A215: ( Lower_Arc C meets (L~ go) \/ (L~ pion1) or Lower_Arc C meets L~ do ) by A126, XBOOLE_1:70;
A216: Lower_Arc C c= C by JORDAN6:76;

per cases by A215, XBOOLE_1:70;

suppose Lower_Arc C meets L~ go ; :: thesis:

then Lower_Arc C meets L~ (Cage C,n) by A43, A127, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A216, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;

suppose Lower_Arc C meets L~ pion1 ; :: thesis:

hence contradiction by A5, A75, A130; :: thesis:

end;

suppose Lower_Arc C meets L~ do ; :: thesis:

then Lower_Arc C meets L~ (Cage C,n) by A50, A127, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A216, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;