let n be Nat; 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; 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; ( 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
; 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 ;
TARSKI:def 3 ( 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))}
;
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;
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 ;
TARSKI:def 3 ( 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))}
;
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;
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)
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 ;
TARSKI:def 3 ( not x in (L~ go) /\ (L~ co) or x in {(go /. 1)} )
assume A70:
x in (L~ go) /\ (L~ co)
;
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 not x = E-max (L~ (Cage (C,n)))assume
x = E-max (L~ (Cage (C,n)))
;
contradictionthen 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;
verum end;
hence
x in {(go /. 1)}
by A61, A73, TARSKI:def 1;
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 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)))
;
contradictionthen
((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;
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 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;
( 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))*>
;
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;
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 contradictionper 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 )
;
contradictionthen
<*((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 ;
TARSKI:def 3 ( 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))}
;
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;
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 ;
TARSKI:def 3 ( 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))}
;
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;
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)
(L~ go) /\ (L~ pion1) c= {(pion1 /. 1)}
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)
(L~ co) /\ (L~ pion1) c= {(pion1 /. (len pion1))}
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 not ((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1assume A148:
((Gauge (C,n)) * (i1,j)) .. (Upper_Seq (C,n)) <= 1
;
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;
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;
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
;
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;
verum
end; now not east_halfline (E-max C) meets L~ godoassume
east_halfline (E-max C) meets L~ godo
;
contradictionthen 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
;
contradictionthen 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 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;
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;
verum end; suppose
east_halfline (E-max C) meets L~ co
;
contradictionthen 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 contradictionper 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
;
contradictionthen
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;
verum end; suppose A246:
((Index (p,co)) + (((Gauge (C,n)) * (i2,k)) .. (Lower_Seq (C,n)))) -' 1
= 1
+ 1
;
contradictionthen
(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;
verum end; end; end; hence
contradiction
;
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
;
verum end; suppose
((Gauge (C,n)) * (i2,k)) `1 = ((Gauge (C,n)) * (i1,j)) `1
;
contradictionthen 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;
verum end; suppose
((Gauge (C,n)) * (i2,k)) `2 = ((Gauge (C,n)) * (i1,j)) `2
;
contradictionthen 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;
verum end; end; end;
hence
contradiction
; verum