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)) * (i2,k))} & ((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)) * (i1,j))} 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 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)) * (i2,k))} & ((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)) * (i1,j))} 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 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)) * (i2,k))} & ((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)) * (i1,j))} 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 < 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)) * (i2,k))} 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)) * (i1,j))} 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 Gi1k = (Gauge (C,n)) * (i1,k);
set Gik = (Gauge (C,n)) * (i2,k);
A10: 1 <= k by ;
A11: i2 < len (Gauge (C,n)) by ;
then A12: [i2,k] in Indices (Gauge (C,n)) by ;
set Wmin = W-min (L~ (Cage (C,n)));
set Wbo = W-bound (L~ (Cage (C,n)));
A13: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
set go = R_Cut ((Upper_Seq (C,n)),((Gauge (C,n)) * (i2,k)));
A14: 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 A15: (Upper_Seq (C,n)) . 1 = (Upper_Seq (C,n)) /. 1 by PARTFUN1:def 6
.= W-min (L~ (Cage (C,n))) by JORDAN1F:5 ;
set Gij = (Gauge (C,n)) * (i1,j);
set co = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i1,j)));
(Gauge (C,n)) * (i1,j) in {((Gauge (C,n)) * (i1,j))} by TARSKI:def 1;
then A16: (Gauge (C,n)) * (i1,j) in L~ (Lower_Seq (C,n)) by ;
A17: 1 < i1 by ;
then A18: ((Gauge (C,n)) * (i1,k)) `2 = ((Gauge (C,n)) * (1,k)) `2 by
.= ((Gauge (C,n)) * (i2,k)) `2 by ;
A19: j <= width (Gauge (C,n)) by ;
then A20: [i1,j] in Indices (Gauge (C,n)) by ;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A21: len (Gauge (C,n)) >= 1 by XXREAL_0:2;
then A22: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by ;
A23: [1,k] in Indices (Gauge (C,n)) by ;
A24: 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 ;
hence contradiction by A1, A12, A23, JORDAN1G:7; :: thesis: verum
end;
A25: [i1,j] in Indices (Gauge (C,n)) by ;
set pion = <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*>;
A26: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))) by RLTOPSP1:68;
set LA = Lower_Arc C;
A27: (Gauge (C,n)) * (i1,k) in LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k))) by RLTOPSP1:68;
A28: [i1,k] in Indices (Gauge (C,n)) by ;
A29: now :: thesis: for n being Nat st n in dom <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> holds
ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> /. n = (Gauge (C,n)) * (i,j) )
let n be Nat; :: thesis: ( n in dom <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> implies ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> /. n = (Gauge (C,n)) * (i,j) ) )

assume n in dom <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (Gauge (C,n)) & <*((Gauge (C,n)) * (i2,k)),((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i1,j))*> /. n = (Gauge (C,n)) * (i,j) )

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