let n be Element of NAT ; :: thesis: for C being Simple_closed_curve
for i1, i2, j, k being Element of 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 Lower_Arc C
let C be Simple_closed_curve; :: thesis: for i1, i2, j, k being Element of 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 Lower_Arc C
let i1, i2, j, k be Element of 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 Lower_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 Lower_Arc C ; :: thesis: contradiction
set UA = 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 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:23;
(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_1:37;
A18: [i2,k] in Indices (Gauge C,n) by A3, A6, A11, A16, MATRIX_1:37;
A19: [i1,k] in Indices (Gauge C,n) by A1, A6, A10, A16, MATRIX_1:37;
set go = R_Cut (Upper_Seq C,n),((Gauge C,n) * i1,j);
set do = 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:19;
then len (Upper_Seq C,n) >= 1 by XXREAL_0:2;
then 1 in dom (Upper_Seq C,n) by FINSEQ_3:27;
then A22: (Upper_Seq C,n) . 1 = (Upper_Seq C,n) /. 1 by PARTFUN1:def 8
.= 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:56
.= ((Gauge C,n) * 1,k) `1 by A6, A16, A20, JORDAN1A:94 ;
len (Gauge C,n) >= 4 by JORDAN8:13;
then A24: len (Gauge C,n) >= 1 by XXREAL_0:2;
then A25: [1,k] in Indices (Gauge C,n) by A6, A16, MATRIX_1:37;
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:70;
A27: [1,j] in Indices (Gauge C,n) by A4, A15, A24, MATRIX_1:37;
A28: len (Lower_Seq C,n) >= 1 + 2 by JORDAN1E:19;
then A29: len (Lower_Seq C,n) >= 1 by XXREAL_0:2;
then A30: 1 in dom (Lower_Seq C,n) by FINSEQ_3:27;
len (Lower_Seq C,n) in dom (Lower_Seq C,n) by A29, FINSEQ_3:27;
then A31: (Lower_Seq C,n) . (len (Lower_Seq C,n)) = (Lower_Seq C,n) /. (len (Lower_Seq C,n)) by PARTFUN1:def 8
.= W-min (L~ (Cage C,n)) by JORDAN1F:8 ;
(W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * 1,k) `1 by A6, A16, A20, JORDAN1A:94 ;
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 do = L_Cut (Lower_Seq C,n),((Gauge C,n) * i2,k) as being_S-Seq FinSequence of (TOP-REAL 2) by A13, JORDAN3:69;
A33: [(len (Gauge C,n)),k] in Indices (Gauge C,n) by A6, A16, A24, MATRIX_1:37;
A34: (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by A30, PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
(E-max (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56
.= ((Gauge C,n) * (len (Gauge C,n)),k) `1 by A6, A16, A20, JORDAN1A:92 ;
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 10;
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 do >= 1 + 1 by TOPREAL1:def 10;
A40: (Gauge C,n) * i2,k in rng (Lower_Seq C,n) by A3, A6, A11, A13, A16, JORDAN1G:5, JORDAN1J:40;
then A41: do is_sequence_on Gauge C,n by JORDAN1G:5, JORDAN1J:39;
reconsider go = go as non constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A36, A38, JGRAPH_1:16, JORDAN8:8;
reconsider do = do as non constant being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A39, A41, JGRAPH_1:16, JORDAN8:8;
A42: len go > 1 by A36, NAT_1:13;
then A43: len go in dom go by FINSEQ_3:27;
then A44: go /. (len go) = go . (len go) by PARTFUN1:def 8
.= (Gauge C,n) * i1,j by A14, JORDAN3:59 ;
len do >= 1 by A39, XXREAL_0:2;
then 1 in dom do by FINSEQ_3:27;
then A45: do /. 1 = do . 1 by PARTFUN1:def 8
.= (Gauge C,n) * i2,k by A13, JORDAN3:58 ;
reconsider m = (len go) - 1 as Element of NAT by A43, FINSEQ_3:28;
A46: m + 1 = len go ;
then A47: (len go) -' 1 = m by NAT_D:34;
A48: LSeg go,m c= L~ go by TOPREAL3:26;
A49: L~ go c= L~ (Upper_Seq C,n) by A14, JORDAN3:76;
then LSeg go,m c= L~ (Upper_Seq C,n) by A48, XBOOLE_1:1;
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:21;
then A51: LSeg go,m = LSeg (go /. m),((Gauge C,n) * i1,j) by A44, A46, TOPREAL1:def 5;
{((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
let x be set ; :: 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:69;
(Gauge C,n) * i1,j in LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k) by RLTOPSP1:69;
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:10;
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;
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, XBOOLE_0:def 10;
A55: LSeg do,1 c= L~ do by TOPREAL3:26;
A56: L~ do c= L~ (Lower_Seq C,n) by A13, JORDAN3:77;
then LSeg do,1 c= L~ (Lower_Seq C,n) by A55, XBOOLE_1:1;
then A57: (LSeg do,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 do,1 = LSeg ((Gauge C,n) * i2,k),(do /. (1 + 1)) by A39, A45, TOPREAL1:def 5;
{((Gauge C,n) * i2,k)} c= (LSeg do,1) /\ (L~ <*((Gauge C,n) * i1,j),((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)*>)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge C,n) * i2,k)} or x in (LSeg do,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 do,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 do,1 by A58, RLTOPSP1:69;
(Gauge C,n) * i2,k in LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k) by RLTOPSP1:69;
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:10;
hence x in (LSeg do,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;
then A61: (L~ <*((Gauge C,n) * i1,j),((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)*>) /\ (LSeg do,1) = {((Gauge C,n) * i2,k)} by A57, XBOOLE_0:def 10;
A62: go /. 1 = (Upper_Seq C,n) /. 1 by A14, SPRECT_3:39
.= 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
.= do /. (len do) by A13, JORDAN1J:35 ;
A64: rng go c= L~ go by A36, SPPOL_2:18;
A65: rng do c= L~ do by A39, SPPOL_2:18;
A66: {(go /. 1)} c= (L~ go) /\ (L~ do)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(go /. 1)} or x in (L~ go) /\ (L~ do) )
assume x in {(go /. 1)} ; :: thesis: x in (L~ go) /\ (L~ do)
then A67: x = go /. 1 by TARSKI:def 1;
then A68: x in rng go by FINSEQ_6:46;
x in rng do by A63, A67, REVROT_1:3;
hence x in (L~ go) /\ (L~ do) by A64, A65, A68, XBOOLE_0:def 4; :: thesis: verum
end;
A69: (Lower_Seq C,n) . 1 = (Lower_Seq C,n) /. 1 by A30, PARTFUN1:def 8
.= 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_1:37;
(L~ go) /\ (L~ do) c= {(go /. 1)}
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ go) /\ (L~ do) or x in {(go /. 1)} )
assume A71: x in (L~ go) /\ (L~ do) ; :: thesis: x in {(go /. 1)}
then A72: x in L~ go by XBOOLE_0:def 4;
A73: x in L~ do 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:20;
then A74: ( x = W-min (L~ (Cage C,n)) or x = E-max (L~ (Cage C,n)) ) by TARSKI:def 2;
now
assume x = E-max (L~ (Cage C,n)) ; :: thesis: contradiction
then A75: E-max (L~ (Cage C,n)) = (Gauge C,n) * i2,k by A13, A69, A73, JORDAN1E:11;
((Gauge C,n) * (len (Gauge C,n)),j) `1 = E-bound (L~ (Cage C,n)) by A4, A15, A20, JORDAN1A:92;
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:56; :: thesis: verum
end;
hence x in {(go /. 1)} by A62, A74, TARSKI:def 1; :: thesis: verum
end;
then A76: (L~ go) /\ (L~ do) = {(go /. 1)} by A66, XBOOLE_0:def 10;
set W2 = go /. 2;
A77: 2 in dom go by A36, FINSEQ_3:27;
A78: now
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:94;
hence contradiction by A1, A17, A27, JORDAN1G:7; :: thesis: verum
end;
go = mid (Upper_Seq C,n),1,(((Gauge C,n) * i1,j) .. (Upper_Seq C,n)) by A37, JORDAN1G:57
.= (Upper_Seq C,n) | (((Gauge C,n) * i1,j) .. (Upper_Seq C,n)) by A37, FINSEQ_4:31, JORDAN3:25 ;
then A79: go /. 2 = (Upper_Seq C,n) /. 2 by A77, FINSEQ_4:85;
A80: W-min (L~ (Cage C,n)) in rng go by A62, FINSEQ_6:46;
set pion = <*((Gauge C,n) * i1,j),((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)*>;
A81: now
let n be Element of 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 Element of 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 Element of 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_3:1, FINSEQ_3:30;
then ( n = 1 or n = 2 or n = 3 ) by ENUMSET1:def 1;
hence ex i, j being Element of 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:27; :: thesis: verum
end;
A82: ((Gauge C,n) * i1,k) `1 = ((Gauge C,n) * i1,1) `1 by A1, A6, A10, A16, GOBOARD5:3
.= ((Gauge C,n) * i1,j) `1 by A1, A4, A10, A15, GOBOARD5:3 ;
((Gauge C,n) * i1,k) `2 = ((Gauge C,n) * 1,k) `2 by A1, A6, A10, A16, GOBOARD5:2
.= ((Gauge C,n) * i2,k) `2 by A3, A6, A11, A16, GOBOARD5:2 ;
then A83: (Gauge C,n) * i1,k = |[(((Gauge C,n) * i1,j) `1 ),(((Gauge C,n) * i2,k) `2 )]| by A82, EUCLID:57;
A84: (Gauge C,n) * i1,k in LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k) by RLTOPSP1:69;
A85: (Gauge C,n) * i1,k in LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k) by RLTOPSP1:69;
now
per 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 ) ;
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:41;
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) ^' do;
A92: ((Gauge C,n) * i1,k) `1 = ((Gauge C,n) * i1,1) `1 by A1, A6, A10, A16, GOBOARD5:3
.= ((Gauge C,n) * i1,j) `1 by A1, A4, A10, A15, GOBOARD5:3 ;
A93: ((Gauge C,n) * i1,k) `1 <= ((Gauge C,n) * i2,k) `1 by A1, A2, A3, A6, A16, JORDAN1A:39;
then A94: W-bound (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) = ((Gauge C,n) * i1,k) `1 by SPRECT_1:62;
A95: W-bound (LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) = ((Gauge C,n) * i1,j) `1 by A92, SPRECT_1:62;
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:54
.= ((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:23;
A97: 1 + 1 <= len (Cage C,n) by GOBOARD7:36, XXREAL_0:2;
A98: 1 + 1 <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by GOBOARD7:36, XXREAL_0:2;
len (go ^' pion1) >= len go by TOPREAL8:7;
then 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) ^' do) >= len (go ^' pion1) by TOPREAL8:7;
then A102: 1 + 1 <= len ((go ^' pion1) ^' do) 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:27;
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, GRAPH_2:58
.= <*((Gauge C,n) * i1,j),((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)*> /. 3 by FINSEQ_1:62
.= do /. 1 by A45, FINSEQ_4:27 ;
then A107: (go ^' pion1) ^' do 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:26;
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:62;
then A109: len pion1 > 1 + 1 by NAT_1:13;
{((Gauge C,n) * i1,j)} c= (LSeg go,m) /\ (LSeg pion1,1)
proof
let x be set ; :: 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:69;
(Gauge C,n) * i1,j in LSeg pion1,1 by A44, A104, A109, TOPREAL1:27;
hence x in (LSeg go,m) /\ (LSeg pion1,1) by A110, A111, XBOOLE_0:def 4; :: thesis: verum
end;
then (LSeg go,((len go) -' 1)) /\ (LSeg pion1,1) = {(go /. (len go))} by A44, A47, A108, XBOOLE_0:def 10;
then A112: go ^' pion1 is unfolded by A104, TOPREAL8:34;
len pion1 >= 2 + 1 by A91, FINSEQ_1:62;
then A113: (len pion1) - 2 >= 0 by XREAL_1:21;
((len (go ^' pion1)) + 1) - 1 = ((len go) + (len pion1)) - 1 by GRAPH_2:13;
then (len (go ^' pion1)) - 1 = (len go) + ((len pion1) - 2)
.= (len go) + ((len pion1) -' 2) by 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:21;
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:26;
then A119: (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) c= {((Gauge C,n) * i2,k)} by A61, XBOOLE_1:27;
{((Gauge C,n) * i2,k)} c= (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge C,n) * i2,k)} or x in (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) )
assume x in {((Gauge C,n) * i2,k)} ; :: thesis: x in (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1)
then A120: x = (Gauge C,n) * i2,k by TARSKI:def 1;
A121: (Gauge C,n) * i2,k in LSeg do,1 by A58, RLTOPSP1:69;
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:62
.= (Gauge C,n) * i2,k by FINSEQ_4:27 ;
then (Gauge C,n) * i2,k in LSeg pion1,((len pion1) -' 1) by A115, A116, TOPREAL1:27;
hence x in (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) by A120, A121, XBOOLE_0:def 4; :: thesis: verum
end;
then (LSeg pion1,((len pion1) -' 1)) /\ (LSeg do,1) = {((Gauge C,n) * i2,k)} by A119, XBOOLE_0:def 10;
then A122: (LSeg (go ^' pion1),((len go) + ((len pion1) -' 2))) /\ (LSeg do,1) = {((go ^' pion1) /. (len (go ^' pion1)))} by A45, A104, A106, A117, A118, TOPREAL8:31;
A123: not go ^' pion1 is trivial by A99, REALSET1:13;
A124: rng pion1 c= L~ pion1 by A109, SPPOL_2:18;
A125: {(pion1 /. 1)} c= (L~ go) /\ (L~ pion1)
proof
let x be set ; :: 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, REVROT_1:3;
x in rng pion1 by A126, FINSEQ_6:46;
hence x in (L~ go) /\ (L~ pion1) by A64, A124, A127, XBOOLE_0:def 4; :: thesis: verum
end;
(L~ go) /\ (L~ pion1) c= {(pion1 /. 1)}
proof
let x be set ; :: 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;
then A130: (L~ go) /\ (L~ pion1) = {(pion1 /. 1)} by A125, XBOOLE_0:def 10;
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:62
.= do /. 1 by A45, FINSEQ_4:27 ;
A134: {(pion1 /. (len pion1))} c= (L~ do) /\ (L~ pion1)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(pion1 /. (len pion1))} or x in (L~ do) /\ (L~ pion1) )
assume x in {(pion1 /. (len pion1))} ; :: thesis: x in (L~ do) /\ (L~ pion1)
then A135: x = pion1 /. (len pion1) by TARSKI:def 1;
then A136: x in rng do by A90, A133, FINSEQ_6:46;
x in rng pion1 by A135, REVROT_1:3;
hence x in (L~ do) /\ (L~ pion1) by A65, A124, A136, XBOOLE_0:def 4; :: thesis: verum
end;
(L~ do) /\ (L~ pion1) c= {(pion1 /. (len pion1))}
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ do) /\ (L~ pion1) or x in {(pion1 /. (len pion1))} )
assume A137: x in (L~ do) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. (len pion1))}
then A138: x in L~ do 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;
then A139: (L~ do) /\ (L~ pion1) = {(pion1 /. (len pion1))} by A134, XBOOLE_0:def 10;
A140: (L~ (go ^' pion1)) /\ (L~ do) = ((L~ go) \/ (L~ pion1)) /\ (L~ do) by A104, TOPREAL8:35
.= {(go /. 1)} \/ {(do /. 1)} by A76, A90, A133, A139, XBOOLE_1:23
.= {((go ^' pion1) /. 1)} \/ {(do /. 1)} by GRAPH_2:57
.= {((go ^' pion1) /. 1),(do /. 1)} by ENUMSET1:41 ;
do /. (len do) = (go ^' pion1) /. 1 by A63, GRAPH_2:57;
then reconsider godo = (go ^' pion1) ^' do as non constant standard special_circular_sequence by A102, A106, A107, A112, A114, A122, A123, A131, A132, A140, JORDAN8:7, JORDAN8:8, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;
A141: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def 9;
then A142: Lower_Arc C is connected by JORDAN6:11;
A143: W-min C in Lower_Arc C by A141, TOPREAL1:4;
A144: E-max C in Lower_Arc C by A141, TOPREAL1:4;
set ff = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A145: (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_6:98;
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:23;
then (N-min (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A145, A146, SPRECT_5:24, XXREAL_0:2;
then (N-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A145, A146, SPRECT_5:25, 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:26, XXREAL_0:2;
A148: now
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:31;
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:41;
hence contradiction by A22, A26, JORDAN1F:5; :: thesis: verum
end;
A150: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
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:29;
A153: L~ godo = (L~ (go ^' pion1)) \/ (L~ do) by A106, TOPREAL8:35
.= ((L~ go) \/ (L~ pion1)) \/ (L~ do) by A104, TOPREAL8:35 ;
A154: L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by JORDAN1E:17;
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, XBOOLE_1:1;
A158: L~ do c= L~ (Cage C,n) by A56, A156, XBOOLE_1:1;
A159: W-min C in C by SPRECT_1:15;
A160: now
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~ do ) by A153, XBOOLE_0:def 3;
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 A98, JORDAN1H:29
.= right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1,(GoB (Cage C,n)) by REVROT_1:28
.= right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1,(Gauge C,n) by JORDAN1H:52
.= right_cell ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))),1,(Gauge C,n) by 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:8;
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 GRAPH_2:57
.= W-min (L~ (Cage C,n)) by A62, GRAPH_2:57 ;
A164: len (Upper_Seq C,n) >= 2 by A21, XXREAL_0:2;
A165: godo /. 2 = (go ^' pion1) /. 2 by A99, GRAPH_2:61
.= (Upper_Seq C,n) /. 2 by A36, A79, GRAPH_2:61
.= ((Upper_Seq C,n) ^' (Lower_Seq C,n)) /. 2 by A164, GRAPH_2:61
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 2 by JORDAN1E:15 ;
A166: (L~ go) \/ (L~ do) is compact by COMPTS_1:19;
W-min (L~ (Cage C,n)) in (L~ go) \/ (L~ do) by A64, A80, XBOOLE_0:def 3;
then A167: W-min ((L~ go) \/ (L~ do)) = W-min (L~ (Cage C,n)) by A157, A158, A166, JORDAN1J:21, XBOOLE_1:8;
A168: (W-min ((L~ go) \/ (L~ do))) `1 = W-bound ((L~ go) \/ (L~ do)) by EUCLID:56;
A169: (W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n)) by EUCLID:56;
((Gauge C,n) * i1,j) `1 >= W-bound (L~ (Cage C,n)) by A14, A155, PSCOMP_1:71;
then ((Gauge C,n) * i1,j) `1 > W-bound (L~ (Cage C,n)) by A78, XXREAL_0:1;
then W-min (((L~ go) \/ (L~ do)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ do)) 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:27;
then A172: godo /. 2 in rng godo by PARTFUN2:4;
godo /. 2 in W-most (L~ (Cage C,n)) by A165, JORDAN1I:27;
then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A170, PSCOMP_1:88
.= W-bound (L~ godo) by EUCLID:56 ;
then godo /. 2 in W-most (L~ godo) by A171, A172, SPRECT_2:16;
then (Rotate godo,(W-min (L~ godo))) /. 2 in W-most (L~ godo) by A163, A170, FINSEQ_6:95;
then reconsider godo = godo as non constant standard clockwise_oriented special_circular_sequence by JORDAN1I:27;
len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A173: (Upper_Seq C,n) . (len (Upper_Seq C,n)) = (Upper_Seq C,n) /. (len (Upper_Seq C,n)) by PARTFUN1:def 8
.= E-max (L~ (Cage C,n)) by JORDAN1F:7 ;
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 set 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:104, PSCOMP_1:111;
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:92;
hence contradiction by A2, A3, A17, A33, JORDAN1G:7; :: thesis: verum
end;
now
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~ do ) 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~ do ) by A179, XBOOLE_1:70;
suppose east_halfline (E-max C) meets L~ pion1 ; :: thesis: contradiction
then consider p being set 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;
A182: now
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;
suppose p in LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k) ; :: thesis: p `1 <= ((Gauge C,n) * i2,k) `1
hence p `1 <= ((Gauge C,n) * i2,k) `1 by A93, TOPREAL1:9; :: thesis: verum
end;
suppose p in LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k) ; :: thesis: p `1 <= ((Gauge C,n) * i2,k) `1
hence p `1 <= ((Gauge C,n) * i2,k) `1 by A92, A93, GOBOARD7:5; :: thesis: verum
end;
end;
end;
i2 + 1 <= len (Gauge C,n) by A3, NAT_1:13;
then i2 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
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:39;
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:15;
then A184: p `1 <= (E-max C) `1 by EUCLID:56;
p `1 >= (E-max C) `1 by A180, TOPREAL1:def 13;
then A185: p `1 = (E-max C) `1 by A184, XXREAL_0:1;
p `2 = (E-max C) `2 by A180, TOPREAL1:def 13;
then p = E-max C by A185, TOPREAL3:11;
hence contradiction by A9, A12, A88, A144, A181, XBOOLE_0:3; :: thesis: verum
end;
suppose east_halfline (E-max C) meets L~ do ; :: thesis: contradiction
then consider p being set such that
A186: p in east_halfline (E-max C) and
A187: p in L~ do 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:104, PSCOMP_1:111;
A189: (E-max C) `2 = p `2 by A186, TOPREAL1:def 13;
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:9;
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:26;
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 REVROT_1:14;
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:52 ;
A196: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
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:98;
consider ii, jj being Element of 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:98, JORDAN1I:25;
consider jj2 being Element of 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:29;
A206: len (Gauge C,n) >= 4 by JORDAN8:13;
then len (Gauge C,n) >= 1 by XXREAL_0:2;
then [(len (Gauge C,n)),jj2] in Indices (Gauge C,n) by A203, A204, MATRIX_1:37;
then A207: ii = len (Gauge C,n) by A193, A198, A199, A201, A205, GOBOARD1:21;
A208: 1 <= ii by A199, MATRIX_1:39;
A209: ii <= len (Gauge C,n) by A199, MATRIX_1:39;
A210: 1 <= jj + 1 by A199, MATRIX_1:39;
A211: jj + 1 <= width (Gauge C,n) by A199, MATRIX_1:39;
A212: 1 <= ii by A200, MATRIX_1:39;
A213: ii <= len (Gauge C,n) by A200, MATRIX_1:39;
A214: 1 <= jj by A200, MATRIX_1:39;
A215: jj <= width (Gauge C,n) by A200, MATRIX_1:39;
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:237;
ii - 1 >= 4 - 1 by A206, A207, XREAL_1:11;
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:19;
A222: p `2 <= ((Gauge C,n) * (ii -' 1),(jj + 1)) `2 by A189, A190, A209, A211, A214, A217, A218, A219, JORDAN9:19;
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:2
.= ((Gauge C,n) * ii,jj) `2 by A212, A213, A214, A215, GOBOARD5:2 ;
A225: ((Gauge C,n) * (ii -' 1),(jj + 1)) `2 = ((Gauge C,n) * 1,(jj + 1)) `2 by A210, A211, A220, A223, GOBOARD5:2
.= ((Gauge C,n) * ii,(jj + 1)) `2 by A208, A209, A210, A211, GOBOARD5:2 ;
A226: ((Gauge C,n) * (len (Gauge C,n)),jj) `1 = E-bound (L~ (Cage C,n)) by A20, A214, A215, JORDAN1A:92;
E-bound (L~ (Cage C,n)) = ((Gauge C,n) * (len (Gauge C,n)),(jj + 1)) `1 by A20, A210, A211, JORDAN1A:92;
then p in LSeg ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1),((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. (1 + 1)) by A188, A201, A202, A207, A221, A222, A224, A225, A226, GOBOARD7:8;
then A227: p in LSeg (Lower_Seq C,n),1 by A97, A192, A194, TOPREAL1:def 5;
A228: p in LSeg do,(Index p,do) by A187, JORDAN3:42;
A229: do = 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:31;
A231: ((Gauge C,n) * i2,k) .. (Lower_Seq C,n) <= len (Lower_Seq C,n) by A40, FINSEQ_4:31;
((Gauge C,n) * i2,k) .. (Lower_Seq C,n) <> len (Lower_Seq C,n) by A32, A40, FINSEQ_4:29;
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,do by A187, JORDAN3:41;
A234: Index p,do < len do by A187, JORDAN3:41;
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:11;
A238: 1 <= t by A236, FINSEQ_3:27;
A239: t <= len (Lower_Seq C,n) by A236, FINSEQ_3:27;
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:45;
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:61;
set tt = ((Index p,do) + (((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:41;
0 + (Index ((Gauge C,n) * i2,k),(Lower_Seq C,n)) < len (Lower_Seq C,n) by A13, JORDAN3:41;
then A242: (len (Lower_Seq C,n)) - (Index ((Gauge C,n) * i2,k),(Lower_Seq C,n)) > 0 by XREAL_1:22;
Index p,do < (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,do) + 1 <= (len (Lower_Seq C,n)) -' (Index ((Gauge C,n) * i2,k),(Lower_Seq C,n)) by NAT_1:13;
then Index p,do <= ((len (Lower_Seq C,n)) -' (Index ((Gauge C,n) * i2,k),(Lower_Seq C,n))) - 1 by XREAL_1:21;
then Index p,do <= ((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,do <= (len (Lower_Seq C,n)) - (((Gauge C,n) * i2,k) .. (Lower_Seq C,n)) by A235;
then Index p,do <= (len (Lower_Seq C,n)) -' (((Gauge C,n) * i2,k) .. (Lower_Seq C,n)) by XREAL_0:def 2;
then Index p,do < ((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,do) = LSeg (Lower_Seq C,n),(((Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) -' 1) by A230, A232, A233, JORDAN4:31;
A244: 1 + 1 <= ((Gauge C,n) * i2,k) .. (Lower_Seq C,n) by A235, A241, XREAL_1:9;
then (Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n)) >= (1 + 1) + 1 by A233, XREAL_1:9;
then ((Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) - 1 >= ((1 + 1) + 1) - 1 by XREAL_1:11;
then A245: ((Index p,do) + (((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:27;
now
per cases ( ((Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) -' 1 > 1 + 1 or ((Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) -' 1 = 1 + 1 ) by A245, XXREAL_0:1;
suppose ((Index p,do) + (((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,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) -' 1) by TOPREAL1:def 9;
hence contradiction by A227, A228, A229, A243, XBOOLE_0:3; :: thesis: verum
end;
suppose A247: ((Index p,do) + (((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,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) -' 1)) = {((Lower_Seq C,n) /. 2)} by A28, TOPREAL1:def 8;
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:44;
1 + 1 = ((Index p,do) + (((Gauge C,n) * i2,k) .. (Lower_Seq C,n))) - 1 by A247, XREAL_0:def 2;
then (1 + 1) + 1 = (Index p,do) + (((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:10;
p in rng (Lower_Seq C,n) by A246, A248, PARTFUN2:4;
then p = (Gauge C,n) * i2,k by A40, A249, A250, FINSEQ_5:10;
then ((Gauge C,n) * i2,k) `1 = E-bound (L~ (Cage C,n)) by A248, JORDAN1G:40;
then ((Gauge C,n) * i2,k) `1 = ((Gauge C,n) * (len (Gauge C,n)),j) `1 by A4, A15, A20, JORDAN1A:92;
hence contradiction by A3, A18, A70, JORDAN1G:7; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
then east_halfline (E-max C) c= (L~ godo) ` by SUBSET_1:43;
then consider W being Subset of (TOP-REAL 2) such that
A251: W is_a_component_of (L~ godo) ` and
A252: east_halfline (E-max C) c= W by GOBOARD9:5;
not W is Bounded by A252, JORDAN2C:16, JORDAN2C:129;
then W is_outside_component_of L~ godo by A251, JORDAN2C:def 4;
then W c= UBD (L~ godo) by JORDAN2C:27;
then A253: east_halfline (E-max C) c= UBD (L~ godo) by A252, XBOOLE_1:1;
E-max C in east_halfline (E-max C) by TOPREAL1:45;
then E-max C in UBD (L~ godo) by A253;
then E-max C in LeftComp godo by GOBRD14:46;
then Lower_Arc C meets L~ godo by A142, A143, A144, A152, A162, JORDAN1J:36;
then A254: ( Lower_Arc C meets (L~ go) \/ (L~ pion1) or Lower_Arc C meets L~ do ) by A153, XBOOLE_1:70;
A255: Lower_Arc C c= C by JORDAN6:76;
hence contradiction ; :: thesis: verum
end;
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:71;
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:37;
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, Th14; :: thesis: verum
end;
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:71;
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:37;
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:38; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum