let n be Nat; :: thesis: for C being Simple_closed_curve

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

let C be Simple_closed_curve; :: thesis: for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

let i1, i2, j, k be Nat; :: thesis: ( 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} implies (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C )

set G = Gauge (C,n);

set pio = LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)));

set poz = LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)));

set US = Upper_Seq (C,n);

set LS = Lower_Seq (C,n);

assume that

A1: 1 < i1 and

A2: i1 <= i2 and

A3: i2 < len (Gauge (C,n)) and

A4: 1 <= j and

A5: j <= k and

A6: k <= width (Gauge (C,n)) and

A7: ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} and

A8: ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} and

A9: (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) misses Upper_Arc C ; :: thesis: contradiction

set UA = Upper_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 Gik = (Gauge (C,n)) * (i2,k);

set Gij = (Gauge (C,n)) * (i1,j);

set Gi1k = (Gauge (C,n)) * (i1,k);

A10: i1 < len (Gauge (C,n)) by A2, A3, XXREAL_0:2;

A11: 1 < i2 by A1, A2, XXREAL_0:2;

A12: L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> = (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) by TOPREAL3:16;

(Gauge (C,n)) * (i2,k) in {((Gauge (C,n)) * (i2,k))} by TARSKI:def 1;

then A13: (Gauge (C,n)) * (i2,k) in L~ (Lower_Seq (C,n)) by A8, XBOOLE_0:def 4;

(Gauge (C,n)) * (i1,j) in {((Gauge (C,n)) * (i1,j))} by TARSKI:def 1;

then A14: (Gauge (C,n)) * (i1,j) in L~ (Upper_Seq (C,n)) by A7, XBOOLE_0:def 4;

A15: j <= width (Gauge (C,n)) by A5, A6, XXREAL_0:2;

A16: 1 <= k by A4, A5, XXREAL_0:2;

A17: [i1,j] in Indices (Gauge (C,n)) by A1, A4, A10, A15, MATRIX_0:30;

A18: [i2,k] in Indices (Gauge (C,n)) by A3, A6, A11, A16, MATRIX_0:30;

A19: [i1,k] in Indices (Gauge (C,n)) by A1, A6, A10, A16, MATRIX_0:30;

set go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i1,j)));

set co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k)));

A20: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

A21: 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 A22: (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6

.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;

A23: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52

.= ((Gauge (C,n)) * (1,k)) `1 by A6, A16, A20, JORDAN1A:73 ;

len (Gauge (C,n)) >= 4 by JORDAN8:10;

then A24: len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then A25: [1,k] in Indices (Gauge (C,n)) by A6, A16, MATRIX_0:30;

then A26: (Gauge (C,n)) * (i1,j) <> (Upper_Seq (C,n)) . 1 by A1, A17, A22, A23, JORDAN1G:7;

then reconsider go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i1,j))) as being_S-Seq FinSequence of (TOP-REAL 2) by A14, JORDAN3:35;

A27: [1,j] in Indices (Gauge (C,n)) by A4, A15, A24, MATRIX_0:30;

A28: len (Lower_Seq (C,n)) >= 1 + 2 by JORDAN1E:15;

then A29: len (Lower_Seq (C,n)) >= 1 by XXREAL_0:2;

then A30: 1 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;

len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A29, FINSEQ_3:25;

then A31: (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 ;

(W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52

.= ((Gauge (C,n)) * (1,k)) `1 by A6, A16, A20, JORDAN1A:73 ;

then A32: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A1, A2, A18, A25, A31, JORDAN1G:7;

then reconsider co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k))) as being_S-Seq FinSequence of (TOP-REAL 2) by A13, JORDAN3:34;

A33: [(len (Gauge (C,n))),k] in Indices (Gauge (C,n)) by A6, A16, A24, MATRIX_0:30;

A34: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A30, 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 A6, A16, A20, JORDAN1A:71 ;

then A35: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . 1 by A3, A18, A33, A34, JORDAN1G:7;

A36: len go >= 1 + 1 by TOPREAL1:def 8;

A37: (Gauge (C,n)) * (i1,j) in rng (Upper_Seq (C,n)) by A1, A4, A10, A14, A15, JORDAN1G:4, JORDAN1J:40;

then A38: go is_sequence_on Gauge (C,n) by JORDAN1G:4, JORDAN1J:38;

A39: len co >= 1 + 1 by TOPREAL1:def 8;

A40: (Gauge (C,n)) * (i2,k) in rng (Lower_Seq (C,n)) by A3, A6, A11, A13, A16, JORDAN1G:5, JORDAN1J:40;

then A41: co is_sequence_on Gauge (C,n) by JORDAN1G:5, JORDAN1J:39;

reconsider go = go as V26() being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A36, A38, JGRAPH_1:12, JORDAN8:5;

reconsider co = co as V26() being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A39, A41, JGRAPH_1:12, JORDAN8:5;

A42: len go > 1 by A36, NAT_1:13;

then A43: len go in dom go by FINSEQ_3:25;

then A44: go /. (len go) = go . (len go) by PARTFUN1:def 6

.= (Gauge (C,n)) * (i1,j) by A14, JORDAN3:24 ;

len co >= 1 by A39, XXREAL_0:2;

then 1 in dom co by FINSEQ_3:25;

then A45: co /. 1 = co . 1 by PARTFUN1:def 6

.= (Gauge (C,n)) * (i2,k) by A13, JORDAN3:23 ;

reconsider m = (len go) - 1 as Nat by A43, FINSEQ_3:26;

A46: m + 1 = len go ;

then A47: (len go) -' 1 = m by NAT_D:34;

A48: LSeg (go,m) c= L~ go by TOPREAL3:19;

A49: L~ go c= L~ (Upper_Seq (C,n)) by A14, JORDAN3:41;

then LSeg (go,m) c= L~ (Upper_Seq (C,n)) by A48;

then A50: (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) c= {((Gauge (C,n)) * (i1,j))} by A7, A12, XBOOLE_1:26;

m >= 1 by A36, XREAL_1:19;

then A51: LSeg (go,m) = LSeg ((go /. m),((Gauge (C,n)) * (i1,j))) by A44, A46, TOPREAL1:def 3;

{((Gauge (C,n)) * (i1,j))} c= (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

A55: LSeg (co,1) c= L~ co by TOPREAL3:19;

A56: L~ co c= L~ (Lower_Seq (C,n)) by A13, JORDAN3:42;

then LSeg (co,1) c= L~ (Lower_Seq (C,n)) by A55;

then A57: (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) c= {((Gauge (C,n)) * (i2,k))} by A8, A12, XBOOLE_1:26;

A58: LSeg (co,1) = LSeg (((Gauge (C,n)) * (i2,k)),(co /. (1 + 1))) by A39, A45, TOPREAL1:def 3;

{((Gauge (C,n)) * (i2,k))} c= (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

A62: go /. 1 = (Upper_Seq (C,n)) /. 1 by A14, SPRECT_3:22

.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;

then A63: go /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by JORDAN1F:8

.= co /. (len co) by A13, JORDAN1J:35 ;

A64: rng go c= L~ go by A36, SPPOL_2:18;

A65: rng co c= L~ co by A39, SPPOL_2:18;

A66: {(go /. 1)} c= (L~ go) /\ (L~ co)

.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;

A70: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A4, A15, A24, MATRIX_0:30;

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

set W2 = go /. 2;

A77: 2 in dom go by A36, FINSEQ_3:25;

.= (Upper_Seq (C,n)) | (((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n))) by A37, FINSEQ_4:21, FINSEQ_6:116 ;

then A79: go /. 2 = (Upper_Seq (C,n)) /. 2 by A77, FINSEQ_4:70;

A80: W-min (L~ (Cage (C,n))) in rng go by A62, FINSEQ_6:42;

set pion = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>;

.= ((Gauge (C,n)) * (i1,j)) `1 by A1, A4, A10, A15, GOBOARD5:2 ;

((Gauge (C,n)) * (i1,k)) `2 = ((Gauge (C,n)) * (1,k)) `2 by A1, A6, A10, A16, GOBOARD5:1

.= ((Gauge (C,n)) * (i2,k)) `2 by A3, A6, A11, A16, GOBOARD5:1 ;

then A83: (Gauge (C,n)) * (i1,k) = |[(((Gauge (C,n)) * (i1,j)) `1),(((Gauge (C,n)) * (i2,k)) `2)]| by A82, EUCLID:53;

A84: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;

A85: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;

for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

let C be Simple_closed_curve; :: thesis: for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds

(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C

let i1, i2, j, k be Nat; :: thesis: ( 1 < i1 & i1 <= i2 & i2 < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} & ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} implies (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C )

set G = Gauge (C,n);

set pio = LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)));

set poz = LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)));

set US = Upper_Seq (C,n);

set LS = Lower_Seq (C,n);

assume that

A1: 1 < i1 and

A2: i1 <= i2 and

A3: i2 < len (Gauge (C,n)) and

A4: 1 <= j and

A5: j <= k and

A6: k <= width (Gauge (C,n)) and

A7: ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} and

A8: ((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} and

A9: (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) misses Upper_Arc C ; :: thesis: contradiction

set UA = Upper_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 Gik = (Gauge (C,n)) * (i2,k);

set Gij = (Gauge (C,n)) * (i1,j);

set Gi1k = (Gauge (C,n)) * (i1,k);

A10: i1 < len (Gauge (C,n)) by A2, A3, XXREAL_0:2;

A11: 1 < i2 by A1, A2, XXREAL_0:2;

A12: L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> = (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) by TOPREAL3:16;

(Gauge (C,n)) * (i2,k) in {((Gauge (C,n)) * (i2,k))} by TARSKI:def 1;

then A13: (Gauge (C,n)) * (i2,k) in L~ (Lower_Seq (C,n)) by A8, XBOOLE_0:def 4;

(Gauge (C,n)) * (i1,j) in {((Gauge (C,n)) * (i1,j))} by TARSKI:def 1;

then A14: (Gauge (C,n)) * (i1,j) in L~ (Upper_Seq (C,n)) by A7, XBOOLE_0:def 4;

A15: j <= width (Gauge (C,n)) by A5, A6, XXREAL_0:2;

A16: 1 <= k by A4, A5, XXREAL_0:2;

A17: [i1,j] in Indices (Gauge (C,n)) by A1, A4, A10, A15, MATRIX_0:30;

A18: [i2,k] in Indices (Gauge (C,n)) by A3, A6, A11, A16, MATRIX_0:30;

A19: [i1,k] in Indices (Gauge (C,n)) by A1, A6, A10, A16, MATRIX_0:30;

set go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i1,j)));

set co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k)));

A20: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

A21: 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 A22: (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6

.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;

A23: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52

.= ((Gauge (C,n)) * (1,k)) `1 by A6, A16, A20, JORDAN1A:73 ;

len (Gauge (C,n)) >= 4 by JORDAN8:10;

then A24: len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then A25: [1,k] in Indices (Gauge (C,n)) by A6, A16, MATRIX_0:30;

then A26: (Gauge (C,n)) * (i1,j) <> (Upper_Seq (C,n)) . 1 by A1, A17, A22, A23, JORDAN1G:7;

then reconsider go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i1,j))) as being_S-Seq FinSequence of (TOP-REAL 2) by A14, JORDAN3:35;

A27: [1,j] in Indices (Gauge (C,n)) by A4, A15, A24, MATRIX_0:30;

A28: len (Lower_Seq (C,n)) >= 1 + 2 by JORDAN1E:15;

then A29: len (Lower_Seq (C,n)) >= 1 by XXREAL_0:2;

then A30: 1 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;

len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A29, FINSEQ_3:25;

then A31: (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 ;

(W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52

.= ((Gauge (C,n)) * (1,k)) `1 by A6, A16, A20, JORDAN1A:73 ;

then A32: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A1, A2, A18, A25, A31, JORDAN1G:7;

then reconsider co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k))) as being_S-Seq FinSequence of (TOP-REAL 2) by A13, JORDAN3:34;

A33: [(len (Gauge (C,n))),k] in Indices (Gauge (C,n)) by A6, A16, A24, MATRIX_0:30;

A34: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A30, 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 A6, A16, A20, JORDAN1A:71 ;

then A35: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . 1 by A3, A18, A33, A34, JORDAN1G:7;

A36: len go >= 1 + 1 by TOPREAL1:def 8;

A37: (Gauge (C,n)) * (i1,j) in rng (Upper_Seq (C,n)) by A1, A4, A10, A14, A15, JORDAN1G:4, JORDAN1J:40;

then A38: go is_sequence_on Gauge (C,n) by JORDAN1G:4, JORDAN1J:38;

A39: len co >= 1 + 1 by TOPREAL1:def 8;

A40: (Gauge (C,n)) * (i2,k) in rng (Lower_Seq (C,n)) by A3, A6, A11, A13, A16, JORDAN1G:5, JORDAN1J:40;

then A41: co is_sequence_on Gauge (C,n) by JORDAN1G:5, JORDAN1J:39;

reconsider go = go as V26() being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A36, A38, JGRAPH_1:12, JORDAN8:5;

reconsider co = co as V26() being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A39, A41, JGRAPH_1:12, JORDAN8:5;

A42: len go > 1 by A36, NAT_1:13;

then A43: len go in dom go by FINSEQ_3:25;

then A44: go /. (len go) = go . (len go) by PARTFUN1:def 6

.= (Gauge (C,n)) * (i1,j) by A14, JORDAN3:24 ;

len co >= 1 by A39, XXREAL_0:2;

then 1 in dom co by FINSEQ_3:25;

then A45: co /. 1 = co . 1 by PARTFUN1:def 6

.= (Gauge (C,n)) * (i2,k) by A13, JORDAN3:23 ;

reconsider m = (len go) - 1 as Nat by A43, FINSEQ_3:26;

A46: m + 1 = len go ;

then A47: (len go) -' 1 = m by NAT_D:34;

A48: LSeg (go,m) c= L~ go by TOPREAL3:19;

A49: L~ go c= L~ (Upper_Seq (C,n)) by A14, JORDAN3:41;

then LSeg (go,m) c= L~ (Upper_Seq (C,n)) by A48;

then A50: (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) c= {((Gauge (C,n)) * (i1,j))} by A7, A12, XBOOLE_1:26;

m >= 1 by A36, XREAL_1:19;

then A51: LSeg (go,m) = LSeg ((go /. m),((Gauge (C,n)) * (i1,j))) by A44, A46, TOPREAL1:def 3;

{((Gauge (C,n)) * (i1,j))} c= (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

proof

then A54:
(LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) = {((Gauge (C,n)) * (i1,j))}
by A50;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,n)) * (i1,j))} or x in (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) )

assume x in {((Gauge (C,n)) * (i1,j))} ; :: thesis: x in (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

then A52: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;

A53: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A51, RLTOPSP1:68;

(Gauge (C,n)) * (i1,j) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;

then (Gauge (C,n)) * (i1,j) in (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) by XBOOLE_0:def 3;

then (Gauge (C,n)) * (i1,j) in L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by SPRECT_1:8;

hence x in (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A52, A53, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {((Gauge (C,n)) * (i1,j))} ; :: thesis: x in (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

then A52: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;

A53: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A51, RLTOPSP1:68;

(Gauge (C,n)) * (i1,j) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;

then (Gauge (C,n)) * (i1,j) in (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) by XBOOLE_0:def 3;

then (Gauge (C,n)) * (i1,j) in L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by SPRECT_1:8;

hence x in (LSeg (go,m)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A52, A53, XBOOLE_0:def 4; :: thesis: verum

A55: LSeg (co,1) c= L~ co by TOPREAL3:19;

A56: L~ co c= L~ (Lower_Seq (C,n)) by A13, JORDAN3:42;

then LSeg (co,1) c= L~ (Lower_Seq (C,n)) by A55;

then A57: (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) c= {((Gauge (C,n)) * (i2,k))} by A8, A12, XBOOLE_1:26;

A58: LSeg (co,1) = LSeg (((Gauge (C,n)) * (i2,k)),(co /. (1 + 1))) by A39, A45, TOPREAL1:def 3;

{((Gauge (C,n)) * (i2,k))} c= (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

proof

then A61:
(L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) /\ (LSeg (co,1)) = {((Gauge (C,n)) * (i2,k))}
by A57;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,n)) * (i2,k))} or x in (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) )

assume x in {((Gauge (C,n)) * (i2,k))} ; :: thesis: x in (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

then A59: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;

A60: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A58, RLTOPSP1:68;

(Gauge (C,n)) * (i2,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;

then (Gauge (C,n)) * (i2,k) in (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) by XBOOLE_0:def 3;

then (Gauge (C,n)) * (i2,k) in L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by SPRECT_1:8;

hence x in (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A59, A60, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {((Gauge (C,n)) * (i2,k))} ; :: thesis: x in (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>)

then A59: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;

A60: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A58, RLTOPSP1:68;

(Gauge (C,n)) * (i2,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;

then (Gauge (C,n)) * (i2,k) in (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) by XBOOLE_0:def 3;

then (Gauge (C,n)) * (i2,k) in L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by SPRECT_1:8;

hence x in (LSeg (co,1)) /\ (L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A59, A60, XBOOLE_0:def 4; :: thesis: verum

A62: go /. 1 = (Upper_Seq (C,n)) /. 1 by A14, SPRECT_3:22

.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;

then A63: go /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by JORDAN1F:8

.= co /. (len co) by A13, JORDAN1J:35 ;

A64: rng go c= L~ go by A36, SPPOL_2:18;

A65: rng co c= L~ co by A39, SPPOL_2:18;

A66: {(go /. 1)} c= (L~ go) /\ (L~ co)

proof

A69: (Lower_Seq (C,n)) . 1 =
(Lower_Seq (C,n)) /. 1
by A30, PARTFUN1:def 6
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(go /. 1)} or x in (L~ go) /\ (L~ co) )

assume x in {(go /. 1)} ; :: thesis: x in (L~ go) /\ (L~ co)

then A67: x = go /. 1 by TARSKI:def 1;

then A68: x in rng go by FINSEQ_6:42;

x in rng co by A63, A67, FINSEQ_6:168;

hence x in (L~ go) /\ (L~ co) by A64, A65, A68, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {(go /. 1)} ; :: thesis: x in (L~ go) /\ (L~ co)

then A67: x = go /. 1 by TARSKI:def 1;

then A68: x in rng go by FINSEQ_6:42;

x in rng co by A63, A67, FINSEQ_6:168;

hence x in (L~ go) /\ (L~ co) by A64, A65, A68, XBOOLE_0:def 4; :: thesis: verum

.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;

A70: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A4, A15, A24, MATRIX_0:30;

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

proof

then A76:
(L~ go) /\ (L~ co) = {(go /. 1)}
by A66;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ go) /\ (L~ co) or x in {(go /. 1)} )

assume A71: x in (L~ go) /\ (L~ co) ; :: thesis: x in {(go /. 1)}

then A72: x in L~ go by XBOOLE_0:def 4;

A73: x in L~ co by A71, XBOOLE_0:def 4;

then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A49, A56, A72, XBOOLE_0:def 4;

then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

then A74: ( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) ) by TARSKI:def 2;

end;assume A71: x in (L~ go) /\ (L~ co) ; :: thesis: x in {(go /. 1)}

then A72: x in L~ go by XBOOLE_0:def 4;

A73: x in L~ co by A71, XBOOLE_0:def 4;

then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A49, A56, A72, XBOOLE_0:def 4;

then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

then A74: ( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) ) by TARSKI:def 2;

now :: thesis: not x = E-max (L~ (Cage (C,n)))

hence
x in {(go /. 1)}
by A62, A74, TARSKI:def 1; :: thesis: verumassume
x = E-max (L~ (Cage (C,n)))
; :: thesis: contradiction

then A75: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i2,k) by A13, A69, A73, JORDAN1E:7;

((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = E-bound (L~ (Cage (C,n))) by A4, A15, A20, JORDAN1A:71;

then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A3, A18, A70, A75, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum

end;then A75: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i2,k) by A13, A69, A73, JORDAN1E:7;

((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = E-bound (L~ (Cage (C,n))) by A4, A15, A20, JORDAN1A:71;

then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A3, A18, A70, A75, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum

set W2 = go /. 2;

A77: 2 in dom go by A36, FINSEQ_3:25;

A78: now :: thesis: not ((Gauge (C,n)) * (i1,j)) `1 = W-bound (L~ (Cage (C,n)))

go =
mid ((Upper_Seq (C,n)),1,(((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n))))
by A37, JORDAN1G:49
assume
((Gauge (C,n)) * (i1,j)) `1 = W-bound (L~ (Cage (C,n)))
; :: thesis: contradiction

then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (i1,j)) `1 by A4, A15, A20, JORDAN1A:73;

hence contradiction by A1, A17, A27, JORDAN1G:7; :: thesis: verum

end;then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (i1,j)) `1 by A4, A15, A20, JORDAN1A:73;

hence contradiction by A1, A17, A27, JORDAN1G:7; :: thesis: verum

.= (Upper_Seq (C,n)) | (((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n))) by A37, FINSEQ_4:21, FINSEQ_6:116 ;

then A79: go /. 2 = (Upper_Seq (C,n)) /. 2 by A77, FINSEQ_4:70;

A80: W-min (L~ (Cage (C,n))) in rng go by A62, FINSEQ_6:42;

set pion = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>;

A81: now :: thesis: for n being Nat st n in dom <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> holds

ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) )

A82: ((Gauge (C,n)) * (i1,k)) `1 =
((Gauge (C,n)) * (i1,1)) `1
by A1, A6, A10, A16, GOBOARD5:2
ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) )

let n be Nat; :: thesis: ( n in dom <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> implies ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) ) )

assume n in dom <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> ; :: thesis: ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) )

then n in {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;

then ( n = 1 or n = 2 or n = 3 ) by ENUMSET1:def 1;

hence ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) ) by A17, A18, A19, FINSEQ_4:18; :: thesis: verum

end;( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) ) )

assume n in dom <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> ; :: thesis: ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) )

then n in {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;

then ( n = 1 or n = 2 or n = 3 ) by ENUMSET1:def 1;

hence ex i, j being Nat st

( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. n = (Gauge (C,n)) * (i,j) ) by A17, A18, A19, FINSEQ_4:18; :: thesis: verum

.= ((Gauge (C,n)) * (i1,j)) `1 by A1, A4, A10, A15, GOBOARD5:2 ;

((Gauge (C,n)) * (i1,k)) `2 = ((Gauge (C,n)) * (1,k)) `2 by A1, A6, A10, A16, GOBOARD5:1

.= ((Gauge (C,n)) * (i2,k)) `2 by A3, A6, A11, A16, GOBOARD5:1 ;

then A83: (Gauge (C,n)) * (i1,k) = |[(((Gauge (C,n)) * (i1,j)) `1),(((Gauge (C,n)) * (i2,k)) `2)]| by A82, EUCLID:53;

A84: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;

A85: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ( ((Gauge (C,n)) * (i2,k)) `1 <> ((Gauge (C,n)) * (i1,j)) `1 & ((Gauge (C,n)) * (i2,k)) `2 <> ((Gauge (C,n)) * (i1,j)) `2 ) or ((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * (i1,j)) `1 or ((Gauge (C,n)) * (i2,k)) `2 = ((Gauge (C,n)) * (i1,j)) `2 )
;

end;

suppose
( ((Gauge (C,n)) * (i2,k)) `1 <> ((Gauge (C,n)) * (i1,j)) `1 & ((Gauge (C,n)) * (i2,k)) `2 <> ((Gauge (C,n)) * (i1,j)) `2 )
; :: thesis: contradiction

then
<*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> is being_S-Seq
by A83, TOPREAL3:34;

then consider pion1 being FinSequence of (TOP-REAL 2) such that

A86: pion1 is_sequence_on Gauge (C,n) and

A87: pion1 is being_S-Seq and

A88: L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> = L~ pion1 and

A89: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 1 = pion1 /. 1 and

A90: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) = pion1 /. (len pion1) and

A91: len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> <= len pion1 by A81, GOBOARD3:2;

reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A87;

set godo = (go ^' pion1) ^' co;

A92: ((Gauge (C,n)) * (i1,k)) `1 = ((Gauge (C,n)) * (i1,1)) `1 by A1, A6, A10, A16, GOBOARD5:2

.= ((Gauge (C,n)) * (i1,j)) `1 by A1, A4, A10, A15, GOBOARD5:2 ;

A93: ((Gauge (C,n)) * (i1,k)) `1 <= ((Gauge (C,n)) * (i2,k)) `1 by A1, A2, A3, A6, A16, JORDAN1A:18;

then A94: W-bound (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = ((Gauge (C,n)) * (i1,k)) `1 by SPRECT_1:54;

A95: W-bound (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) = ((Gauge (C,n)) * (i1,j)) `1 by A92, SPRECT_1:54;

W-bound ((LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))))) = min ((W-bound (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))),(W-bound (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))))) by SPRECT_1:47

.= ((Gauge (C,n)) * (i1,j)) `1 by A92, A94, A95 ;

then A96: W-bound (L~ pion1) = ((Gauge (C,n)) * (i1,j)) `1 by A88, TOPREAL3:16;

A97: 1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;

A98: 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 A99: len (go ^' pion1) >= 1 + 1 by A36, XXREAL_0:2;

then A100: len (go ^' pion1) > 1 + 0 by NAT_1:13;

A101: len ((go ^' pion1) ^' co) >= len (go ^' pion1) by TOPREAL8:7;

then A102: 1 + 1 <= len ((go ^' pion1) ^' co) by A99, XXREAL_0:2;

A103: Upper_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1G:4;

A104: go /. (len go) = pion1 /. 1 by A44, A89, FINSEQ_4:18;

then A105: go ^' pion1 is_sequence_on Gauge (C,n) by A38, A86, TOPREAL8:12;

A106: (go ^' pion1) /. (len (go ^' pion1)) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A90, FINSEQ_6:156

.= <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by FINSEQ_1:45

.= co /. 1 by A45, FINSEQ_4:18 ;

then A107: (go ^' pion1) ^' co is_sequence_on Gauge (C,n) by A41, A105, TOPREAL8:12;

LSeg (pion1,1) c= L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by A88, TOPREAL3:19;

then A108: (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) c= {((Gauge (C,n)) * (i1,j))} by A47, A54, XBOOLE_1:27;

len pion1 >= 2 + 1 by A91, FINSEQ_1:45;

then A109: len pion1 > 1 + 1 by NAT_1:13;

{((Gauge (C,n)) * (i1,j))} c= (LSeg (go,m)) /\ (LSeg (pion1,1))

then A112: go ^' pion1 is unfolded by A104, TOPREAL8:34;

len pion1 >= 2 + 1 by A91, FINSEQ_1:45;

then A113: (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 A113, XREAL_0:def 2 ;

then A114: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;

A115: (len pion1) - 1 >= 1 by A109, XREAL_1:19;

then A116: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;

A117: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A113, XREAL_0:def 2

.= (len pion1) -' 1 by A115, XREAL_0:def 2 ;

((len pion1) - 1) + 1 <= len pion1 ;

then A118: (len pion1) -' 1 < len pion1 by A116, NAT_1:13;

LSeg (pion1,((len pion1) -' 1)) c= L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by A88, TOPREAL3:19;

then A119: (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) c= {((Gauge (C,n)) * (i2,k))} by A61, XBOOLE_1:27;

{((Gauge (C,n)) * (i2,k))} c= (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))

then A122: (LSeg ((go ^' pion1),((len go) + ((len pion1) -' 2)))) /\ (LSeg (co,1)) = {((go ^' pion1) /. (len (go ^' pion1)))} by A45, A104, A106, A117, A118, TOPREAL8:31;

A123: not go ^' pion1 is trivial by A99, NAT_D:60;

A124: rng pion1 c= L~ pion1 by A109, SPPOL_2:18;

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

then A131: go ^' pion1 is s.n.c. by A104, JORDAN1J:54;

(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A64, A124, A130, XBOOLE_1:27;

then A132: go ^' pion1 is one-to-one by JORDAN1J:55;

A133: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by FINSEQ_1:45

.= co /. 1 by A45, FINSEQ_4:18 ;

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

A140: (L~ (go ^' pion1)) /\ (L~ co) = ((L~ go) \/ (L~ pion1)) /\ (L~ co) by A104, TOPREAL8:35

.= {(go /. 1)} \/ {(co /. 1)} by A76, A90, A133, A139, XBOOLE_1:23

.= {((go ^' pion1) /. 1)} \/ {(co /. 1)} by FINSEQ_6:155

.= {((go ^' pion1) /. 1),(co /. 1)} by ENUMSET1:1 ;

co /. (len co) = (go ^' pion1) /. 1 by A63, FINSEQ_6:155;

then reconsider godo = (go ^' pion1) ^' co as V26() standard special_circular_sequence by A102, A106, A107, A112, A114, A122, A123, A131, A132, A140, JORDAN8:4, JORDAN8:5, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;

A141: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def 8;

then A142: Upper_Arc C is connected by JORDAN6:10;

A143: W-min C in Upper_Arc C by A141, TOPREAL1:1;

A144: E-max C in Upper_Arc C by A141, TOPREAL1:1;

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:43;

then A145: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

A146: 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 A145, SPRECT_5:22;

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 A145, A146, SPRECT_5:23, 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 A145, A146, SPRECT_5:24, XXREAL_0:2;

then A147: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A145, A146, SPRECT_5:25, XXREAL_0:2;

then A151: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;

A152: (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) c= RightComp godo by A102, A107, JORDAN9:27;

A153: L~ godo = (L~ (go ^' pion1)) \/ (L~ co) by A106, TOPREAL8:35

.= ((L~ go) \/ (L~ pion1)) \/ (L~ co) by A104, TOPREAL8:35 ;

A154: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:13;

then A155: L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n)) by XBOOLE_1:7;

A156: L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n)) by A154, XBOOLE_1:7;

A157: L~ go c= L~ (Cage (C,n)) by A49, A155;

A158: L~ co c= L~ (Cage (C,n)) by A56, A156;

A159: W-min C in C by SPRECT_1:13;

.= 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 A147, A151, 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)) * (i1,j)))),1,(Gauge (C,n))) by A37, A103, A148, JORDAN1J:52

.= right_cell ((go ^' pion1),1,(Gauge (C,n))) by A42, A105, JORDAN1J:51

.= right_cell (godo,1,(Gauge (C,n))) by A100, A107, JORDAN1J:51 ;

then W-min C in right_cell (godo,1,(Gauge (C,n))) by JORDAN1I:6;

then A162: W-min C in (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) by A160, XBOOLE_0:def 5;

A163: godo /. 1 = (go ^' pion1) /. 1 by FINSEQ_6:155

.= W-min (L~ (Cage (C,n))) by A62, FINSEQ_6:155 ;

A164: len (Upper_Seq (C,n)) >= 2 by A21, XXREAL_0:2;

A165: godo /. 2 = (go ^' pion1) /. 2 by A99, FINSEQ_6:159

.= (Upper_Seq (C,n)) /. 2 by A36, A79, FINSEQ_6:159

.= ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) /. 2 by A164, FINSEQ_6:159

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 2 by JORDAN1E:11 ;

A166: (L~ go) \/ (L~ co) is compact by COMPTS_1:10;

W-min (L~ (Cage (C,n))) in (L~ go) \/ (L~ co) by A64, A80, XBOOLE_0:def 3;

then A167: W-min ((L~ go) \/ (L~ co)) = W-min (L~ (Cage (C,n))) by A157, A158, A166, JORDAN1J:21, XBOOLE_1:8;

A168: (W-min ((L~ go) \/ (L~ co))) `1 = W-bound ((L~ go) \/ (L~ co)) by EUCLID:52;

A169: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;

((Gauge (C,n)) * (i1,j)) `1 >= W-bound (L~ (Cage (C,n))) by A14, A155, PSCOMP_1:24;

then ((Gauge (C,n)) * (i1,j)) `1 > W-bound (L~ (Cage (C,n))) by A78, XXREAL_0:1;

then W-min (((L~ go) \/ (L~ co)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ co)) by A96, A166, A167, A168, A169, JORDAN1J:33;

then A170: W-min (L~ godo) = W-min (L~ (Cage (C,n))) by A153, A167, XBOOLE_1:4;

A171: rng godo c= L~ godo by A99, A101, SPPOL_2:18, XXREAL_0:2;

2 in dom godo by A102, FINSEQ_3:25;

then A172: godo /. 2 in rng godo by PARTFUN2:2;

godo /. 2 in W-most (L~ (Cage (C,n))) by A165, JORDAN1I:25;

then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A170, PSCOMP_1:31

.= W-bound (L~ godo) by EUCLID:52 ;

then godo /. 2 in W-most (L~ godo) by A171, A172, SPRECT_2:12;

then (Rotate (godo,(W-min (L~ godo)))) /. 2 in W-most (L~ godo) by A163, A170, FINSEQ_6:89;

then reconsider godo = godo as V26() 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 A173: (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 ;

A174: east_halfline (E-max C) misses L~ go

then consider W being Subset of (TOP-REAL 2) such that

A251: W is_a_component_of (L~ godo) ` and

A252: east_halfline (E-max C) c= W by GOBOARD9:3;

not W is bounded by A252, JORDAN2C:121, RLTOPSP1:42;

then W is_outside_component_of L~ godo by A251, JORDAN2C:def 3;

then W c= UBD (L~ godo) by JORDAN2C:23;

then A253: east_halfline (E-max C) c= UBD (L~ godo) by A252;

E-max C in east_halfline (E-max C) by TOPREAL1:38;

then E-max C in UBD (L~ godo) by A253;

then E-max C in LeftComp godo by GOBRD14:36;

then Upper_Arc C meets L~ godo by A142, A143, A144, A152, A162, JORDAN1J:36;

then A254: ( Upper_Arc C meets (L~ go) \/ (L~ pion1) or Upper_Arc C meets L~ co ) by A153, XBOOLE_1:70;

A255: Upper_Arc C c= C by JORDAN6:61;

end;then consider pion1 being FinSequence of (TOP-REAL 2) such that

A86: pion1 is_sequence_on Gauge (C,n) and

A87: pion1 is being_S-Seq and

A88: L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> = L~ pion1 and

A89: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 1 = pion1 /. 1 and

A90: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) = pion1 /. (len pion1) and

A91: len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> <= len pion1 by A81, GOBOARD3:2;

reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A87;

set godo = (go ^' pion1) ^' co;

A92: ((Gauge (C,n)) * (i1,k)) `1 = ((Gauge (C,n)) * (i1,1)) `1 by A1, A6, A10, A16, GOBOARD5:2

.= ((Gauge (C,n)) * (i1,j)) `1 by A1, A4, A10, A15, GOBOARD5:2 ;

A93: ((Gauge (C,n)) * (i1,k)) `1 <= ((Gauge (C,n)) * (i2,k)) `1 by A1, A2, A3, A6, A16, JORDAN1A:18;

then A94: W-bound (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = ((Gauge (C,n)) * (i1,k)) `1 by SPRECT_1:54;

A95: W-bound (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) = ((Gauge (C,n)) * (i1,j)) `1 by A92, SPRECT_1:54;

W-bound ((LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))))) = min ((W-bound (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))),(W-bound (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))))) by SPRECT_1:47

.= ((Gauge (C,n)) * (i1,j)) `1 by A92, A94, A95 ;

then A96: W-bound (L~ pion1) = ((Gauge (C,n)) * (i1,j)) `1 by A88, TOPREAL3:16;

A97: 1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;

A98: 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 A99: len (go ^' pion1) >= 1 + 1 by A36, XXREAL_0:2;

then A100: len (go ^' pion1) > 1 + 0 by NAT_1:13;

A101: len ((go ^' pion1) ^' co) >= len (go ^' pion1) by TOPREAL8:7;

then A102: 1 + 1 <= len ((go ^' pion1) ^' co) by A99, XXREAL_0:2;

A103: Upper_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1G:4;

A104: go /. (len go) = pion1 /. 1 by A44, A89, FINSEQ_4:18;

then A105: go ^' pion1 is_sequence_on Gauge (C,n) by A38, A86, TOPREAL8:12;

A106: (go ^' pion1) /. (len (go ^' pion1)) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) by A90, FINSEQ_6:156

.= <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by FINSEQ_1:45

.= co /. 1 by A45, FINSEQ_4:18 ;

then A107: (go ^' pion1) ^' co is_sequence_on Gauge (C,n) by A41, A105, TOPREAL8:12;

LSeg (pion1,1) c= L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by A88, TOPREAL3:19;

then A108: (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) c= {((Gauge (C,n)) * (i1,j))} by A47, A54, XBOOLE_1:27;

len pion1 >= 2 + 1 by A91, FINSEQ_1:45;

then A109: len pion1 > 1 + 1 by NAT_1:13;

{((Gauge (C,n)) * (i1,j))} c= (LSeg (go,m)) /\ (LSeg (pion1,1))

proof

then
(LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) = {(go /. (len go))}
by A44, A47, A108;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,n)) * (i1,j))} or x in (LSeg (go,m)) /\ (LSeg (pion1,1)) )

assume x in {((Gauge (C,n)) * (i1,j))} ; :: thesis: x in (LSeg (go,m)) /\ (LSeg (pion1,1))

then A110: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;

A111: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A51, RLTOPSP1:68;

(Gauge (C,n)) * (i1,j) in LSeg (pion1,1) by A44, A104, A109, TOPREAL1:21;

hence x in (LSeg (go,m)) /\ (LSeg (pion1,1)) by A110, A111, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {((Gauge (C,n)) * (i1,j))} ; :: thesis: x in (LSeg (go,m)) /\ (LSeg (pion1,1))

then A110: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;

A111: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A51, RLTOPSP1:68;

(Gauge (C,n)) * (i1,j) in LSeg (pion1,1) by A44, A104, A109, TOPREAL1:21;

hence x in (LSeg (go,m)) /\ (LSeg (pion1,1)) by A110, A111, XBOOLE_0:def 4; :: thesis: verum

then A112: go ^' pion1 is unfolded by A104, TOPREAL8:34;

len pion1 >= 2 + 1 by A91, FINSEQ_1:45;

then A113: (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 A113, XREAL_0:def 2 ;

then A114: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;

A115: (len pion1) - 1 >= 1 by A109, XREAL_1:19;

then A116: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;

A117: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A113, XREAL_0:def 2

.= (len pion1) -' 1 by A115, XREAL_0:def 2 ;

((len pion1) - 1) + 1 <= len pion1 ;

then A118: (len pion1) -' 1 < len pion1 by A116, NAT_1:13;

LSeg (pion1,((len pion1) -' 1)) c= L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by A88, TOPREAL3:19;

then A119: (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) c= {((Gauge (C,n)) * (i2,k))} by A61, XBOOLE_1:27;

{((Gauge (C,n)) * (i2,k))} c= (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))

proof

then
(LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) = {((Gauge (C,n)) * (i2,k))}
by A119;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,n)) * (i2,k))} or x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) )

assume x in {((Gauge (C,n)) * (i2,k))} ; :: thesis: x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))

then A120: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;

A121: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A58, RLTOPSP1:68;

pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by A90, A116, FINSEQ_1:45

.= (Gauge (C,n)) * (i2,k) by FINSEQ_4:18 ;

then (Gauge (C,n)) * (i2,k) in LSeg (pion1,((len pion1) -' 1)) by A115, A116, TOPREAL1:21;

hence x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) by A120, A121, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {((Gauge (C,n)) * (i2,k))} ; :: thesis: x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))

then A120: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;

A121: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A58, RLTOPSP1:68;

pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by A90, A116, FINSEQ_1:45

.= (Gauge (C,n)) * (i2,k) by FINSEQ_4:18 ;

then (Gauge (C,n)) * (i2,k) in LSeg (pion1,((len pion1) -' 1)) by A115, A116, TOPREAL1:21;

hence x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) by A120, A121, XBOOLE_0:def 4; :: thesis: verum

then A122: (LSeg ((go ^' pion1),((len go) + ((len pion1) -' 2)))) /\ (LSeg (co,1)) = {((go ^' pion1) /. (len (go ^' pion1)))} by A45, A104, A106, A117, A118, TOPREAL8:31;

A123: not go ^' pion1 is trivial by A99, NAT_D:60;

A124: rng pion1 c= L~ pion1 by A109, SPPOL_2:18;

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

proof

(L~ go) /\ (L~ pion1) c= {(pion1 /. 1)}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(pion1 /. 1)} or x in (L~ go) /\ (L~ pion1) )

assume x in {(pion1 /. 1)} ; :: thesis: x in (L~ go) /\ (L~ pion1)

then A126: x = pion1 /. 1 by TARSKI:def 1;

then A127: x in rng go by A104, FINSEQ_6:168;

x in rng pion1 by A126, FINSEQ_6:42;

hence x in (L~ go) /\ (L~ pion1) by A64, A124, A127, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {(pion1 /. 1)} ; :: thesis: x in (L~ go) /\ (L~ pion1)

then A126: x = pion1 /. 1 by TARSKI:def 1;

then A127: x in rng go by A104, FINSEQ_6:168;

x in rng pion1 by A126, FINSEQ_6:42;

hence x in (L~ go) /\ (L~ pion1) by A64, A124, A127, XBOOLE_0:def 4; :: thesis: verum

proof

then A130:
(L~ go) /\ (L~ pion1) = {(pion1 /. 1)}
by A125;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ go) /\ (L~ pion1) or x in {(pion1 /. 1)} )

assume A128: x in (L~ go) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. 1)}

then A129: x in L~ go by XBOOLE_0:def 4;

x in L~ pion1 by A128, XBOOLE_0:def 4;

hence x in {(pion1 /. 1)} by A7, A12, A44, A49, A88, A104, A129, XBOOLE_0:def 4; :: thesis: verum

end;assume A128: x in (L~ go) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. 1)}

then A129: x in L~ go by XBOOLE_0:def 4;

x in L~ pion1 by A128, XBOOLE_0:def 4;

hence x in {(pion1 /. 1)} by A7, A12, A44, A49, A88, A104, A129, XBOOLE_0:def 4; :: thesis: verum

then A131: go ^' pion1 is s.n.c. by A104, JORDAN1J:54;

(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A64, A124, A130, XBOOLE_1:27;

then A132: go ^' pion1 is one-to-one by JORDAN1J:55;

A133: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. (len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by FINSEQ_1:45

.= co /. 1 by A45, FINSEQ_4:18 ;

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

proof

(L~ co) /\ (L~ pion1) c= {(pion1 /. (len pion1))}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(pion1 /. (len pion1))} or x in (L~ co) /\ (L~ pion1) )

assume x in {(pion1 /. (len pion1))} ; :: thesis: x in (L~ co) /\ (L~ pion1)

then A135: x = pion1 /. (len pion1) by TARSKI:def 1;

then A136: x in rng co by A90, A133, FINSEQ_6:42;

x in rng pion1 by A135, FINSEQ_6:168;

hence x in (L~ co) /\ (L~ pion1) by A65, A124, A136, XBOOLE_0:def 4; :: thesis: verum

end;assume x in {(pion1 /. (len pion1))} ; :: thesis: x in (L~ co) /\ (L~ pion1)

then A135: x = pion1 /. (len pion1) by TARSKI:def 1;

then A136: x in rng co by A90, A133, FINSEQ_6:42;

x in rng pion1 by A135, FINSEQ_6:168;

hence x in (L~ co) /\ (L~ pion1) by A65, A124, A136, XBOOLE_0:def 4; :: thesis: verum

proof

then A139:
(L~ co) /\ (L~ pion1) = {(pion1 /. (len pion1))}
by A134;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ co) /\ (L~ pion1) or x in {(pion1 /. (len pion1))} )

assume A137: x in (L~ co) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. (len pion1))}

then A138: x in L~ co by XBOOLE_0:def 4;

x in L~ pion1 by A137, XBOOLE_0:def 4;

hence x in {(pion1 /. (len pion1))} by A8, A12, A45, A56, A88, A90, A133, A138, XBOOLE_0:def 4; :: thesis: verum

end;assume A137: x in (L~ co) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. (len pion1))}

then A138: x in L~ co by XBOOLE_0:def 4;

x in L~ pion1 by A137, XBOOLE_0:def 4;

hence x in {(pion1 /. (len pion1))} by A8, A12, A45, A56, A88, A90, A133, A138, XBOOLE_0:def 4; :: thesis: verum

A140: (L~ (go ^' pion1)) /\ (L~ co) = ((L~ go) \/ (L~ pion1)) /\ (L~ co) by A104, TOPREAL8:35

.= {(go /. 1)} \/ {(co /. 1)} by A76, A90, A133, A139, XBOOLE_1:23

.= {((go ^' pion1) /. 1)} \/ {(co /. 1)} by FINSEQ_6:155

.= {((go ^' pion1) /. 1),(co /. 1)} by ENUMSET1:1 ;

co /. (len co) = (go ^' pion1) /. 1 by A63, FINSEQ_6:155;

then reconsider godo = (go ^' pion1) ^' co as V26() standard special_circular_sequence by A102, A106, A107, A112, A114, A122, A123, A131, A132, A140, JORDAN8:4, JORDAN8:5, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;

A141: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def 8;

then A142: Upper_Arc C is connected by JORDAN6:10;

A143: W-min C in Upper_Arc C by A141, TOPREAL1:1;

A144: E-max C in Upper_Arc C by A141, TOPREAL1:1;

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:43;

then A145: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;

A146: 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 A145, SPRECT_5:22;

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 A145, A146, SPRECT_5:23, 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 A145, A146, SPRECT_5:24, XXREAL_0:2;

then A147: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A145, A146, SPRECT_5:25, XXREAL_0:2;

A148: now :: thesis: not ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1

A150:
Cage (C,n) is_sequence_on Gauge (C,n)
by JORDAN9:def 1;assume A149:
((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1
; :: thesis: contradiction

((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) >= 1 by A37, FINSEQ_4:21;

then ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) = 1 by A149, XXREAL_0:1;

then (Gauge (C,n)) * (i1,j) = (Upper_Seq (C,n)) /. 1 by A37, FINSEQ_5:38;

hence contradiction by A22, A26, JORDAN1F:5; :: thesis: verum

end;((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) >= 1 by A37, FINSEQ_4:21;

then ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) = 1 by A149, XXREAL_0:1;

then (Gauge (C,n)) * (i1,j) = (Upper_Seq (C,n)) /. 1 by A37, FINSEQ_5:38;

hence contradiction by A22, A26, JORDAN1F:5; :: thesis: verum

then A151: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;

A152: (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) c= RightComp godo by A102, A107, JORDAN9:27;

A153: L~ godo = (L~ (go ^' pion1)) \/ (L~ co) by A106, TOPREAL8:35

.= ((L~ go) \/ (L~ pion1)) \/ (L~ co) by A104, TOPREAL8:35 ;

A154: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:13;

then A155: L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n)) by XBOOLE_1:7;

A156: L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n)) by A154, XBOOLE_1:7;

A157: L~ go c= L~ (Cage (C,n)) by A49, A155;

A158: L~ co c= L~ (Cage (C,n)) by A56, A156;

A159: W-min C in C by SPRECT_1:13;

A160: now :: thesis: not W-min C in L~ godo

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 A98, JORDAN1H:23
assume
W-min C in L~ godo
; :: thesis: contradiction

then A161: ( W-min C in (L~ go) \/ (L~ pion1) or W-min C in L~ co ) by A153, XBOOLE_0:def 3;

end;then A161: ( W-min C in (L~ go) \/ (L~ pion1) or W-min C in L~ co ) by A153, XBOOLE_0:def 3;

per cases
( W-min C in L~ go or W-min C in L~ pion1 or W-min C in L~ co )
by A161, XBOOLE_0:def 3;

end;

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

then
C meets L~ (Cage (C,n))
by A157, A159, XBOOLE_0:3;

hence contradiction by JORDAN10:5; :: thesis: verum

end;hence contradiction by JORDAN10:5; :: thesis: verum

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

then
C meets L~ (Cage (C,n))
by A158, A159, XBOOLE_0:3;

hence contradiction by JORDAN10:5; :: thesis: verum

end;hence contradiction by JORDAN10:5; :: thesis: verum

.= 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 A147, A151, 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)) * (i1,j)))),1,(Gauge (C,n))) by A37, A103, A148, JORDAN1J:52

.= right_cell ((go ^' pion1),1,(Gauge (C,n))) by A42, A105, JORDAN1J:51

.= right_cell (godo,1,(Gauge (C,n))) by A100, A107, JORDAN1J:51 ;

then W-min C in right_cell (godo,1,(Gauge (C,n))) by JORDAN1I:6;

then A162: W-min C in (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) by A160, XBOOLE_0:def 5;

A163: godo /. 1 = (go ^' pion1) /. 1 by FINSEQ_6:155

.= W-min (L~ (Cage (C,n))) by A62, FINSEQ_6:155 ;

A164: len (Upper_Seq (C,n)) >= 2 by A21, XXREAL_0:2;

A165: godo /. 2 = (go ^' pion1) /. 2 by A99, FINSEQ_6:159

.= (Upper_Seq (C,n)) /. 2 by A36, A79, FINSEQ_6:159

.= ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) /. 2 by A164, FINSEQ_6:159

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 2 by JORDAN1E:11 ;

A166: (L~ go) \/ (L~ co) is compact by COMPTS_1:10;

W-min (L~ (Cage (C,n))) in (L~ go) \/ (L~ co) by A64, A80, XBOOLE_0:def 3;

then A167: W-min ((L~ go) \/ (L~ co)) = W-min (L~ (Cage (C,n))) by A157, A158, A166, JORDAN1J:21, XBOOLE_1:8;

A168: (W-min ((L~ go) \/ (L~ co))) `1 = W-bound ((L~ go) \/ (L~ co)) by EUCLID:52;

A169: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;

((Gauge (C,n)) * (i1,j)) `1 >= W-bound (L~ (Cage (C,n))) by A14, A155, PSCOMP_1:24;

then ((Gauge (C,n)) * (i1,j)) `1 > W-bound (L~ (Cage (C,n))) by A78, XXREAL_0:1;

then W-min (((L~ go) \/ (L~ co)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ co)) by A96, A166, A167, A168, A169, JORDAN1J:33;

then A170: W-min (L~ godo) = W-min (L~ (Cage (C,n))) by A153, A167, XBOOLE_1:4;

A171: rng godo c= L~ godo by A99, A101, SPPOL_2:18, XXREAL_0:2;

2 in dom godo by A102, FINSEQ_3:25;

then A172: godo /. 2 in rng godo by PARTFUN2:2;

godo /. 2 in W-most (L~ (Cage (C,n))) by A165, JORDAN1I:25;

then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A170, PSCOMP_1:31

.= W-bound (L~ godo) by EUCLID:52 ;

then godo /. 2 in W-most (L~ godo) by A171, A172, SPRECT_2:12;

then (Rotate (godo,(W-min (L~ godo)))) /. 2 in W-most (L~ godo) by A163, A170, FINSEQ_6:89;

then reconsider godo = godo as V26() 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 A173: (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 ;

A174: east_halfline (E-max C) misses L~ go

proof

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

then consider p being object such that

A175: p in east_halfline (E-max C) and

A176: p in L~ go by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A175;

p in L~ (Upper_Seq (C,n)) by A49, A176;

then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A155, A175, XBOOLE_0:def 4;

then A177: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

then A178: p = E-max (L~ (Cage (C,n))) by A49, A176, JORDAN1J:46;

then E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j) by A14, A173, A176, JORDAN1J:43;

then ((Gauge (C,n)) * (i1,j)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A6, A16, A20, A177, A178, JORDAN1A:71;

hence contradiction by A2, A3, A17, A33, JORDAN1G:7; :: thesis: verum

end;then consider p being object such that

A175: p in east_halfline (E-max C) and

A176: p in L~ go by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A175;

p in L~ (Upper_Seq (C,n)) by A49, A176;

then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A155, A175, XBOOLE_0:def 4;

then A177: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

then A178: p = E-max (L~ (Cage (C,n))) by A49, A176, JORDAN1J:46;

then E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j) by A14, A173, A176, JORDAN1J:43;

then ((Gauge (C,n)) * (i1,j)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A6, A16, A20, A177, A178, JORDAN1A:71;

hence contradiction by A2, A3, A17, A33, JORDAN1G:7; :: thesis: verum

now :: thesis: not east_halfline (E-max C) meets L~ godo

then
east_halfline (E-max C) c= (L~ godo) `
by SUBSET_1:23;assume
east_halfline (E-max C) meets L~ godo
; :: thesis: contradiction

then A179: ( east_halfline (E-max C) meets (L~ go) \/ (L~ pion1) or east_halfline (E-max C) meets L~ co ) by A153, XBOOLE_1:70;

end;then A179: ( east_halfline (E-max C) meets (L~ go) \/ (L~ pion1) or east_halfline (E-max C) meets L~ co ) by A153, XBOOLE_1:70;

per cases
( east_halfline (E-max C) meets L~ go or east_halfline (E-max C) meets L~ pion1 or east_halfline (E-max C) meets L~ co )
by A179, XBOOLE_1:70;

end;

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

then consider p being object such that

A180: p in east_halfline (E-max C) and

A181: p in L~ pion1 by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A180;

then i2 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;

then A183: i2 <= (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)) * (i2,k)) `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A6, A11, A16, A20, A24, A183, JORDAN1A:18;

then p `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A182, XXREAL_0:2;

then p `1 <= E-bound C by A24, JORDAN8:12;

then A184: p `1 <= (E-max C) `1 by EUCLID:52;

p `1 >= (E-max C) `1 by A180, TOPREAL1:def 11;

then A185: p `1 = (E-max C) `1 by A184, XXREAL_0:1;

p `2 = (E-max C) `2 by A180, TOPREAL1:def 11;

then p = E-max C by A185, TOPREAL3:6;

hence contradiction by A9, A12, A88, A144, A181, XBOOLE_0:3; :: thesis: verum

end;A180: p in east_halfline (E-max C) and

A181: p in L~ pion1 by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A180;

A182: now :: thesis: p `1 <= ((Gauge (C,n)) * (i2,k)) `1 end;

i2 + 1 <= len (Gauge (C,n))
by A3, NAT_1:13;per cases
( p in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) or p in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) )
by A12, A88, A181, XBOOLE_0:def 3;

end;

then i2 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;

then A183: i2 <= (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)) * (i2,k)) `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A6, A11, A16, A20, A24, A183, JORDAN1A:18;

then p `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A182, XXREAL_0:2;

then p `1 <= E-bound C by A24, JORDAN8:12;

then A184: p `1 <= (E-max C) `1 by EUCLID:52;

p `1 >= (E-max C) `1 by A180, TOPREAL1:def 11;

then A185: p `1 = (E-max C) `1 by A184, XXREAL_0:1;

p `2 = (E-max C) `2 by A180, TOPREAL1:def 11;

then p = E-max C by A185, TOPREAL3:6;

hence contradiction by A9, A12, A88, A144, A181, XBOOLE_0:3; :: thesis: verum

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

then consider p being object such that

A186: p in east_halfline (E-max C) and

A187: p in L~ co by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A186;

p in L~ (Lower_Seq (C,n)) by A56, A187;

then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A156, A186, XBOOLE_0:def 4;

then A188: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

A189: (E-max C) `2 = p `2 by A186, TOPREAL1:def 11;

set RC = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));

A190: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by JORDAN1I:7;

A191: 1 + 1 <= len (Lower_Seq (C,n)) by A28, 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:18;

then A192: LSeg ((Lower_Seq (C,n)),1) = LSeg ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by A191, SPPOL_2:9;

A193: L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = L~ (Cage (C,n)) by REVROT_1:33;

A194: len (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = len (Cage (C,n)) by FINSEQ_6:179;

A195: GoB (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = GoB (Cage (C,n)) by REVROT_1:28

.= Gauge (C,n) by JORDAN1H:44 ;

A196: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

A197: Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by A150, REVROT_1:34;

A198: (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 A193, A196, FINSEQ_6:92;

consider ii, jj being Nat such that

A199: [ii,(jj + 1)] in Indices (Gauge (C,n)) and

A200: [ii,jj] in Indices (Gauge (C,n)) and

A201: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = (Gauge (C,n)) * (ii,(jj + 1)) and

A202: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. (1 + 1) = (Gauge (C,n)) * (ii,jj) by A97, A193, A194, A196, A197, FINSEQ_6:92, JORDAN1I:23;

consider jj2 being Nat such that

A203: 1 <= jj2 and

A204: jj2 <= width (Gauge (C,n)) and

A205: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),jj2) by JORDAN1D:25;

A206: len (Gauge (C,n)) >= 4 by JORDAN8:10;

then len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then [(len (Gauge (C,n))),jj2] in Indices (Gauge (C,n)) by A203, A204, MATRIX_0:30;

then A207: ii = len (Gauge (C,n)) by A193, A198, A199, A201, A205, GOBOARD1:5;

A208: 1 <= ii by A199, MATRIX_0:32;

A209: ii <= len (Gauge (C,n)) by A199, MATRIX_0:32;

A210: 1 <= jj + 1 by A199, MATRIX_0:32;

A211: jj + 1 <= width (Gauge (C,n)) by A199, MATRIX_0:32;

A212: 1 <= ii by A200, MATRIX_0:32;

A213: ii <= len (Gauge (C,n)) by A200, MATRIX_0:32;

A214: 1 <= jj by A200, MATRIX_0:32;

A215: jj <= width (Gauge (C,n)) by A200, MATRIX_0:32;

A216: ii + 1 <> ii ;

(jj + 1) + 1 <> jj ;

then A217: right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) = cell ((Gauge (C,n)),(ii -' 1),jj) by A97, A194, A195, A199, A200, A201, A202, A216, GOBOARD5:def 6;

A218: (ii -' 1) + 1 = ii by A208, XREAL_1:235;

ii - 1 >= 4 - 1 by A206, A207, XREAL_1:9;

then A219: ii - 1 >= 1 by XXREAL_0:2;

then A220: 1 <= ii -' 1 by XREAL_0:def 2;

A221: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 <= p `2 by A189, A190, A209, A211, A214, A217, A218, A219, JORDAN9:17;

A222: p `2 <= ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 by A189, A190, A209, A211, A214, A217, A218, A219, JORDAN9:17;

A223: ii -' 1 < len (Gauge (C,n)) by A209, A218, NAT_1:13;

then A224: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 = ((Gauge (C,n)) * (1,jj)) `2 by A214, A215, A220, GOBOARD5:1

.= ((Gauge (C,n)) * (ii,jj)) `2 by A212, A213, A214, A215, GOBOARD5:1 ;

A225: ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 = ((Gauge (C,n)) * (1,(jj + 1))) `2 by A210, A211, A220, A223, GOBOARD5:1

.= ((Gauge (C,n)) * (ii,(jj + 1))) `2 by A208, A209, A210, A211, GOBOARD5:1 ;

A226: ((Gauge (C,n)) * ((len (Gauge (C,n))),jj)) `1 = E-bound (L~ (Cage (C,n))) by A20, A214, A215, JORDAN1A:71;

E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),(jj + 1))) `1 by A20, A210, A211, JORDAN1A:71;

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 A188, A201, A202, A207, A221, A222, A224, A225, A226, GOBOARD7:7;

then A227: p in LSeg ((Lower_Seq (C,n)),1) by A97, A192, A194, TOPREAL1:def 3;

A228: p in LSeg (co,(Index (p,co))) by A187, JORDAN3:9;

A229: co = mid ((Lower_Seq (C,n)),(((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))),(len (Lower_Seq (C,n)))) by A40, JORDAN1J:37;

A230: 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A40, FINSEQ_4:21;

A231: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <= len (Lower_Seq (C,n)) by A40, FINSEQ_4:21;

((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <> len (Lower_Seq (C,n)) by A32, A40, FINSEQ_4:19;

then A232: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) < len (Lower_Seq (C,n)) by A231, XXREAL_0:1;

A233: 1 <= Index (p,co) by A187, JORDAN3:8;

A234: Index (p,co) < len co by A187, JORDAN3:8;

A235: (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A35, A40, JORDAN1J:56;

consider t being Nat such that

A236: t in dom (Lower_Seq (C,n)) and

A237: (Lower_Seq (C,n)) . t = (Gauge (C,n)) * (i2,k) by A40, FINSEQ_2:10;

A238: 1 <= t by A236, FINSEQ_3:25;

A239: t <= len (Lower_Seq (C,n)) by A236, FINSEQ_3:25;

1 < t by A35, A237, A238, XXREAL_0:1;

then (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = t by A237, A239, JORDAN3:12;

then A240: len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k)))) = (len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by A13, A237, JORDAN3:26;

set tt = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1;

A241: 1 <= Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))) by A13, JORDAN3:8;

0 + (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) < len (Lower_Seq (C,n)) by A13, JORDAN3:8;

then A242: (len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) > 0 by XREAL_1:20;

Index (p,co) < (len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by A234, A240, XREAL_0:def 2;

then (Index (p,co)) + 1 <= (len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by NAT_1:13;

then Index (p,co) <= ((len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))))) - 1 by XREAL_1:19;

then Index (p,co) <= ((len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))))) - 1 by A242, XREAL_0:def 2;

then Index (p,co) <= (len (Lower_Seq (C,n))) - (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) by A235;

then Index (p,co) <= (len (Lower_Seq (C,n))) -' (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) by XREAL_0:def 2;

then Index (p,co) < ((len (Lower_Seq (C,n))) -' (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) + 1 by NAT_1:13;

then A243: LSeg ((mid ((Lower_Seq (C,n)),(((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))),(len (Lower_Seq (C,n))))),(Index (p,co))) = LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1)) by A230, A232, A233, JORDAN4:19;

A244: 1 + 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A235, A241, XREAL_1:7;

then (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) >= (1 + 1) + 1 by A233, XREAL_1:7;

then ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) - 1 >= ((1 + 1) + 1) - 1 by XREAL_1:9;

then A245: ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 >= 1 + 1 by XREAL_0:def 2;

A246: 2 in dom (Lower_Seq (C,n)) by A191, FINSEQ_3:25;

end;A186: p in east_halfline (E-max C) and

A187: p in L~ co by XBOOLE_0:3;

reconsider p = p as Point of (TOP-REAL 2) by A186;

p in L~ (Lower_Seq (C,n)) by A56, A187;

then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A156, A186, XBOOLE_0:def 4;

then A188: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;

A189: (E-max C) `2 = p `2 by A186, TOPREAL1:def 11;

set RC = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));

A190: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by JORDAN1I:7;

A191: 1 + 1 <= len (Lower_Seq (C,n)) by A28, 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:18;

then A192: LSeg ((Lower_Seq (C,n)),1) = LSeg ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by A191, SPPOL_2:9;

A193: L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = L~ (Cage (C,n)) by REVROT_1:33;

A194: len (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = len (Cage (C,n)) by FINSEQ_6:179;

A195: GoB (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = GoB (Cage (C,n)) by REVROT_1:28

.= Gauge (C,n) by JORDAN1H:44 ;

A196: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

A197: Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by A150, REVROT_1:34;

A198: (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 A193, A196, FINSEQ_6:92;

consider ii, jj being Nat such that

A199: [ii,(jj + 1)] in Indices (Gauge (C,n)) and

A200: [ii,jj] in Indices (Gauge (C,n)) and

A201: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = (Gauge (C,n)) * (ii,(jj + 1)) and

A202: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. (1 + 1) = (Gauge (C,n)) * (ii,jj) by A97, A193, A194, A196, A197, FINSEQ_6:92, JORDAN1I:23;

consider jj2 being Nat such that

A203: 1 <= jj2 and

A204: jj2 <= width (Gauge (C,n)) and

A205: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),jj2) by JORDAN1D:25;

A206: len (Gauge (C,n)) >= 4 by JORDAN8:10;

then len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then [(len (Gauge (C,n))),jj2] in Indices (Gauge (C,n)) by A203, A204, MATRIX_0:30;

then A207: ii = len (Gauge (C,n)) by A193, A198, A199, A201, A205, GOBOARD1:5;

A208: 1 <= ii by A199, MATRIX_0:32;

A209: ii <= len (Gauge (C,n)) by A199, MATRIX_0:32;

A210: 1 <= jj + 1 by A199, MATRIX_0:32;

A211: jj + 1 <= width (Gauge (C,n)) by A199, MATRIX_0:32;

A212: 1 <= ii by A200, MATRIX_0:32;

A213: ii <= len (Gauge (C,n)) by A200, MATRIX_0:32;

A214: 1 <= jj by A200, MATRIX_0:32;

A215: jj <= width (Gauge (C,n)) by A200, MATRIX_0:32;

A216: ii + 1 <> ii ;

(jj + 1) + 1 <> jj ;

then A217: right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) = cell ((Gauge (C,n)),(ii -' 1),jj) by A97, A194, A195, A199, A200, A201, A202, A216, GOBOARD5:def 6;

A218: (ii -' 1) + 1 = ii by A208, XREAL_1:235;

ii - 1 >= 4 - 1 by A206, A207, XREAL_1:9;

then A219: ii - 1 >= 1 by XXREAL_0:2;

then A220: 1 <= ii -' 1 by XREAL_0:def 2;

A221: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 <= p `2 by A189, A190, A209, A211, A214, A217, A218, A219, JORDAN9:17;

A222: p `2 <= ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 by A189, A190, A209, A211, A214, A217, A218, A219, JORDAN9:17;

A223: ii -' 1 < len (Gauge (C,n)) by A209, A218, NAT_1:13;

then A224: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 = ((Gauge (C,n)) * (1,jj)) `2 by A214, A215, A220, GOBOARD5:1

.= ((Gauge (C,n)) * (ii,jj)) `2 by A212, A213, A214, A215, GOBOARD5:1 ;

A225: ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 = ((Gauge (C,n)) * (1,(jj + 1))) `2 by A210, A211, A220, A223, GOBOARD5:1

.= ((Gauge (C,n)) * (ii,(jj + 1))) `2 by A208, A209, A210, A211, GOBOARD5:1 ;

A226: ((Gauge (C,n)) * ((len (Gauge (C,n))),jj)) `1 = E-bound (L~ (Cage (C,n))) by A20, A214, A215, JORDAN1A:71;

E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),(jj + 1))) `1 by A20, A210, A211, JORDAN1A:71;

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 A188, A201, A202, A207, A221, A222, A224, A225, A226, GOBOARD7:7;

then A227: p in LSeg ((Lower_Seq (C,n)),1) by A97, A192, A194, TOPREAL1:def 3;

A228: p in LSeg (co,(Index (p,co))) by A187, JORDAN3:9;

A229: co = mid ((Lower_Seq (C,n)),(((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))),(len (Lower_Seq (C,n)))) by A40, JORDAN1J:37;

A230: 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A40, FINSEQ_4:21;

A231: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <= len (Lower_Seq (C,n)) by A40, FINSEQ_4:21;

((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <> len (Lower_Seq (C,n)) by A32, A40, FINSEQ_4:19;

then A232: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) < len (Lower_Seq (C,n)) by A231, XXREAL_0:1;

A233: 1 <= Index (p,co) by A187, JORDAN3:8;

A234: Index (p,co) < len co by A187, JORDAN3:8;

A235: (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A35, A40, JORDAN1J:56;

consider t being Nat such that

A236: t in dom (Lower_Seq (C,n)) and

A237: (Lower_Seq (C,n)) . t = (Gauge (C,n)) * (i2,k) by A40, FINSEQ_2:10;

A238: 1 <= t by A236, FINSEQ_3:25;

A239: t <= len (Lower_Seq (C,n)) by A236, FINSEQ_3:25;

1 < t by A35, A237, A238, XXREAL_0:1;

then (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = t by A237, A239, JORDAN3:12;

then A240: len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i2,k)))) = (len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by A13, A237, JORDAN3:26;

set tt = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1;

A241: 1 <= Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))) by A13, JORDAN3:8;

0 + (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) < len (Lower_Seq (C,n)) by A13, JORDAN3:8;

then A242: (len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) > 0 by XREAL_1:20;

Index (p,co) < (len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by A234, A240, XREAL_0:def 2;

then (Index (p,co)) + 1 <= (len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) by NAT_1:13;

then Index (p,co) <= ((len (Lower_Seq (C,n))) -' (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))))) - 1 by XREAL_1:19;

then Index (p,co) <= ((len (Lower_Seq (C,n))) - (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n))))) - 1 by A242, XREAL_0:def 2;

then Index (p,co) <= (len (Lower_Seq (C,n))) - (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) by A235;

then Index (p,co) <= (len (Lower_Seq (C,n))) -' (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) by XREAL_0:def 2;

then Index (p,co) < ((len (Lower_Seq (C,n))) -' (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) + 1 by NAT_1:13;

then A243: LSeg ((mid ((Lower_Seq (C,n)),(((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))),(len (Lower_Seq (C,n))))),(Index (p,co))) = LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1)) by A230, A232, A233, JORDAN4:19;

A244: 1 + 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A235, A241, XREAL_1:7;

then (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) >= (1 + 1) + 1 by A233, XREAL_1:7;

then ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) - 1 >= ((1 + 1) + 1) - 1 by XREAL_1:9;

then A245: ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 >= 1 + 1 by XREAL_0:def 2;

A246: 2 in dom (Lower_Seq (C,n)) by A191, FINSEQ_3:25;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 > 1 + 1 or ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 = 1 + 1 )
by A245, XXREAL_0:1;

end;

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

then
LSeg ((Lower_Seq (C,n)),1) misses LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1))
by TOPREAL1:def 7;

hence contradiction by A227, A228, A229, A243, XBOOLE_0:3; :: thesis: verum

end;hence contradiction by A227, A228, A229, A243, XBOOLE_0:3; :: thesis: verum

suppose A247:
((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 = 1 + 1
; :: thesis: contradiction

then
(LSeg ((Lower_Seq (C,n)),1)) /\ (LSeg ((Lower_Seq (C,n)),(((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1))) = {((Lower_Seq (C,n)) /. 2)}
by A28, TOPREAL1:def 6;

then p in {((Lower_Seq (C,n)) /. 2)} by A227, A228, A229, A243, XBOOLE_0:def 4;

then A248: p = (Lower_Seq (C,n)) /. 2 by TARSKI:def 1;

then A249: p .. (Lower_Seq (C,n)) = 2 by A246, FINSEQ_5:41;

1 + 1 = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) - 1 by A247, XREAL_0:def 2;

then (1 + 1) + 1 = (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) ;

then A250: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) = 2 by A233, A244, JORDAN1E:6;

p in rng (Lower_Seq (C,n)) by A246, A248, PARTFUN2:2;

then p = (Gauge (C,n)) * (i2,k) by A40, A249, A250, FINSEQ_5:9;

then ((Gauge (C,n)) * (i2,k)) `1 = E-bound (L~ (Cage (C,n))) by A248, JORDAN1G:32;

then ((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A15, A20, JORDAN1A:71;

hence contradiction by A3, A18, A70, JORDAN1G:7; :: thesis: verum

end;then p in {((Lower_Seq (C,n)) /. 2)} by A227, A228, A229, A243, XBOOLE_0:def 4;

then A248: p = (Lower_Seq (C,n)) /. 2 by TARSKI:def 1;

then A249: p .. (Lower_Seq (C,n)) = 2 by A246, FINSEQ_5:41;

1 + 1 = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) - 1 by A247, XREAL_0:def 2;

then (1 + 1) + 1 = (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) ;

then A250: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) = 2 by A233, A244, JORDAN1E:6;

p in rng (Lower_Seq (C,n)) by A246, A248, PARTFUN2:2;

then p = (Gauge (C,n)) * (i2,k) by A40, A249, A250, FINSEQ_5:9;

then ((Gauge (C,n)) * (i2,k)) `1 = E-bound (L~ (Cage (C,n))) by A248, JORDAN1G:32;

then ((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A15, A20, JORDAN1A:71;

hence contradiction by A3, A18, A70, JORDAN1G:7; :: thesis: verum

then consider W being Subset of (TOP-REAL 2) such that

A251: W is_a_component_of (L~ godo) ` and

A252: east_halfline (E-max C) c= W by GOBOARD9:3;

not W is bounded by A252, JORDAN2C:121, RLTOPSP1:42;

then W is_outside_component_of L~ godo by A251, JORDAN2C:def 3;

then W c= UBD (L~ godo) by JORDAN2C:23;

then A253: east_halfline (E-max C) c= UBD (L~ godo) by A252;

E-max C in east_halfline (E-max C) by TOPREAL1:38;

then E-max C in UBD (L~ godo) by A253;

then E-max C in LeftComp godo by GOBRD14:36;

then Upper_Arc C meets L~ godo by A142, A143, A144, A152, A162, JORDAN1J:36;

then A254: ( Upper_Arc C meets (L~ go) \/ (L~ pion1) or Upper_Arc C meets L~ co ) by A153, XBOOLE_1:70;

A255: Upper_Arc C c= C by JORDAN6:61;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( Upper_Arc C meets L~ go or Upper_Arc C meets L~ pion1 or Upper_Arc C meets L~ co )
by A254, XBOOLE_1:70;

end;

suppose
Upper_Arc C meets L~ go
; :: thesis: contradiction

then
Upper_Arc C meets L~ (Cage (C,n))
by A49, A155, XBOOLE_1:1, XBOOLE_1:63;

hence contradiction by A255, JORDAN10:5, XBOOLE_1:63; :: thesis: verum

end;hence contradiction by A255, JORDAN10:5, XBOOLE_1:63; :: thesis: verum

suppose
Upper_Arc C meets L~ co
; :: thesis: contradiction

then
Upper_Arc C meets L~ (Cage (C,n))
by A56, A156, XBOOLE_1:1, XBOOLE_1:63;

hence contradiction by A255, JORDAN10:5, XBOOLE_1:63; :: thesis: verum

end;hence contradiction by A255, JORDAN10:5, XBOOLE_1:63; :: thesis: verum

suppose
((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * (i1,j)) `1
; :: thesis: contradiction

then A256:
i1 = i2
by A17, A18, JORDAN1G:7;

then LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) = {((Gauge (C,n)) * (i1,k))} by RLTOPSP1:70;

then LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) c= LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by A84, ZFMISC_1:31;

then (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by XBOOLE_1:12;

hence contradiction by A1, A3, A4, A5, A6, A7, A8, A9, A256, Th12; :: thesis: verum

end;then LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) = {((Gauge (C,n)) * (i1,k))} by RLTOPSP1:70;

then LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) c= LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by A84, ZFMISC_1:31;

then (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by XBOOLE_1:12;

hence contradiction by A1, A3, A4, A5, A6, A7, A8, A9, A256, Th12; :: thesis: verum

suppose
((Gauge (C,n)) * (i2,k)) `2 = ((Gauge (C,n)) * (i1,j)) `2
; :: thesis: contradiction

then A257:
j = k
by A17, A18, JORDAN1G:6;

then LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) = {((Gauge (C,n)) * (i1,k))} by RLTOPSP1:70;

then LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) c= LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by A85, ZFMISC_1:31;

then (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by XBOOLE_1:12;

hence contradiction by A1, A2, A3, A4, A6, A7, A8, A9, A257, JORDAN15:37; :: thesis: verum

end;then LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) = {((Gauge (C,n)) * (i1,k))} by RLTOPSP1:70;

then LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) c= LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by A85, ZFMISC_1:31;

then (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by XBOOLE_1:12;

hence contradiction by A1, A2, A3, A4, A6, A7, A8, A9, A257, JORDAN15:37; :: thesis: verum