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

end;

then A53: (LSeg (go,m)) /\ (LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i)))) = {((Gauge (C,n)) * (k,i))} by A49, XBOOLE_0:def 10;
A54: LSeg (do,1) c= L~ do by TOPREAL3:26;
A55: L~ do c= L~ (Lower_Seq (C,n)) by A9, JORDAN3:77;
then LSeg (do,1) c= L~ (Lower_Seq (C,n)) by A54, XBOOLE_1:1;
then A56: (LSeg (do,1)) /\ (LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i)))) c= {((Gauge (C,n)) * (j,i))} by A7, XBOOLE_1:26;
A57: LSeg (do,1) = LSeg (((Gauge (C,n)) * (j,i)),(do /. (1 + 1))) by A38, A44, 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:
A58: (Gauge (C,n)) * (j,i) in LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))) by RLTOPSP1:69;
assume x in {((Gauge (C,n)) * (j,i))} ; :: thesis:
then A59: x = (Gauge (C,n)) * (j,i) by TARSKI:def 1;
(Gauge (C,n)) * (j,i) in LSeg (do,1) by A57, RLTOPSP1:69;
hence x in (LSeg (do,1)) /\ (LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i)))) by A59, A58, XBOOLE_0:def 4; :: thesis:

end;

then A60: (LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i)))) /\ (LSeg (do,1)) = {((Gauge (C,n)) * (j,i))} by A56, XBOOLE_0:def 10;
A61: go /. 1 = (Upper_Seq (C,n)) /. 1 by A10, SPRECT_3:39
.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;
then A62: go /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by JORDAN1F:8
.= do /. (len do) by A9, JORDAN1J:35 ;
A63: rng go c= L~ go by A35, SPPOL_2:18;
A64: rng do c= L~ do by A38, SPPOL_2:18;
A65: {(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 A66: x = go /. 1 by TARSKI:def 1;
then A67: x in rng go by FINSEQ_6:46;
x in rng do by A62, A66, REVROT_1:3;
hence x in (L~ go) /\ (L~ do) by A63, A64, A67, XBOOLE_0:def 4; :: thesis:

end;

A68: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A27, PARTFUN1:def 8
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
A69: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, A13, A21, MATRIX_1:37;
(L~ go) /\ (L~ do) c= {(go /. 1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A70: x in (L~ go) /\ (L~ do) ; :: thesis:
then A71: x in L~ do by XBOOLE_0:def 4;

A72: now

assume x = E-max (L~ (Cage (C,n))) ; :: thesis:
then A73: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (j,i) by A9, A68, A71, JORDAN1E:11;
((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = E-bound (L~ (Cage (C,n))) by A1, A11, A13, JORDAN1A:92;
then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A2, A3, A16, A69, A73, JORDAN1G:7;
hence contradiction by EUCLID:56; :: thesis:

end;

x in L~ go by A70, XBOOLE_0:def 4;
then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A48, A55, A71, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:20;
then ( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) ) by TARSKI:def 2;
hence x in {(go /. 1)} by A61, A72, TARSKI:def 1; :: thesis:

end;

then A74: (L~ go) /\ (L~ do) = {(go /. 1)} by A65, XBOOLE_0:def 10;
set W2 = go /. 2;
A75: 2 in dom go by A35, FINSEQ_3:27;

A76: 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 A1, A11, A13, JORDAN1A:94;
hence contradiction by A1, A16, A24, JORDAN1G:7; :: thesis:

end;

go = mid ((Upper_Seq (C,n)),1,(((Gauge (C,n)) * (k,i)) .. (Upper_Seq (C,n)))) by A36, JORDAN1G:57
.= (Upper_Seq (C,n)) | (((Gauge (C,n)) * (k,i)) .. (Upper_Seq (C,n))) by A36, FINSEQ_4:31, FINSEQ_6:122 ;
then A77: go /. 2 = (Upper_Seq (C,n)) /. 2 by A75, FINSEQ_4:85;
A78: W-min (L~ (Cage (C,n))) in rng go by A61, FINSEQ_6:46;
set pion = <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*>;

A79: 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;
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 A16, A17, FINSEQ_4:26; :: thesis:

end;

A80: (Gauge (C,n)) * (k,i) <> (Gauge (C,n)) * (j,i) by A12, A16, A17, GOBOARD1:21;
((Gauge (C,n)) * (k,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by A3, A4, A5, A14, GOBOARD5:2
.= ((Gauge (C,n)) * (j,i)) `2 by A1, A4, A5, A11, A13, 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 A80, JORDAN1B:9;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A81: pion1 is_sequence_on Gauge (C,n) and
A82: pion1 is being_S-Seq and
A83: L~ <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> = L~ pion1 and
A84: <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> /. 1 = pion1 /. 1 and
A85: <*((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
A86: len <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> <= len pion1 by A79, GOBOARD3:2;
reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A82;
set godo = (go ^' pion1) ^' do;
A87: 1 + 1 <= len (Cage (C,n)) by GOBOARD7:36, XXREAL_0:2;
A88: 1 + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by GOBOARD7:36, XXREAL_0:2;
len (go ^' pion1) >= len go by TOPREAL8:7;
then A89: len (go ^' pion1) >= 1 + 1 by A35, XXREAL_0:2;
then A90: len (go ^' pion1) > 1 + 0 by NAT_1:13;
A91: len ((go ^' pion1) ^' do) >= len (go ^' pion1) by TOPREAL8:7;
then A92: 1 + 1 <= len ((go ^' pion1) ^' do) by A89, XXREAL_0:2;
A93: Upper_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1G:4;
A94: go /. (len go) = pion1 /. 1 by A43, A84, FINSEQ_4:26;
then A95: go ^' pion1 is_sequence_on Gauge (C,n) by A37, A81, TOPREAL8:12;
A96: (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 A85, GRAPH_2:58
.= <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> /. 2 by FINSEQ_1:61
.= do /. 1 by A44, FINSEQ_4:26 ;
then A97: (go ^' pion1) ^' do is_sequence_on Gauge (C,n) by A40, A95, TOPREAL8:12;
LSeg (pion1,1) c= L~ <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> by A83, TOPREAL3:26;
then LSeg (pion1,1) c= LSeg (((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))) by SPPOL_2:21;
then A98: (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) c= {((Gauge (C,n)) * (k,i))} by A46, A53, XBOOLE_1:27;
A99: len pion1 >= 1 + 1 by A86, 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 A100: x = (Gauge (C,n)) * (k,i) by TARSKI:def 1;
A101: (Gauge (C,n)) * (k,i) in LSeg (go,m) by A50, RLTOPSP1:69;
(Gauge (C,n)) * (k,i) in LSeg (pion1,1) by A43, A94, A99, TOPREAL1:27;
hence x in (LSeg (go,m)) /\ (LSeg (pion1,1)) by A100, A101, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) = {(go /. (len go))} by A43, A46, A98, XBOOLE_0:def 10;
then A102: go ^' pion1 is unfolded by A94, TOPREAL8:34;
len pion1 >= 2 + 0 by A86, FINSEQ_1:61;
then A103: (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 A103, XREAL_0:def 2 ;
then A104: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;
A105: (len pion1) - 1 >= 1 by A99, XREAL_1:21;
then A106: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;
A107: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A103, XREAL_0:def 2
.= (len pion1) -' 1 by A105, XREAL_0:def 2 ;
((len pion1) - 1) + 1 <= len pion1 ;
then A108: (len pion1) -' 1 < len pion1 by A106, NAT_1:13;
LSeg (pion1,((len pion1) -' 1)) c= L~ <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> by A83, 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 A109: (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (do,1)) c= {((Gauge (C,n)) * (j,i))} by A60, 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 A110: x = (Gauge (C,n)) * (j,i) by TARSKI:def 1;
pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge (C,n)) * (k,i)),((Gauge (C,n)) * (j,i))*> /. 2 by A85, A106, FINSEQ_1:61
.= (Gauge (C,n)) * (j,i) by FINSEQ_4:26 ;
then A111: (Gauge (C,n)) * (j,i) in LSeg (pion1,((len pion1) -' 1)) by A105, A106, TOPREAL1:27;
(Gauge (C,n)) * (j,i) in LSeg (do,1) by A57, RLTOPSP1:69;
hence x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (do,1)) by A110, A111, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (do,1)) = {((Gauge (C,n)) * (j,i))} by A109, XBOOLE_0:def 10;
then A112: (LSeg ((go ^' pion1),((len go) + ((len pion1) -' 2)))) /\ (LSeg (do,1)) = {((go ^' pion1) /. (len (go ^' pion1)))} by A44, A94, A96, A107, A108, TOPREAL8:31;
A113: not go ^' pion1 is trivial by A89, REALSET1:13;
A114: rng pion1 c= L~ pion1 by A99, SPPOL_2:18;
A115: {(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 A116: x = pion1 /. 1 by TARSKI:def 1;
then A117: x in rng pion1 by FINSEQ_6:46;
x in rng go by A94, A116, REVROT_1:3;
hence x in (L~ go) /\ (L~ pion1) by A63, A114, A117, 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 A118: x in (L~ go) /\ (L~ pion1) ; :: thesis:
then A119: x in L~ pion1 by XBOOLE_0:def 4;
x in L~ go by A118, XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Upper_Seq (C,n))) by A48, A119, XBOOLE_0:def 4;
hence x in {(pion1 /. 1)} by A6, A43, A83, A94, SPPOL_2:21; :: thesis:

end;

then A120: (L~ go) /\ (L~ pion1) = {(pion1 /. 1)} by A115, XBOOLE_0:def 10;
then A121: go ^' pion1 is s.n.c. by A94, JORDAN1J:54;
(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A63, A114, A120, XBOOLE_1:27;
then A122: go ^' pion1 is one-to-one by JORDAN1J:55;
A123: <*((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 A44, FINSEQ_4:26 ;
A124: {(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 A125: x = pion1 /. (len pion1) by TARSKI:def 1;
then A126: x in rng pion1 by REVROT_1:3;
x in rng do by A85, A123, A125, FINSEQ_6:46;
hence x in (L~ do) /\ (L~ pion1) by A64, A114, A126, 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 A127: x in (L~ do) /\ (L~ pion1) ; :: thesis:
then A128: x in L~ pion1 by XBOOLE_0:def 4;
x in L~ do by A127, XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Lower_Seq (C,n))) by A55, A128, XBOOLE_0:def 4;
hence x in {(pion1 /. (len pion1))} by A7, A44, A83, A85, A123, SPPOL_2:21; :: thesis:

end;

A138: now

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

end;

A140: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A141: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
A142: (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) c= RightComp godo by A92, A97, JORDAN9:29;
A143: L~ godo = (L~ (go ^' pion1)) \/ (L~ do) by A96, TOPREAL8:35
.= ((L~ go) \/ (L~ pion1)) \/ (L~ do) by A94, TOPREAL8:35 ;
A144: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:17;
then A145: L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n)) by XBOOLE_1:7;
A146: L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n)) by A144, XBOOLE_1:7;
A147: L~ go c= L~ (Cage (C,n)) by A48, A145, XBOOLE_1:1;
A148: L~ do c= L~ (Cage (C,n)) by A55, A146, XBOOLE_1:1;
A149: W-min C in C by SPRECT_1:15;
A150: 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;

A151: now

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

per cases by A152, XBOOLE_0:def 3;

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

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

end;

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

hence contradiction by A8, A83, A133, A150, XBOOLE_0:3; :: thesis:

end;

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

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

end;

proof

assume east_halfline (E-max C) meets L~ go ; :: thesis:
then consider p being set such that
A168: p in east_halfline (E-max C) and
A169: p in L~ go by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A168;
p in L~ (Upper_Seq (C,n)) by A48, A169;
then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A145, A168, XBOOLE_0:def 4;
then A170: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:104, PSCOMP_1:111;
then A171: p = E-max (L~ (Cage (C,n))) by A48, A169, JORDAN1J:46;
then E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (k,i) by A10, A166, A169, JORDAN1J:43;
then ((Gauge (C,n)) * (k,i)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A3, A14, A170, A171, JORDAN1A:92;
hence contradiction by A3, A17, A32, JORDAN1G:7; :: thesis:

end;

now

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

per cases by A172, XBOOLE_1:70;

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

hence contradiction by A167; :: thesis:

end;

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

then consider p being set such that
A173: p in east_halfline (E-max C) and
A174: p in L~ pion1 by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A173;
A175: p `2 = (E-max C) `2 by A173, TOPREAL1:def 13;
k + 1 <= len (Gauge (C,n)) by A3, NAT_1:13;
then (k + 1) - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:11;
then A176: 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 A177: ((Gauge (C,n)) * (k,i)) `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A4, A5, A11, A14, A21, A176, JORDAN1A:39;
p `1 <= ((Gauge (C,n)) * (k,i)) `1 by A83, A150, A161, A174, TOPREAL1:9;
then p `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A177, XXREAL_0:2;
then p `1 <= E-bound C by A21, JORDAN8:15;
then A178: p `1 <= (E-max C) `1 by EUCLID:56;
p `1 >= (E-max C) `1 by A173, TOPREAL1:def 13;
then p `1 = (E-max C) `1 by A178, XXREAL_0:1;
then p = E-max C by A175, TOPREAL3:11;
hence contradiction by A8, A83, A134, A150, A174, XBOOLE_0:3; :: thesis:

end;

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

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 A235, 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 A232, A181, A187, A233, XBOOLE_0:3; :: thesis:

end;

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

then 1 + 1 = ((Index (p,do)) + (((Gauge (C,n)) * (j,i)) .. (Lower_Seq (C,n)))) - 1 by XREAL_0:def 2;
then (1 + 1) + 1 = (Index (p,do)) + (((Gauge (C,n)) * (j,i)) .. (Lower_Seq (C,n))) ;
then A237: ((Gauge (C,n)) * (j,i)) .. (Lower_Seq (C,n)) = 2 by A191, A234, JORDAN1E:10;
(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 A25, A236, TOPREAL1:def 8;
then p in {((Lower_Seq (C,n)) /. 2)} by A232, A181, A187, A233, XBOOLE_0:def 4;
then A238: p = (Lower_Seq (C,n)) /. 2 by TARSKI:def 1;
then A239: p in rng (Lower_Seq (C,n)) by A195, PARTFUN2:4;
p .. (Lower_Seq (C,n)) = 2 by A195, A238, FINSEQ_5:44;
then p = (Gauge (C,n)) * (j,i) by A39, A237, A239, FINSEQ_5:10;
then ((Gauge (C,n)) * (j,i)) `1 = E-bound (L~ (Cage (C,n))) by A238, JORDAN1G:40;
then ((Gauge (C,n)) * (j,i)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A1, A11, A13, JORDAN1A:92;
hence contradiction by A2, A3, A16, A69, 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
A240: W is_a_component_of (L~ godo) ` and
A241: east_halfline (E-max C) c= W by GOBOARD9:5;
not W is Bounded by A241, JORDAN2C:16, JORDAN2C:129;
then W is_outside_component_of L~ godo by A240, JORDAN2C:def 4;
then W c= UBD (L~ godo) by JORDAN2C:27;
then A242: east_halfline (E-max C) c= UBD (L~ godo) by A241, XBOOLE_1:1;
E-max C in east_halfline (E-max C) by TOPREAL1:45;
then E-max C in UBD (L~ godo) by A242;
then E-max C in LeftComp godo by GOBRD14:46;
then Lower_Arc C meets L~ godo by A132, A133, A134, A142, A153, JORDAN1J:36;
then A243: ( Lower_Arc C meets (L~ go) \/ (L~ pion1) or Lower_Arc C meets L~ do ) by A143, XBOOLE_1:70;
A244: Lower_Arc C c= C by JORDAN6:76;

per cases by A243, XBOOLE_1:70;

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

then Lower_Arc C meets L~ (Cage (C,n)) by A48, A145, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A244, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;

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

hence contradiction by A8, A83, A150; :: thesis:

end;

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

then Lower_Arc C meets L~ (Cage (C,n)) by A55, A146, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A244, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;