let n be Nat; :: thesis: for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < 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 < i2 & i2 <= i1 & i1 < 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 < i2 & i2 <= i1 & i1 < 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 < i2 and
A2: i2 <= i1 and
A3: i1 < 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: 1 < i1 by A1, A2, XXREAL_0:2;
A11: i2 < len (Gauge (C,n)) by A2, A3, 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 A3, A4, A10, A15, MATRIX_0:30;
A18: [i2,k] in Indices (Gauge (C,n)) by A1, A6, A11, A16, MATRIX_0:30;
A19: [i1,k] in Indices (Gauge (C,n)) by A3, 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, A2, 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: len (Lower_Seq (C,n)) >= 1 + 2 by JORDAN1E:15;
then A28: len (Lower_Seq (C,n)) >= 1 by XXREAL_0:2;
then A29: 1 in dom (Lower_Seq (C,n)) by FINSEQ_3:25;
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A28, FINSEQ_3:25;
then A30: (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 A31: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A1, A18, A25, A30, 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;
A32: [(len (Gauge (C,n))),k] in Indices (Gauge (C,n)) by A6, A16, A24, MATRIX_0:30;
A33: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A29, 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 A34: (Gauge (C,n)) * (i2,k) <> (Lower_Seq (C,n)) . 1 by A2, A3, A18, A32, A33, JORDAN1G:7;
A35: len go >= 1 + 1 by TOPREAL1:def 8;
A36: (Gauge (C,n)) * (i1,j) in rng (Upper_Seq (C,n)) by A3, A4, A10, A14, A15, JORDAN1G:4, JORDAN1J:40;
then A37: go is_sequence_on Gauge (C,n) by JORDAN1G:4, JORDAN1J:38;
A38: len co >= 1 + 1 by TOPREAL1:def 8;
A39: (Gauge (C,n)) * (i2,k) in rng (Lower_Seq (C,n)) by A1, A6, A11, A13, A16, JORDAN1G:5, JORDAN1J:40;
then A40: 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 A35, A37, JGRAPH_1:12, JORDAN8:5;
reconsider co = co as V26() being_S-Seq s.c.c. FinSequence of (TOP-REAL 2) by A38, A40, JGRAPH_1:12, JORDAN8:5;
A41: len go > 1 by A35, NAT_1:13;
then A42: len go in dom go by FINSEQ_3:25;
then A43: go /. (len go) = go . (len go) by PARTFUN1:def 6
.= (Gauge (C,n)) * (i1,j) by A14, JORDAN3:24 ;
len co >= 1 by A38, XXREAL_0:2;
then 1 in dom co by FINSEQ_3:25;
then A44: 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 A42, FINSEQ_3:26;
A45: m + 1 = len go ;
then A46: (len go) -' 1 = m by NAT_D:34;
A47: LSeg (go,m) c= L~ go by TOPREAL3:19;
A48: L~ go c= L~ (Upper_Seq (C,n)) by A14, JORDAN3:41;
then LSeg (go,m) c= L~ (Upper_Seq (C,n)) by A47;
then A49: (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 A35, XREAL_1:19;
then A50: LSeg (go,m) = LSeg ((go /. m),((Gauge (C,n)) * (i1,j))) by A43, A45, 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
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 A51: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;
A52: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A50, 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 A51, A52, XBOOLE_0:def 4; :: thesis: verum
end;
then A53: (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 A49;
A54: LSeg (co,1) c= L~ co by TOPREAL3:19;
A55: L~ co c= L~ (Lower_Seq (C,n)) by A13, JORDAN3:42;
then LSeg (co,1) c= L~ (Lower_Seq (C,n)) by A54;
then A56: (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;
A57: LSeg (co,1) = LSeg (((Gauge (C,n)) * (i2,k)),(co /. (1 + 1))) by A38, A44, 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
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 A58: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;
A59: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A57, 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 A58, A59, XBOOLE_0:def 4; :: thesis: verum
end;
then A60: (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 A56;
A61: go /. 1 = (Upper_Seq (C,n)) /. 1 by A14, SPRECT_3:22
.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;
then A62: go /. 1 = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by JORDAN1F:8
.= co /. (len co) by A13, JORDAN1J:35 ;
A63: rng go c= L~ go by A35, SPPOL_2:18;
A64: rng co c= L~ co by A38, SPPOL_2:18;
A65: {(go /. 1)} c= (L~ go) /\ (L~ co)
proof
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 A66: x = go /. 1 by TARSKI:def 1;
then A67: x in rng go by FINSEQ_6:42;
x in rng co by A62, A66, FINSEQ_6:168;
hence x in (L~ go) /\ (L~ co) by A63, A64, A67, XBOOLE_0:def 4; :: thesis: verum
end;
A68: (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by A29, PARTFUN1:def 6
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
A69: [(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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ go) /\ (L~ co) or x in {(go /. 1)} )
assume A70: x in (L~ go) /\ (L~ co) ; :: thesis: x in {(go /. 1)}
then A71: x in L~ go by XBOOLE_0:def 4;
A72: x in L~ co by A70, XBOOLE_0:def 4;
then x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A48, A55, A71, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;
then A73: ( 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)))
assume x = E-max (L~ (Cage (C,n))) ; :: thesis: contradiction
then A74: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i2,k) by A13, A68, A72, 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 A2, A3, A18, A69, A74, JORDAN1G:7;
hence contradiction by EUCLID:52; :: thesis: verum
end;
hence x in {(go /. 1)} by A61, A73, TARSKI:def 1; :: thesis: verum
end;
then A75: (L~ go) /\ (L~ co) = {(go /. 1)} by A65;
set W2 = go /. 2;
A76: 2 in dom go by A35, FINSEQ_3:25;
A77: now :: thesis: not ((Gauge (C,n)) * (i2,k)) `1 = W-bound (L~ (Cage (C,n)))
assume ((Gauge (C,n)) * (i2,k)) `1 = W-bound (L~ (Cage (C,n))) ; :: thesis: contradiction
then ((Gauge (C,n)) * (1,k)) `1 = ((Gauge (C,n)) * (i2,k)) `1 by A6, A16, A20, JORDAN1A:73;
hence contradiction by A1, A18, A25, JORDAN1G:7; :: thesis: verum
end;
go = mid ((Upper_Seq (C,n)),1,(((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)))) by A36, JORDAN1G:49
.= (Upper_Seq (C,n)) | (((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n))) by A36, FINSEQ_4:21, FINSEQ_6:116 ;
then A78: go /. 2 = (Upper_Seq (C,n)) /. 2 by A76, FINSEQ_4:70;
A79: W-min (L~ (Cage (C,n))) in rng go by A61, FINSEQ_6:42;
set pion = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*>;
A80: 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) )
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;
A81: ((Gauge (C,n)) * (i1,k)) `1 = ((Gauge (C,n)) * (i1,1)) `1 by A3, A6, A10, A16, GOBOARD5:2
.= ((Gauge (C,n)) * (i1,j)) `1 by A3, A4, A10, A15, GOBOARD5:2 ;
((Gauge (C,n)) * (i1,k)) `2 = ((Gauge (C,n)) * (1,k)) `2 by A3, A6, A10, A16, GOBOARD5:1
.= ((Gauge (C,n)) * (i2,k)) `2 by A1, A6, A11, A16, GOBOARD5:1 ;
then A82: (Gauge (C,n)) * (i1,k) = |[(((Gauge (C,n)) * (i1,j)) `1),(((Gauge (C,n)) * (i2,k)) `2)]| by A81, EUCLID:53;
A83: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;
A84: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;
now :: thesis: contradiction
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 A82, TOPREAL3:34;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A85: pion1 is_sequence_on Gauge (C,n) and
A86: pion1 is being_S-Seq and
A87: L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> = L~ pion1 and
A88: <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 1 = pion1 /. 1 and
A89: <*((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
A90: len <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> <= len pion1 by A80, GOBOARD3:2;
reconsider pion1 = pion1 as being_S-Seq FinSequence of (TOP-REAL 2) by A86;
set godo = (go ^' pion1) ^' co;
A91: ((Gauge (C,n)) * (i1,k)) `1 = ((Gauge (C,n)) * (i1,1)) `1 by A3, A6, A10, A16, GOBOARD5:2
.= ((Gauge (C,n)) * (i1,j)) `1 by A3, A4, A10, A15, GOBOARD5:2 ;
A92: ((Gauge (C,n)) * (i2,k)) `1 <= ((Gauge (C,n)) * (i1,k)) `1 by A1, A2, A3, A6, A16, JORDAN1A:18;
then A93: W-bound (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) = ((Gauge (C,n)) * (i2,k)) `1 by SPRECT_1:54;
A94: W-bound (LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) = ((Gauge (C,n)) * (i1,j)) `1 by A91, 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)) * (i2,k)) `1 by A91, A92, A93, A94, XXREAL_0:def 9 ;
then A95: W-bound (L~ pion1) = ((Gauge (C,n)) * (i2,k)) `1 by A87, TOPREAL3:16;
A96: 1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
A97: 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 A98: len (go ^' pion1) >= 1 + 1 by A35, XXREAL_0:2;
then A99: len (go ^' pion1) > 1 + 0 by NAT_1:13;
A100: len ((go ^' pion1) ^' co) >= len (go ^' pion1) by TOPREAL8:7;
then A101: 1 + 1 <= len ((go ^' pion1) ^' co) by A98, XXREAL_0:2;
A102: Upper_Seq (C,n) is_sequence_on Gauge (C,n) by JORDAN1G:4;
A103: go /. (len go) = pion1 /. 1 by A43, A88, FINSEQ_4:18;
then A104: go ^' pion1 is_sequence_on Gauge (C,n) by A37, A85, TOPREAL8:12;
A105: (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 A89, 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 A44, FINSEQ_4:18 ;
then A106: (go ^' pion1) ^' co is_sequence_on Gauge (C,n) by A40, A104, TOPREAL8:12;
LSeg (pion1,1) c= L~ <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> by A87, TOPREAL3:19;
then A107: (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) c= {((Gauge (C,n)) * (i1,j))} by A46, A53, XBOOLE_1:27;
len pion1 >= 2 + 1 by A90, FINSEQ_1:45;
then A108: len pion1 > 1 + 1 by NAT_1:13;
{((Gauge (C,n)) * (i1,j))} c= (LSeg (go,m)) /\ (LSeg (pion1,1))
proof
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 A109: x = (Gauge (C,n)) * (i1,j) by TARSKI:def 1;
A110: (Gauge (C,n)) * (i1,j) in LSeg (go,m) by A50, RLTOPSP1:68;
(Gauge (C,n)) * (i1,j) in LSeg (pion1,1) by A43, A103, A108, TOPREAL1:21;
hence x in (LSeg (go,m)) /\ (LSeg (pion1,1)) by A109, A110, XBOOLE_0:def 4; :: thesis: verum
end;
then (LSeg (go,((len go) -' 1))) /\ (LSeg (pion1,1)) = {(go /. (len go))} by A43, A46, A107;
then A111: go ^' pion1 is unfolded by A103, TOPREAL8:34;
len pion1 >= 2 + 1 by A90, FINSEQ_1:45;
then A112: (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 A112, XREAL_0:def 2 ;
then A113: (len (go ^' pion1)) -' 1 = (len go) + ((len pion1) -' 2) by XREAL_0:def 2;
A114: (len pion1) - 1 >= 1 by A108, XREAL_1:19;
then A115: (len pion1) -' 1 = (len pion1) - 1 by XREAL_0:def 2;
A116: ((len pion1) -' 2) + 1 = ((len pion1) - 2) + 1 by A112, XREAL_0:def 2
.= (len pion1) -' 1 by A114, XREAL_0:def 2 ;
((len pion1) - 1) + 1 <= len pion1 ;
then A117: (len pion1) -' 1 < len pion1 by A115, 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 A87, TOPREAL3:19;
then A118: (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) c= {((Gauge (C,n)) * (i2,k))} by A60, XBOOLE_1:27;
{((Gauge (C,n)) * (i2,k))} c= (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1))
proof
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 A119: x = (Gauge (C,n)) * (i2,k) by TARSKI:def 1;
A120: (Gauge (C,n)) * (i2,k) in LSeg (co,1) by A57, RLTOPSP1:68;
pion1 /. (((len pion1) -' 1) + 1) = <*((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))*> /. 3 by A89, A115, 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 A114, A115, TOPREAL1:21;
hence x in (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) by A119, A120, XBOOLE_0:def 4; :: thesis: verum
end;
then (LSeg (pion1,((len pion1) -' 1))) /\ (LSeg (co,1)) = {((Gauge (C,n)) * (i2,k))} by A118;
then A121: (LSeg ((go ^' pion1),((len go) + ((len pion1) -' 2)))) /\ (LSeg (co,1)) = {((go ^' pion1) /. (len (go ^' pion1)))} by A44, A103, A105, A116, A117, TOPREAL8:31;
A122: not go ^' pion1 is trivial by A98, NAT_D:60;
A123: rng pion1 c= L~ pion1 by A108, SPPOL_2:18;
A124: {(pion1 /. 1)} c= (L~ go) /\ (L~ pion1)
proof
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 A125: x = pion1 /. 1 by TARSKI:def 1;
then A126: x in rng go by A103, FINSEQ_6:168;
x in rng pion1 by A125, FINSEQ_6:42;
hence x in (L~ go) /\ (L~ pion1) by A63, A123, A126, XBOOLE_0:def 4; :: thesis: verum
end;
(L~ go) /\ (L~ pion1) c= {(pion1 /. 1)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ go) /\ (L~ pion1) or x in {(pion1 /. 1)} )
assume A127: x in (L~ go) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. 1)}
then A128: x in L~ go by XBOOLE_0:def 4;
x in L~ pion1 by A127, XBOOLE_0:def 4;
hence x in {(pion1 /. 1)} by A7, A12, A43, A48, A87, A103, A128, XBOOLE_0:def 4; :: thesis: verum
end;
then A129: (L~ go) /\ (L~ pion1) = {(pion1 /. 1)} by A124;
then A130: go ^' pion1 is s.n.c. by A103, JORDAN1J:54;
(rng go) /\ (rng pion1) c= {(pion1 /. 1)} by A63, A123, A129, XBOOLE_1:27;
then A131: go ^' pion1 is one-to-one by JORDAN1J:55;
A132: <*((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 A44, FINSEQ_4:18 ;
A133: {(pion1 /. (len pion1))} c= (L~ co) /\ (L~ pion1)
proof
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 A134: x = pion1 /. (len pion1) by TARSKI:def 1;
then A135: x in rng co by A89, A132, FINSEQ_6:42;
x in rng pion1 by A134, FINSEQ_6:168;
hence x in (L~ co) /\ (L~ pion1) by A64, A123, A135, XBOOLE_0:def 4; :: thesis: verum
end;
(L~ co) /\ (L~ pion1) c= {(pion1 /. (len pion1))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ co) /\ (L~ pion1) or x in {(pion1 /. (len pion1))} )
assume A136: x in (L~ co) /\ (L~ pion1) ; :: thesis: x in {(pion1 /. (len pion1))}
then A137: x in L~ co by XBOOLE_0:def 4;
x in L~ pion1 by A136, XBOOLE_0:def 4;
hence x in {(pion1 /. (len pion1))} by A8, A12, A44, A55, A87, A89, A132, A137, XBOOLE_0:def 4; :: thesis: verum
end;
then A138: (L~ co) /\ (L~ pion1) = {(pion1 /. (len pion1))} by A133;
A139: (L~ (go ^' pion1)) /\ (L~ co) = ((L~ go) \/ (L~ pion1)) /\ (L~ co) by A103, TOPREAL8:35
.= {(go /. 1)} \/ {(co /. 1)} by A75, A89, A132, A138, 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 A62, FINSEQ_6:155;
then reconsider godo = (go ^' pion1) ^' co as V26() standard special_circular_sequence by A101, A105, A106, A111, A113, A121, A122, A130, A131, A139, JORDAN8:4, JORDAN8:5, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;
A140: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def 8;
then A141: Upper_Arc C is connected by JORDAN6:10;
A142: W-min C in Upper_Arc C by A140, TOPREAL1:1;
A143: E-max C in Upper_Arc C by A140, 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 A144: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_6:92;
A145: 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 A144, 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 A144, A145, 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 A144, A145, SPRECT_5:24, XXREAL_0:2;
then A146: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A144, A145, SPRECT_5:25, XXREAL_0:2;
A147: now :: thesis: not ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1
assume A148: ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1 ; :: thesis: contradiction
((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) >= 1 by A36, FINSEQ_4:21;
then ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) = 1 by A148, XXREAL_0:1;
then (Gauge (C,n)) * (i1,j) = (Upper_Seq (C,n)) /. 1 by A36, FINSEQ_5:38;
hence contradiction by A22, A26, JORDAN1F:5; :: thesis: verum
end;
A149: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A150: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by REVROT_1:34;
A151: (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) c= RightComp godo by A101, A106, JORDAN9:27;
A152: L~ godo = (L~ (go ^' pion1)) \/ (L~ co) by A105, TOPREAL8:35
.= ((L~ go) \/ (L~ pion1)) \/ (L~ co) by A103, TOPREAL8:35 ;
A153: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by JORDAN1E:13;
then A154: L~ (Upper_Seq (C,n)) c= L~ (Cage (C,n)) by XBOOLE_1:7;
A155: L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n)) by A153, XBOOLE_1:7;
A156: L~ go c= L~ (Cage (C,n)) by A48, A154;
A157: L~ co c= L~ (Cage (C,n)) by A55, A155;
A158: W-min C in C by SPRECT_1:13;
A159: now :: thesis: not W-min C in L~ godo
assume W-min C in L~ godo ; :: thesis: contradiction
then A160: ( W-min C in (L~ go) \/ (L~ pion1) or W-min C in L~ co ) by A152, 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 A97, JORDAN1H:23
.= right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1,(GoB (Cage (C,n)))) by REVROT_1:28
.= right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1,(Gauge (C,n))) by JORDAN1H:44
.= right_cell (((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))),1,(Gauge (C,n))) by A146, A150, 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 A36, A102, A147, JORDAN1J:52
.= right_cell ((go ^' pion1),1,(Gauge (C,n))) by A41, A104, JORDAN1J:51
.= right_cell (godo,1,(Gauge (C,n))) by A99, A106, JORDAN1J:51 ;
then W-min C in right_cell (godo,1,(Gauge (C,n))) by JORDAN1I:6;
then A161: W-min C in (right_cell (godo,1,(Gauge (C,n)))) \ (L~ godo) by A159, XBOOLE_0:def 5;
A162: godo /. 1 = (go ^' pion1) /. 1 by FINSEQ_6:155
.= W-min (L~ (Cage (C,n))) by A61, FINSEQ_6:155 ;
A163: len (Upper_Seq (C,n)) >= 2 by A21, XXREAL_0:2;
A164: godo /. 2 = (go ^' pion1) /. 2 by A98, FINSEQ_6:159
.= (Upper_Seq (C,n)) /. 2 by A35, A78, FINSEQ_6:159
.= ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) /. 2 by A163, FINSEQ_6:159
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 2 by JORDAN1E:11 ;
A165: (L~ go) \/ (L~ co) is compact by COMPTS_1:10;
W-min (L~ (Cage (C,n))) in (L~ go) \/ (L~ co) by A63, A79, XBOOLE_0:def 3;
then A166: W-min ((L~ go) \/ (L~ co)) = W-min (L~ (Cage (C,n))) by A156, A157, A165, JORDAN1J:21, XBOOLE_1:8;
A167: (W-min ((L~ go) \/ (L~ co))) `1 = W-bound ((L~ go) \/ (L~ co)) by EUCLID:52;
A168: (W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:52;
((Gauge (C,n)) * (i2,k)) `1 >= W-bound (L~ (Cage (C,n))) by A13, A155, PSCOMP_1:24;
then ((Gauge (C,n)) * (i2,k)) `1 > W-bound (L~ (Cage (C,n))) by A77, XXREAL_0:1;
then W-min (((L~ go) \/ (L~ co)) \/ (L~ pion1)) = W-min ((L~ go) \/ (L~ co)) by A95, A165, A166, A167, A168, JORDAN1J:33;
then A169: W-min (L~ godo) = W-min (L~ (Cage (C,n))) by A152, A166, XBOOLE_1:4;
A170: rng godo c= L~ godo by A98, A100, SPPOL_2:18, XXREAL_0:2;
2 in dom godo by A101, FINSEQ_3:25;
then A171: godo /. 2 in rng godo by PARTFUN2:2;
godo /. 2 in W-most (L~ (Cage (C,n))) by A164, JORDAN1I:25;
then (godo /. 2) `1 = (W-min (L~ godo)) `1 by A169, PSCOMP_1:31
.= W-bound (L~ godo) by EUCLID:52 ;
then godo /. 2 in W-most (L~ godo) by A170, A171, SPRECT_2:12;
then (Rotate (godo,(W-min (L~ godo)))) /. 2 in W-most (L~ godo) by A162, A169, 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 A172: (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 ;
A173: 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
A174: p in east_halfline (E-max C) and
A175: p in L~ go by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A174;
p in L~ (Upper_Seq (C,n)) by A48, A175;
then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A154, A174, XBOOLE_0:def 4;
then A176: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;
then A177: p = E-max (L~ (Cage (C,n))) by A48, A175, JORDAN1J:46;
then E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i1,j) by A14, A172, A175, JORDAN1J:43;
then ((Gauge (C,n)) * (i1,j)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),k)) `1 by A6, A16, A20, A176, A177, JORDAN1A:71;
hence contradiction by A3, A17, A32, JORDAN1G:7; :: thesis: verum
end;
now :: thesis: not east_halfline (E-max C) meets L~ godo
assume east_halfline (E-max C) meets L~ godo ; :: thesis: contradiction
then A178: ( east_halfline (E-max C) meets (L~ go) \/ (L~ pion1) or east_halfline (E-max C) meets L~ co ) by A152, 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 A178, XBOOLE_1:70;
suppose east_halfline (E-max C) meets L~ pion1 ; :: thesis: contradiction
then consider p being object such that
A179: p in east_halfline (E-max C) and
A180: p in L~ pion1 by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A179;
A181: now :: thesis: p `1 <= ((Gauge (C,n)) * (i1,j)) `1
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, A87, A180, XBOOLE_0:def 3;
suppose p in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) ; :: thesis: p `1 <= ((Gauge (C,n)) * (i1,j)) `1
hence p `1 <= ((Gauge (C,n)) * (i1,j)) `1 by A91, A92, TOPREAL1:3; :: thesis: verum
end;
suppose p in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) ; :: thesis: p `1 <= ((Gauge (C,n)) * (i1,j)) `1
hence p `1 <= ((Gauge (C,n)) * (i1,j)) `1 by A91, GOBOARD7:5; :: thesis: verum
end;
end;
end;
i1 + 1 <= len (Gauge (C,n)) by A3, NAT_1:13;
then i1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
then A182: i1 <= (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)) * (i1,j)) `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A4, A10, A15, A20, A24, A182, JORDAN1A:18;
then p `1 <= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A181, XXREAL_0:2;
then p `1 <= E-bound C by A24, JORDAN8:12;
then A183: p `1 <= (E-max C) `1 by EUCLID:52;
p `1 >= (E-max C) `1 by A179, TOPREAL1:def 11;
then A184: p `1 = (E-max C) `1 by A183, XXREAL_0:1;
p `2 = (E-max C) `2 by A179, TOPREAL1:def 11;
then p = E-max C by A184, TOPREAL3:6;
hence contradiction by A9, A12, A87, A143, A180, XBOOLE_0:3; :: thesis: verum
end;
suppose east_halfline (E-max C) meets L~ co ; :: thesis: contradiction
then consider p being object such that
A185: p in east_halfline (E-max C) and
A186: p in L~ co by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A185;
p in L~ (Lower_Seq (C,n)) by A55, A186;
then p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A155, A185, XBOOLE_0:def 4;
then A187: p `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50;
A188: (E-max C) `2 = p `2 by A185, TOPREAL1:def 11;
set RC = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));
A189: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by JORDAN1I:7;
A190: 1 + 1 <= len (Lower_Seq (C,n)) by A27, 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 A191: LSeg ((Lower_Seq (C,n)),1) = LSeg ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by A190, SPPOL_2:9;
A192: L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = L~ (Cage (C,n)) by REVROT_1:33;
A193: len (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = len (Cage (C,n)) by FINSEQ_6:179;
A194: 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 ;
A195: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
A196: Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n))))) is_sequence_on Gauge (C,n) by A149, REVROT_1:34;
A197: (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 A192, A195, FINSEQ_6:92;
consider ii, jj being Nat such that
A198: [ii,(jj + 1)] in Indices (Gauge (C,n)) and
A199: [ii,jj] in Indices (Gauge (C,n)) and
A200: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 = (Gauge (C,n)) * (ii,(jj + 1)) and
A201: (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. (1 + 1) = (Gauge (C,n)) * (ii,jj) by A96, A192, A193, A195, A196, FINSEQ_6:92, JORDAN1I:23;
consider jj2 being Nat such that
A202: 1 <= jj2 and
A203: jj2 <= width (Gauge (C,n)) and
A204: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),jj2) by JORDAN1D:25;
A205: 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 A202, A203, MATRIX_0:30;
then A206: ii = len (Gauge (C,n)) by A192, A197, A198, A200, A204, GOBOARD1:5;
A207: 1 <= ii by A198, MATRIX_0:32;
A208: ii <= len (Gauge (C,n)) by A198, MATRIX_0:32;
A209: 1 <= jj + 1 by A198, MATRIX_0:32;
A210: jj + 1 <= width (Gauge (C,n)) by A198, MATRIX_0:32;
A211: 1 <= ii by A199, MATRIX_0:32;
A212: ii <= len (Gauge (C,n)) by A199, MATRIX_0:32;
A213: 1 <= jj by A199, MATRIX_0:32;
A214: jj <= width (Gauge (C,n)) by A199, MATRIX_0:32;
A215: ii + 1 <> ii ;
(jj + 1) + 1 <> jj ;
then A216: right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) = cell ((Gauge (C,n)),(ii -' 1),jj) by A96, A193, A194, A198, A199, A200, A201, A215, GOBOARD5:def 6;
A217: (ii -' 1) + 1 = ii by A207, XREAL_1:235;
ii - 1 >= 4 - 1 by A205, A206, XREAL_1:9;
then A218: ii - 1 >= 1 by XXREAL_0:2;
then A219: 1 <= ii -' 1 by XREAL_0:def 2;
A220: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 <= p `2 by A188, A189, A208, A210, A213, A216, A217, A218, JORDAN9:17;
A221: p `2 <= ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 by A188, A189, A208, A210, A213, A216, A217, A218, JORDAN9:17;
A222: ii -' 1 < len (Gauge (C,n)) by A208, A217, NAT_1:13;
then A223: ((Gauge (C,n)) * ((ii -' 1),jj)) `2 = ((Gauge (C,n)) * (1,jj)) `2 by A213, A214, A219, GOBOARD5:1
.= ((Gauge (C,n)) * (ii,jj)) `2 by A211, A212, A213, A214, GOBOARD5:1 ;
A224: ((Gauge (C,n)) * ((ii -' 1),(jj + 1))) `2 = ((Gauge (C,n)) * (1,(jj + 1))) `2 by A209, A210, A219, A222, GOBOARD5:1
.= ((Gauge (C,n)) * (ii,(jj + 1))) `2 by A207, A208, A209, A210, GOBOARD5:1 ;
A225: ((Gauge (C,n)) * ((len (Gauge (C,n))),jj)) `1 = E-bound (L~ (Cage (C,n))) by A20, A213, A214, JORDAN1A:71;
E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),(jj + 1))) `1 by A20, A209, A210, 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 A187, A200, A201, A206, A220, A221, A223, A224, A225, GOBOARD7:7;
then A226: p in LSeg ((Lower_Seq (C,n)),1) by A96, A191, A193, TOPREAL1:def 3;
A227: p in LSeg (co,(Index (p,co))) by A186, JORDAN3:9;
A228: co = mid ((Lower_Seq (C,n)),(((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))),(len (Lower_Seq (C,n)))) by A39, JORDAN1J:37;
A229: 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A39, FINSEQ_4:21;
A230: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <= len (Lower_Seq (C,n)) by A39, FINSEQ_4:21;
((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) <> len (Lower_Seq (C,n)) by A31, A39, FINSEQ_4:19;
then A231: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) < len (Lower_Seq (C,n)) by A230, XXREAL_0:1;
A232: 1 <= Index (p,co) by A186, JORDAN3:8;
A233: Index (p,co) < len co by A186, JORDAN3:8;
A234: (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A34, A39, JORDAN1J:56;
consider t being Nat such that
A235: t in dom (Lower_Seq (C,n)) and
A236: (Lower_Seq (C,n)) . t = (Gauge (C,n)) * (i2,k) by A39, FINSEQ_2:10;
A237: 1 <= t by A235, FINSEQ_3:25;
A238: t <= len (Lower_Seq (C,n)) by A235, FINSEQ_3:25;
1 < t by A34, A236, A237, XXREAL_0:1;
then (Index (((Gauge (C,n)) * (i2,k)),(Lower_Seq (C,n)))) + 1 = t by A236, A238, JORDAN3:12;
then A239: 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, A236, JORDAN3:26;
set tt = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1;
A240: 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 A241: (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 A233, A239, 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 A241, XREAL_0:def 2;
then Index (p,co) <= (len (Lower_Seq (C,n))) - (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) by A234;
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 A242: 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 A229, A231, A232, JORDAN4:19;
A243: 1 + 1 <= ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) by A234, A240, XREAL_1:7;
then (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) >= (1 + 1) + 1 by A232, 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 A244: ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1 >= 1 + 1 by XREAL_0:def 2;
A245: 2 in dom (Lower_Seq (C,n)) by A190, FINSEQ_3:25;
now :: thesis: contradiction
per 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 A244, XXREAL_0:1;
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 A226, A227, A228, A242, XBOOLE_0:3; :: thesis: verum
end;
suppose A246: ((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 A27, TOPREAL1:def 6;
then p in {((Lower_Seq (C,n)) /. 2)} by A226, A227, A228, A242, XBOOLE_0:def 4;
then A247: p = (Lower_Seq (C,n)) /. 2 by TARSKI:def 1;
then A248: p .. (Lower_Seq (C,n)) = 2 by A245, FINSEQ_5:41;
1 + 1 = ((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) - 1 by A246, XREAL_0:def 2;
then (1 + 1) + 1 = (Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n))) ;
then A249: ((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)) = 2 by A232, A243, JORDAN1E:6;
p in rng (Lower_Seq (C,n)) by A245, A247, PARTFUN2:2;
then p = (Gauge (C,n)) * (i2,k) by A39, A248, A249, FINSEQ_5:9;
then ((Gauge (C,n)) * (i2,k)) `1 = E-bound (L~ (Cage (C,n))) by A247, 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 A2, A3, A18, A69, 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:23;
then consider W being Subset of (TOP-REAL 2) such that
A250: W is_a_component_of (L~ godo) ` and
A251: east_halfline (E-max C) c= W by GOBOARD9:3;
not W is bounded by A251, JORDAN2C:121, RLTOPSP1:42;
then W is_outside_component_of L~ godo by A250, JORDAN2C:def 3;
then W c= UBD (L~ godo) by JORDAN2C:23;
then A252: east_halfline (E-max C) c= UBD (L~ godo) by A251;
E-max C in east_halfline (E-max C) by TOPREAL1:38;
then E-max C in UBD (L~ godo) by A252;
then E-max C in LeftComp godo by GOBRD14:36;
then Upper_Arc C meets L~ godo by A141, A142, A143, A151, A161, JORDAN1J:36;
then A253: ( Upper_Arc C meets (L~ go) \/ (L~ pion1) or Upper_Arc C meets L~ co ) by A152, XBOOLE_1:70;
A254: Upper_Arc C c= C by JORDAN6:61;
hence contradiction ; :: thesis: verum
end;
suppose ((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * (i1,j)) `1 ; :: thesis: contradiction
then A255: 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 A83, 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, A255, Th12; :: thesis: verum
end;
suppose ((Gauge (C,n)) * (i2,k)) `2 = ((Gauge (C,n)) * (i1,j)) `2 ; :: thesis: contradiction
then A256: 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 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,k)),((Gauge (C,n)) * (i2,k))) by XBOOLE_1:12;
hence contradiction by A1, A2, A3, A4, A6, A7, A8, A9, A256, JORDAN15:29; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum