let n be Nat; :: thesis:
let C be Simple_closed_curve; :: thesis:
let i, j, k be 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)) * (i,j);
set Gik = (Gauge (C,n)) * (i,k);
assume that
A1: 1 < i and
A2: i < len (Gauge (C,n)) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width (Gauge (C,n)) and
A6: (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} and
A7: (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} and
A8: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) misses Lower_Arc C ; :: thesis:
(Gauge (C,n)) * (i,j) in {((Gauge (C,n)) * (i,j))} by TARSKI:def 1;
then A9: (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) by A7, XBOOLE_0:def 4;
(Gauge (C,n)) * (i,k) in {((Gauge (C,n)) * (i,k))} by TARSKI:def 1;
then A10: (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) by A6, XBOOLE_0:def 4;
then A11: j <> k by A1, A2, A3, A5, A9, Th57;
A12: j <= width (Gauge (C,n)) by A4, A5, XXREAL_0:2;
A13: 1 <= k by A3, A4, XXREAL_0:2;
A14: [i,j] in Indices (Gauge (C,n)) by A1, A2, A3, A12, MATRIX_0:30;
A15: [i,k] in Indices (Gauge (C,n)) by A1, A2, A5, A13, MATRIX_0:30;
set go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,k)));
set co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)));
A16: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A17: len (Upper_Seq (C,n)) >= 3 by JORDAN1E:15;
then len (Upper_Seq (C,n)) >= 1 by XXREAL_0:2;
then 1 in dom (Upper_Seq (C,n)) by FINSEQ_3:25;
then A18: (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6
.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;
A19: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52
.= ((Gauge (C,n)) * (1,k)) `1 by A5, A13, A16, JORDAN1A:73 ;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A20: len (Gauge (C,n)) >= 1 by XXREAL_0:2;
then A21: [1,k] in Indices (Gauge (C,n)) by A5, A13, MATRIX_0:30;
then A22: (Gauge (C,n)) * (i,k) <> (Upper_Seq (C,n)) . 1 by A1, A15, A18, A19, JORDAN1G:7;
then reconsider go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i,k))) as being_S-Seq FinSequence of (TOP-REAL 2) by A10, JORDAN3:35;
A23: len (Lower_Seq (C,n)) >= 1 + 2 by JORDAN1E:15;
then A24: len (Lower_Seq (C,n)) >= 1 by XXREAL_0:2;
then A25: 1 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A24, FINSEQ_3:25;
then A26: (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by PARTFUN1:def 6
.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;
A27: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52
.= ((Gauge (C,n)) * (1,k)) `1 by A5, A13, A16, JORDAN1A:73 ;
A28: [i,j] in Indices (Gauge (C,n)) by A1, A2, A3, A12, MATRIX_0:30;
then A29: (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A1, A21, A26, A27, JORDAN1G:7;
then reconsider co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) as being_S-Seq FinSequence of (TOP-REAL 2) by A9, JORDAN3:34;
A30: [(len (Gauge (C,n))),k] in Indices (Gauge (C,n)) by A5, A13, A20, MATRIX_0:30;
A31: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A25, PARTFUN1:def 6
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
(E-max (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) by EUCLID:52
.= ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A5, A13, A16, JORDAN1A:71 ;
then A32: (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . 1 by A2, A28, A30, A31, JORDAN1G:7;
A33: len go >= 1 + 1 by TOPREAL1:def 8;
A34: (Gauge (C,n)) * (i,k) in rng (Upper_Seq (C,n)) by A1, A2, A5, A10, A13, Th40, JORDAN1G:4;
then A35: go is_sequence_on Gauge (C,n) by Th38, JORDAN1G:4;
A36: len co >= 1 + 1 by TOPREAL1:def 8;
A37: (Gauge (C,n)) * (i,j) in rng (Lower_Seq (C,n)) by A1, A2, A3, A9, A12, Th40, JORDAN1G:5;
then A38: co is_sequence_on Gauge (C,n) by Th39, JORDAN1G:5;
reconsider go = go as constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A33, A35, JGRAPH_1:12, JORDAN8:5;
reconsider co = co as constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A36, A38, JGRAPH_1:12, JORDAN8:5;
A39: len go > 1 by A33, NAT_1:13;
then A40: len go in dom go by FINSEQ_3:25;
then A41: go /. (len go) = go . (len go) by PARTFUN1:def 6
.= (Gauge (C,n)) * (i,k) by A10, JORDAN3:24 ;
len co >= 1 by A36, XXREAL_0:2;
then 1 in dom co by FINSEQ_3:25;
then A42: co /. 1 = co . 1 by PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j) by A9, JORDAN3:23 ;
reconsider m = (len go) - 1 as Nat by A40, FINSEQ_3:26;
A43: m + 1 = len go ;
then A44: (len go) -' 1 = m by NAT_D:34;
A45: LSeg (go,m) c= L~ go by TOPREAL3:19;
A46: L~ go c= L~ (Upper_Seq (C,n)) by A10, JORDAN3:41;
then LSeg (go,m) c= L~ (Upper_Seq (C,n)) by A45;
then A47: (LSeg (go,m)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) c= {((Gauge (C,n)) * (i,k))} by A6, XBOOLE_1:26;
m >= 1 by A33, XREAL_1:19;
then A48: LSeg (go,m) = LSeg ((go /. m),((Gauge (C,n)) * (i,k))) by A41, A43, TOPREAL1:def 3;
{((Gauge (C,n)) * (i,k))} c= (LSeg (go,m)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A49: (Gauge (C,n)) * (i,k) in LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
assume x in {((Gauge (C,n)) * (i,k))} ; :: thesis:
then A50: x = (Gauge (C,n)) * (i,k) by TARSKI:def 1;
(Gauge (C,n)) * (i,k) in LSeg (go,m) by A48, RLTOPSP1:68;
hence x in (LSeg (go,m)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) by A50, A49, XBOOLE_0:def 4; :: thesis:

end;

then A51: (LSeg (go,m)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) = {((Gauge (C,n)) * (i,k))} by A47;
A52: LSeg (co,1) c= L~ co by TOPREAL3:19;
A53: L~ co c= L~ (Lower_Seq (C,n)) by A9, JORDAN3:42;
then LSeg (co,1) c= L~ (Lower_Seq (C,n)) by A52;
then A54: (LSeg (co,1)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) c= {((Gauge (C,n)) * (i,j))} by A7, XBOOLE_1:26;
A55: LSeg (co,1) = LSeg (((Gauge (C,n)) * (i,j)),(co /. (1 + 1))) by A36, A42, TOPREAL1:def 3;
{((Gauge (C,n)) * (i,j))} c= (LSeg (co,1)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A56: (Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;
assume x in {((Gauge (C,n)) * (i,j))} ; :: thesis:
then A57: x = (Gauge (C,n)) * (i,j) by TARSKI:def 1;
(Gauge (C,n)) * (i,j) in LSeg (co,1) by A55, RLTOPSP1:68;
hence x in (LSeg (co,1)) /\ (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) by A57, A56, XBOOLE_0:def 4; :: thesis:

end;

then A58: (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (LSeg (co,1)) = {((Gauge (C,n)) * (i,j))} by A54;
A59: go /. 1 = (Upper_Seq (C,n)) /. 1 by A10, SPRECT_3:22
.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;
then A60: go /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by JORDAN1F:8
.= co /. (len co) by A9, Th35 ;
A61: rng go c= L~ go by A33, SPPOL_2:18;
A62: rng co c= L~ co by A36, SPPOL_2:18;
A63: {(go /. 1)} c= (L~ go) /\ (L~ co)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {(go /. 1)} ; :: thesis:
then A64: x = go /. 1 by TARSKI:def 1;
then A65: x in rng go by FINSEQ_6:42;
x in rng co by A60, A64, FINSEQ_6:168;
hence x in (L~ go) /\ (L~ co) by A61, A62, A65, XBOOLE_0:def 4; :: thesis:

end;

A66: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A25, PARTFUN1:def 6
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
A67: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A3, A12, A20, MATRIX_0:30;
(L~ go) /\ (L~ co) c= {(go /. 1)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A68: x in (L~ go) /\ (L~ co) ; :: thesis:
then A69: x in L~ co by XBOOLE_0:def 4;

A70: now :: thesis:

assume x = E-max (L~ (Cage (C,n))) ; :: thesis:
then A71: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,j) by A9, A66, A69, JORDAN1E:7;
((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = E-bound (L~ (Cage (C,n))) by A3, A12, A16, JORDAN1A:71;
then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A2, A14, A67, A71, JORDAN1G:7;
hence contradiction by EUCLID:52; :: thesis:

end;

x in L~ go by A68, XBOOLE_0:def 4;
then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A46, A53, A69, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
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 A59, A70, TARSKI:def 1; :: thesis:

end;

then A72: (L~ go) /\ (L~ co) = {(go /. 1)} by A63;
set W2 = go /. 2;
A73: 2 in dom go by A33, FINSEQ_3:25;

A74: now :: thesis:

assume ((Gauge (C,n)) * (i,k)) `1 = W-bound (L~ (Cage (C,n))) ; :: thesis:
then ((Gauge (C,n)) * (1,k)) `1 = ((Gauge (C,n)) * (i,k)) `1 by A5, A13, A16, JORDAN1A:73;
hence contradiction by A1, A15, A21, JORDAN1G:7; :: thesis:

end;

go = mid ((Upper_Seq (C,n)),1,(((Gauge (C,n)) * (i,k)) .. (Upper_Seq (C,n)))) by A34, JORDAN1G:49
.= (Upper_Seq (C,n)) | (((Gauge (C,n)) * (i,k)) .. (Upper_Seq (C,n))) by A34, FINSEQ_4:21, FINSEQ_6:116 ;
then A75: go /. 2 = (Upper_Seq (C,n)) /. 2 by A73, FINSEQ_4:70;
set pion = <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*>;

A76: now :: thesis:

let n be Nat; :: thesis:
assume n in dom <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> ; :: thesis:
then n in Seg 2 by FINSEQ_1:89;
then ( n = 1 or n = 2 ) by FINSEQ_1:2, TARSKI:def 2;
hence ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. n = (Gauge (C,n)) * (i,j) ) by A14, A15, FINSEQ_4:17; :: thesis:

end;

A77: (Gauge (C,n)) * (i,k) <> (Gauge (C,n)) * (i,j) by A11, A14, A15, GOBOARD1:5;
A78: ((Gauge (C,n)) * (i,k)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, A13, GOBOARD5:2
.= ((Gauge (C,n)) * (i,j)) `1 by A1, A2, A3, A12, GOBOARD5:2 ;
then LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) is vertical by SPPOL_1:16;
then <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> is being_S-Seq by A77, JORDAN1B:7;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A79: pion1 is_sequence_on Gauge (C,n) and
A80: pion1 is being_S-Seq and
A81: L~ <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> = L~ pion1 and
A82: <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. 1 = pion1 /. 1 and
A83: <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. (len <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*>) = pion1 /. (len pion1) and
A84: len <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> <= len pion1 by A76, GOBOARD3:2;
reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A80;
set godo = (go ^' pion1) ^' co;
A85: 1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
A86: 1 + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by GOBOARD7:34, XXREAL_0:2;
len (go ^' pion1) >= len go by TOPREAL8:7;
then A87: len (go ^' pion1) >= 1 + 1 by A33, XXREAL_0:2;
then A88: len (go ^' pion1) > 1 + 0 by NAT_1:13;
A89: len ((go ^' pion1) ^' co) >= len (go ^' pion1) by TOPREAL8:7;
then A90: 1 + 1 <= len ((go ^' pion1) ^' co) by A87, XXREAL_0:2;
A91: Upper_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1G:4;
A92: go /. (len go) = pion1 /. 1 by A41, A82, FINSEQ_4:17;
then A93: go ^' pion1 is_sequence_on Gauge (C,n) by A35, A79, TOPREAL8:12;
A94: (go ^' pion1) /. (len (go ^' pion1)) = <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. (len <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*>) by A83, FINSEQ_6:156
.= <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. 2 by FINSEQ_1:44
.= co /. 1 by A42, FINSEQ_4:17 ;
then A95: (go ^' pion1) ^' co is_sequence_on Gauge (C,n) by A38, A93, TOPREAL8:12;
LSeg (pion1,1) c= L~ <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> by A81, TOPREAL3:19;
then LSeg (pion1,1) c= LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by SPPOL_2:21;
then A96: (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) c= {((Gauge (C,n)) * (i,k))} by A44, A51, XBOOLE_1:27;
A97: len pion1 >= 1 + 1 by A84, FINSEQ_1:44;
{((Gauge (C,n)) * (i,k))} c= (LSeg (go,m)) /\ (LSeg (pion1,1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge (C,n)) * (i,k))} ; :: thesis:
then A98: x = (Gauge (C,n)) * (i,k) by TARSKI:def 1;
A99: (Gauge (C,n)) * (i,k) in LSeg (go,m) by A48, RLTOPSP1:68;
(Gauge (C,n)) * (i,k) in LSeg (pion1,1) by A41, A92, A97, TOPREAL1:21;
hence x in (LSeg (go,m)) /\ (LSeg (pion1,1)) by A98, A99, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) = {(go /. (len go))} by A41, A44, A96;
then A100: go ^' pion1 is unfolded by A92, TOPREAL8:34;
len pion1 >= 2 + 0 by A84, FINSEQ_1:44;
then A101: (len pion1) - 2 >= 0 by XREAL_1:19;
((len (go ^' pion1)) + 1) - 1 = ((len go) + (len pion1)) - 1 by FINSEQ_6:139;
then (len (go ^' pion1)) - 1 = (len go) + ((len pion1) - 2)
.= (len go) + ((len pion1) -' 2) by A101, XREAL_0:def 2 ;
then A102: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;
A103: (len pion1) - 1 >= 1 by A97, XREAL_1:19;
then A104: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;
A105: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A101, XREAL_0:def 2
.= (len pion1) -' 1 by A103, XREAL_0:def 2 ;
((len pion1) - 1) + 1 <= len pion1 ;
then A106: (len pion1) -' 1 < len pion1 by A104, NAT_1:13;
LSeg (pion1,((len pion1) -' 1)) c= L~ <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> by A81, TOPREAL3:19;
then LSeg (pion1,((len pion1) -' 1)) c= LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by SPPOL_2:21;
then A107: (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) c= {((Gauge (C,n)) * (i,j))} by A58, XBOOLE_1:27;
{((Gauge (C,n)) * (i,j))} c= (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge (C,n)) * (i,j))} ; :: thesis:
then A108: x = (Gauge (C,n)) * (i,j) by TARSKI:def 1;
pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. 2 by A83, A104, FINSEQ_1:44
.= (Gauge (C,n)) * (i,j) by FINSEQ_4:17 ;
then A109: (Gauge (C,n)) * (i,j) in LSeg (pion1,((len pion1) -' 1)) by A103, A104, TOPREAL1:21;
(Gauge (C,n)) * (i,j) in LSeg (co,1) by A55, RLTOPSP1:68;
hence x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) by A108, A109, XBOOLE_0:def 4; :: thesis:

end;

then (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) = {((Gauge (C,n)) * (i,j))} by A107;
then A110: (LSeg ((go ^' pion1),((len go) + ((len pion1) -' 2)))) /\ (LSeg (co,1)) = {((go ^' pion1) /. (len (go ^' pion1)))} by A42, A92, A94, A105, A106, TOPREAL8:31;
A111: not go ^' pion1 is trivial by A87, NAT_D:60;
A112: rng pion1 c= L~ pion1 by A97, SPPOL_2:18;
A113: {(pion1 /. 1)} c= (L~ go) /\ (L~ pion1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {(pion1 /. 1)} ; :: thesis:
then A114: x = pion1 /. 1 by TARSKI:def 1;
then A115: x in rng pion1 by FINSEQ_6:42;
x in rng go by A92, A114, FINSEQ_6:168;
hence x in (L~ go) /\ (L~ pion1) by A61, A112, A115, XBOOLE_0:def 4; :: thesis:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A116: x in (L~ go) /\ (L~ pion1) ; :: thesis:
then A117: x in L~ pion1 by XBOOLE_0:def 4;
x in L~ go by A116, XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Upper_Seq (C,n))) by A46, A117, XBOOLE_0:def 4;
hence x in {(pion1 /. 1)} by A6, A41, A81, A92, SPPOL_2:21; :: thesis:

end;

then A118: (L~ go) /\ (L~ pion1) = {(pion1 /. 1)} by A113;
then A119: go ^' pion1 is s.n.c. by A92, Th54;
(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A61, A112, A118, XBOOLE_1:27;
then A120: go ^' pion1 is one-to-one by Th55;
A121: <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. (len <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*>) = <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> /. 2 by FINSEQ_1:44
.= co /. 1 by A42, FINSEQ_4:17 ;
A122: {(pion1 /. (len pion1))} c= (L~ co) /\ (L~ pion1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {(pion1 /. (len pion1))} ; :: thesis:
then A123: x = pion1 /. (len pion1) by TARSKI:def 1;
then A124: x in rng pion1 by FINSEQ_6:168;
x in rng co by A83, A121, A123, FINSEQ_6:42;
hence x in (L~ co) /\ (L~ pion1) by A62, A112, A124, XBOOLE_0:def 4; :: thesis:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A125: x in (L~ co) /\ (L~ pion1) ; :: thesis:
then A126: x in L~ pion1 by XBOOLE_0:def 4;
x in L~ co by A125, XBOOLE_0:def 4;
then x in (L~ pion1) /\ (L~ (Lower_Seq (C,n))) by A53, A126, XBOOLE_0:def 4;
hence x in {(pion1 /. (len pion1))} by A7, A42, A81, A83, A121, SPPOL_2:21; :: thesis:

end;

A136: now :: thesis:

assume A137: ((Gauge (C,n)) * (i,k)) .. (Upper_Seq (C,n)) <= 1 ; :: thesis:
((Gauge (C,n)) * (i,k)) .. (Upper_Seq (C,n)) >= 1 by A34, FINSEQ_4:21;
then ((Gauge (C,n)) * (i,k)) .. (Upper_Seq (C,n)) = 1 by A137, XXREAL_0:1;
then (Gauge (C,n)) * (i,k) = (Upper_Seq (C,n)) /. 1 by A34, FINSEQ_5:38;
hence contradiction by A18, A22, JORDAN1F:5; :: thesis:

end;

A138: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A139: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
A140: (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) c= RightComp godo by A90, A95, JORDAN9:27;
A141: L~ godo = (L~ (go ^' pion1)) \/ (L~ co) by A94, TOPREAL8:35
.= ((L~ go) \/ (L~ pion1)) \/ (L~ co) by A92, TOPREAL8:35 ;
A142: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:13;
then A143: L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n)) by XBOOLE_1:7;
A144: L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n)) by A142, XBOOLE_1:7;
A145: L~ go c= L~ (Cage (C,n)) by A46, A143;
A146: L~ co c= L~ (Cage (C,n)) by A53, A144;
A147: W-min C in C by SPRECT_1:13;
A148: L~ <*((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))*> = LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by SPPOL_2:21;

A149: now :: thesis:

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

per cases by A150, XBOOLE_0:def 3;

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

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

end;

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

hence contradiction by A8, A81, A131, A148, XBOOLE_0:3; :: thesis:

end;

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

then C meets L~ (Cage (C,n)) by A146, A147, 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 A86, JORDAN1H:23
.= 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:44
.= right_cell (((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))),1,(Gauge (C,n))) by A135, A139, Th53
.= 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)) * (i,k)))),1,(Gauge (C,n))) by A34, A91, A136, Th52
.= right_cell ((go ^' pion1),1,(Gauge (C,n))) by A39, A93, Th51
.= right_cell (godo,1,(Gauge (C,n))) by A88, A95, Th51 ;
then W-min C in right_cell (godo,1,(Gauge (C,n))) by JORDAN1I:6;
then A151: W-min C in (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) by A149, XBOOLE_0:def 5;
A152: godo /. 1 = (go ^' pion1) /. 1 by FINSEQ_6:155
.= W-min (L~ (Cage (C,n))) by A59, FINSEQ_6:155 ;
A153: len (Upper_Seq (C,n)) >= 2 by A17, XXREAL_0:2;
A154: godo /. 2 = (go ^' pion1) /. 2 by A87, FINSEQ_6:159
.= (Upper_Seq (C,n)) /. 2 by A33, A75, FINSEQ_6:159
.= ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) /. 2 by A153, FINSEQ_6:159
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 2 by JORDAN1E:11 ;
A155: (L~ go) \/ (L~ co) is compact by COMPTS_1:10;
W-min (L~ (Cage (C,n))) in rng go by A59, FINSEQ_6:42;
then W-min (L~ (Cage (C,n))) in (L~ go) \/ (L~ co) by A61, XBOOLE_0:def 3;
then A156: W-min ((L~ go) \/ (L~ co)) = W-min (L~ (Cage (C,n))) by A145, A146, A155, Th21, XBOOLE_1:8;
A157: (W-min ((L~ go) \/ (L~ co))) `1 = W-bound ((L~ go) \/ (L~ co)) by EUCLID:52;
A158: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;
W-bound (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) = ((Gauge (C,n)) * (i,k)) `1 by A78, SPRECT_1:54;
then A159: W-bound (L~ pion1) = ((Gauge (C,n)) * (i,k)) `1 by A81, SPPOL_2:21;
((Gauge (C,n)) * (i,k)) `1 >= W-bound (L~ (Cage (C,n))) by A10, A143, PSCOMP_1:24;
then ((Gauge (C,n)) * (i,k)) `1 > W-bound (L~ (Cage (C,n))) by A74, XXREAL_0:1;
then W-min (((L~ go) \/ (L~ co)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ co)) by A155, A156, A157, A158, A159, Th33;
then A160: W-min (L~ godo) = W-min (L~ (Cage (C,n))) by A141, A156, XBOOLE_1:4;
A161: rng godo c= L~ godo by A87, A89, SPPOL_2:18, XXREAL_0:2;
2 in dom godo by A90, FINSEQ_3:25;
then A162: godo /. 2 in rng godo by PARTFUN2:2;
godo /. 2 in W-most (L~ (Cage (C,n))) by A154, JORDAN1I:25;
then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A160, PSCOMP_1:31
.= W-bound (L~ godo) by EUCLID:52 ;
then godo /. 2 in W-most (L~ godo) by A161, A162, SPRECT_2:12;
then (Rotate (godo,(W-min (L~ godo)))) /. 2 in W-most (L~ godo) by A152, A160, FINSEQ_6:89;
then reconsider godo = godo as constant standard clockwise_oriented special_circular_sequence by JORDAN1I:25;
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by FINSEQ_5:6;
then A163: (Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) by PARTFUN1:def 6
.= E-max (L~ (Cage (C,n))) by JORDAN1F:7 ;
A164: east_halfline (E-max C) misses L~ go

proof

assume east_halfline (E-max C) meets L~ go ; :: thesis:
then consider p being object such that
A165: p in east_halfline (E-max C) and
A166: p in L~ go by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A165;
p in L~ (Upper_Seq (C,n)) by A46, A166;
then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A143, A165, XBOOLE_0:def 4;
then A167: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;
then A168: p = E-max (L~ (Cage (C,n))) by A46, A166, Th46;
then E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,k) by A10, A163, A166, Th43;
then ((Gauge (C,n)) * (i,k)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A5, A13, A16, A167, A168, JORDAN1A:71;
hence contradiction by A2, A15, A30, JORDAN1G:7; :: thesis:

end;

now :: thesis:

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

per cases by A169, XBOOLE_1:70;

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

hence contradiction by A164; :: thesis:

end;

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

then consider p being object such that
A170: p in east_halfline (E-max C) and
A171: p in L~ pion1 by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A170;
A172: p `2 = (E-max C) `2 by A170, TOPREAL1:def 11;
i + 1 <= len (Gauge (C,n)) by A2, NAT_1:13;
then (i + 1) - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:9;
then A173: i <= (len (Gauge (C,n))) -' 1 by XREAL_0:def 2;
A174: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:35;
p `1 = ((Gauge (C,n)) * (i,k)) `1 by A78, A81, A148, A171, GOBOARD7:5;
then p `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A1, A5, A13, A16, A20, A173, A174, JORDAN1A:18;
then p `1 <= E-bound C by A20, JORDAN8:12;
then A175: p `1 <= (E-max C) `1 by EUCLID:52;
p `1 >= (E-max C) `1 by A170, TOPREAL1:def 11;
then p `1 = (E-max C) `1 by A175, XXREAL_0:1;
then p = E-max C by A172, TOPREAL3:6;
hence contradiction by A8, A81, A132, A148, A171, XBOOLE_0:3; :: thesis:

end;

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

now :: thesis:

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

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

then LSeg ((Lower_Seq (C,n)),1) misses LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i,j)) .. (Lower_Seq (C,n)))) -' 1)) by TOPREAL1:def 7;
hence contradiction by A224, A229, A185, A230, XBOOLE_0:3; :: thesis:

end;

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

then 1 + 1 = ((Index (p,co)) + (((Gauge (C,n)) * (i,j)) .. (Lower_Seq (C,n)))) - 1 by XREAL_0:def 2;
then (1 + 1) + 1 = (Index (p,co)) + (((Gauge (C,n)) * (i,j)) .. (Lower_Seq (C,n))) ;
then A234: ((Gauge (C,n)) * (i,j)) .. (Lower_Seq (C,n)) = 2 by A196, A231, JORDAN1E:6;
(LSeg ((Lower_Seq (C,n)),1)) /\ (LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i,j)) .. (Lower_Seq (C,n)))) -' 1))) = {((Lower_Seq (C,n)) /. 2)} by A23, A233, TOPREAL1:def 6;
then p in {((Lower_Seq (C,n)) /. 2)} by A224, A229, A185, A230, XBOOLE_0:def 4;
then A235: p = (Lower_Seq (C,n)) /. 2 by TARSKI:def 1;
then A236: p in rng (Lower_Seq (C,n)) by A190, PARTFUN2:2;
p .. (Lower_Seq (C,n)) = 2 by A190, A235, FINSEQ_5:41;
then p = (Gauge (C,n)) * (i,j) by A37, A234, A236, FINSEQ_5:9;
then ((Gauge (C,n)) * (i,j)) `1 = E-bound (L~ (Cage (C,n))) by A235, JORDAN1G:32;
then ((Gauge (C,n)) * (i,j)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A3, A12, A16, JORDAN1A:71;
hence contradiction by A2, A14, A67, JORDAN1G:7; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then east_halfline (E-max C) c= (L~ godo) ` by SUBSET_1:23;
then consider W being Subset of (TOP-REAL 2) such that
A237: W is_a_component_of (L~ godo) ` and
A238: east_halfline (E-max C) c= W by GOBOARD9:3;
not W is bounded by A238, JORDAN2C:121, RLTOPSP1:42;
then W is_outside_component_of L~ godo by A237, JORDAN2C:def 3;
then W c= UBD (L~ godo) by JORDAN2C:23;
then A239: east_halfline (E-max C) c= UBD (L~ godo) by A238;
E-max C in east_halfline (E-max C) by TOPREAL1:38;
then E-max C in UBD (L~ godo) by A239;
then E-max C in LeftComp godo by GOBRD14:36;
then Lower_Arc C meets L~ godo by A130, A131, A132, A140, A151, Th36;
then A240: ( Lower_Arc C meets (L~ go) \/ (L~ pion1) or Lower_Arc C meets L~ co ) by A141, XBOOLE_1:70;
A241: Lower_Arc C c= C by JORDAN6:61;

per cases by A240, XBOOLE_1:70;

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

then Lower_Arc C meets L~ (Cage (C,n)) by A46, A143, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A241, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;

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

hence contradiction by A8, A81, A148; :: thesis:

end;

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

then Lower_Arc C meets L~ (Cage (C,n)) by A53, A144, XBOOLE_1:1, XBOOLE_1:63;
hence contradiction by A241, JORDAN10:5, XBOOLE_1:63; :: thesis:

end;