Copyright (c) 2002 Association of Mizar Users
environ
vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, GROUP_2, REALSET1,
JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1, COMPTS_1, TOPREAL1,
SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1, MATRIX_1, GOBOARD9,
PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1, ARYTM_1, FINSEQ_6,
GOBOARD2, GRAPH_2, ORDINAL2, LATTICES, SEQ_2, FUNCT_5, ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
REAL_1, NAT_1, SQUARE_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_5,
SEQ_4, MATRIX_1, REALSET1, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC,
RCOMP_1, TOPREAL2, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1,
SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13,
SPPOL_1, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A,
JORDAN1E;
constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, SQUARE_1, FINSEQ_4,
JORDAN1, JORDAN3, TOPREAL2, JORDAN5C, GRAPH_2, SPRECT_1, GOBOARD2,
JORDAN1E, RCOMP_1, WSIERP_1, JORDAN1H, ENUMSET1, INT_1;
clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1,
SPRECT_3, GOBOARD2, SPPOL_2, JORDAN1A, JORDAN1B, JORDAN1E, GOBRD11,
XBOOLE_0, SPRECT_4, BORSUK_2, PSCOMP_1, JORDAN1J, MEMBERED, NUMBERS,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, AXIOMS,
REAL_1, SPPOL_2, TARSKI, JORDAN3, SQUARE_1, PSCOMP_1, FINSEQ_5, FINSEQ_6,
GOBOARD7, TOPREAL1, BINARITH, AMI_5, GOBOARD5, SPRECT_2, SPPOL_1,
FUNCT_2, GOBOARD9, FINSEQ_2, SUBSET_1, JORDAN4, SPRECT_3, TOPREAL3,
JORDAN8, PARTFUN2, SPRECT_1, XBOOLE_0, XBOOLE_1, ZFMISC_1, SEQ_4,
GOBRD14, TOPREAL6, JORDAN2C, PRE_TOPC, JORDAN6, JORDAN9, JORDAN1H,
JORDAN1A, JORDAN1C, JORDAN1E, JORDAN10, JGRAPH_1, REVROT_1, RCOMP_1,
COMPTS_1, ENUMSET1, JORDAN1B, JORDAN1F, JORDAN1G, JORDAN1I, JORDAN1J,
GOBOARD3, TOPREAL8, AMISTD_1, GRAPH_2, SPRECT_5, JORDAN1D, XCMPLX_1;
begin
reserve n for Nat;
theorem
for A,B be Subset of TOP-REAL 2 st A meets B holds
proj1.:A meets proj1.:B
proof
let A,B be Subset of TOP-REAL 2;
assume A meets B;
then consider e be set such that
A1: e in A and
A2: e in B by XBOOLE_0:3;
reconsider e as Point of TOP-REAL 2 by A1;
A3: e`1 = proj1.e by PSCOMP_1:def 28;
then A4: e`1 in proj1.:A by A1,FUNCT_2:43;
e`1 in proj1.:B by A2,A3,FUNCT_2:43;
hence proj1.:A meets proj1.:B by A4,XBOOLE_0:3;
end;
theorem
for A,B be Subset of TOP-REAL 2
for s be real number st
A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1.:A misses proj1.:B
proof
let A,B be Subset of TOP-REAL 2;
let s be real number such that
A1: A misses B and
A2: A c= Horizontal_Line s and
A3: B c= Horizontal_Line s;
assume proj1.:A meets proj1.:B;
then consider e be set such that
A4: e in proj1.:A and
A5: e in proj1.:B by XBOOLE_0:3;
reconsider e as Real by A4;
consider c being Point of TOP-REAL 2 such that
A6: c in A and
A7: e = proj1.c by A4,FUNCT_2:116;
consider d be Point of TOP-REAL 2 such that
A8: d in B and
A9: e = proj1.d by A5,FUNCT_2:116;
c`2 = s & d`2 = s by A2,A3,A6,A8,JORDAN6:35;
then c = |[c`1,d`2]| by EUCLID:57
.= |[e,d`2]| by A7,PSCOMP_1:def 28
.= |[d`1,d`2]| by A9,PSCOMP_1:def 28
.= d by EUCLID:57;
hence contradiction by A1,A6,A8,XBOOLE_0:3;
end;
theorem Th3:
for S be closed Subset of TOP-REAL 2 st S is Bounded holds
proj1.:S is closed
proof
let S be closed Subset of TOP-REAL 2;
assume S is Bounded;
then Cl(proj1.:S) = proj1.:Cl S by TOPREAL6:92
.= proj1.:S by PRE_TOPC:52;
hence proj1.:S is closed;
end;
theorem Th4:
for S be compact Subset of TOP-REAL 2 holds proj1.:S is compact
proof
let S being compact Subset of TOP-REAL 2;
A1: S is Bounded closed by JORDAN2C:73;
then A2: proj1.:S is closed by Th3;
proj1.:S is bounded by A1,JORDAN1C:4;
hence proj1.:S is compact by A2,RCOMP_1:29;
end;
theorem Th5:
for p,q,p1,q1 be Point of TOP-REAL 2 st
LSeg(p,q) is vertical & LSeg(p1,q1) is vertical & p`1 = p1`1 &
p`2 <= p1`2 & p1`2 <= q1`2 & q1`2 <= q`2 holds
LSeg(p1,q1) c= LSeg(p,q)
proof
let p,q,p1,q1 be Point of TOP-REAL 2;
assume that
A1: LSeg(p,q) is vertical and
A2: LSeg(p1,q1) is vertical and
A3: p`1 = p1`1 and
A4: p`2 <= p1`2 & p1`2 <= q1`2 & q1`2 <= q`2;
let x be set;
assume A5: x in LSeg(p1,q1);
then reconsider r=x as Point of TOP-REAL 2;
A6: p1`1 = r`1 by A2,A5,SPRECT_3:20;
A7: p`1 = q`1 by A1,SPPOL_1:37;
p1`2 <= r`2 & r`2 <= q1`2 by A4,A5,TOPREAL1:10;
then p`2 <= r`2 & r`2 <= q`2 by A4,AXIOMS:22;
hence x in LSeg(p,q) by A3,A6,A7,GOBOARD7:8;
end;
theorem Th6:
for p,q,p1,q1 be Point of TOP-REAL 2 st
LSeg(p,q) is horizontal & LSeg(p1,q1) is horizontal & p`2 = p1`2 &
p`1 <= p1`1 & p1`1 <= q1`1 & q1`1 <= q`1 holds
LSeg(p1,q1) c= LSeg(p,q)
proof
let p,q,p1,q1 be Point of TOP-REAL 2;
assume that
A1: LSeg(p,q) is horizontal and
A2: LSeg(p1,q1) is horizontal and
A3: p`2 = p1`2 and
A4: p`1 <= p1`1 & p1`1 <= q1`1 & q1`1 <= q`1;
let x be set;
assume A5: x in LSeg(p1,q1);
then reconsider r=x as Point of TOP-REAL 2;
A6: p1`2 = r`2 by A2,A5,SPRECT_3:19;
A7: p`2 = q`2 by A1,SPPOL_1:36;
p1`1 <= r`1 & r`1 <= q1`1 by A4,A5,TOPREAL1:9;
then p`1 <= r`1 & r`1 <= q`1 by A4,AXIOMS:22;
hence x in LSeg(p,q) by A3,A6,A7,GOBOARD7:9;
end;
theorem Th7:
for G be Go-board
for i,j,k,j1,k1 be Nat st
1 <= i & i <= len G &
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg(G*(i,j1),G*(i,k1)) c= LSeg(G*(i,j),G*(i,k))
proof
let G be Go-board;
let i,j,k,j1,k1 be Nat;
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G;
j <= k1 & k1 <= width G & 1 <= j1 & j1 <= k by A2,AXIOMS:22;
then A3: j <= width G & 1 <= k by AXIOMS:22;
then G*(i,j)`1 = G*(i,1)`1 by A1,A2,GOBOARD5:3
.= G*(i,k)`1 by A1,A2,A3,GOBOARD5:3;
then A4: LSeg(G*(i,j),G*(i,k)) is vertical by SPPOL_1:37;
j1 <= k & j <= k1 by A2,AXIOMS:22;
then A5: 1 <= j1 & j1 <= width G & 1 <= k1 & k1 <= width G by A2,AXIOMS:22;
then G*(i,j1)`1 = G*(i,1)`1 by A1,GOBOARD5:3
.= G*(i,k1)`1 by A1,A5,GOBOARD5:3;
then A6: LSeg(G*(i,j1),G*(i,k1)) is vertical by SPPOL_1:37;
A7: G*(i,j)`1 = G*(i,1)`1 by A1,A2,A3,GOBOARD5:3
.= G*(i,j1)`1 by A1,A5,GOBOARD5:3;
A8: G*(i,j)`2 <= G*(i,j1)`2 by A1,A2,A5,SPRECT_3:24;
A9: G*(i,j1)`2 <= G*(i,k1)`2 by A1,A2,A5,SPRECT_3:24;
G*(i,k1)`2 <= G*(i,k)`2 by A1,A2,A5,SPRECT_3:24;
hence LSeg(G*(i,j1),G*(i,k1)) c= LSeg(G*(i,j),G*(i,k))
by A4,A6,A7,A8,A9,Th5;
end;
theorem Th8:
for G be Go-board
for i,j,k,j1,k1 be Nat st
1 <= i & i <= width G &
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg(G*(j1,i),G*(k1,i)) c= LSeg(G*(j,i),G*(k,i))
proof
let G be Go-board;
let i,j,k,j1,k1 be Nat;
assume that
A1: 1 <= i & i <= width G and
A2: 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G;
j <= k1 & k1 <= len G & 1 <= j1 & j1 <= k by A2,AXIOMS:22;
then A3: j <= len G & 1 <= k by AXIOMS:22;
then G*(j,i)`2 = G*(1,i)`2 by A1,A2,GOBOARD5:2
.= G*(k,i)`2 by A1,A2,A3,GOBOARD5:2;
then A4: LSeg(G*(j,i),G*(k,i)) is horizontal by SPPOL_1:36;
j1 <= k & j <= k1 by A2,AXIOMS:22;
then A5: 1 <= j1 & j1 <= len G & 1 <= k1 & k1 <= len G by A2,AXIOMS:22;
then G*(j1,i)`2 = G*(1,i)`2 by A1,GOBOARD5:2
.= G*(k1,i)`2 by A1,A5,GOBOARD5:2;
then A6: LSeg(G*(j1,i),G*(k1,i)) is horizontal by SPPOL_1:36;
A7: G*(j,i)`2 = G*(1,i)`2 by A1,A2,A3,GOBOARD5:2
.= G*(j1,i)`2 by A1,A5,GOBOARD5:2;
A8: G*(j,i)`1 <= G*(j1,i)`1 by A1,A2,A5,SPRECT_3:25;
A9: G*(j1,i)`1 <= G*(k1,i)`1 by A1,A2,A5,SPRECT_3:25;
G*(k1,i)`1 <= G*(k,i)`1 by A1,A2,A5,SPRECT_3:25;
hence LSeg(G*(j1,i),G*(k1,i)) c= LSeg(G*(j,i),G*(k,i))
by A4,A6,A7,A8,A9,Th6;
end;
theorem
for G be Go-board
for j,k,j1,k1 be Nat st
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg(G*(Center G,j1),G*(Center G,k1)) c=
LSeg(G*(Center G,j),G*(Center G,k))
proof
let G be Go-board;
let j,k,j1,k1 be Nat;
assume A1: 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G;
1 <= Center G & Center G <= len G by JORDAN1B:12,14;
hence LSeg(G*(Center G,j1),G*(Center G,k1)) c=
LSeg(G*(Center G,j),G*(Center G,k)) by A1,Th7;
end;
theorem
for G be Go-board st len G = width G
for j,k,j1,k1 be Nat st
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg(G*(j1,Center G),G*(k1,Center G)) c=
LSeg(G*(j,Center G),G*(k,Center G))
proof
let G be Go-board;
assume A1: len G = width G;
let j,k,j1,k1 be Nat;
assume A2: 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G;
1 <= Center G & Center G <= width G by A1,JORDAN1B:12,14;
hence LSeg(G*(j1,Center G),G*(k1,Center G)) c=
LSeg(G*(j,Center G),G*(k,Center G)) by A2,Th8;
end;
theorem Th11:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w2 = sup(proj2.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set q = |[s,w2]|;
A4: j <= width G by A2,AXIOMS:22;
then A5: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A6: k >= 1 by A2,AXIOMS:22;
then A7: G*(i,k)`1 = s by A1,A2,GOBOARD5:3;
A8: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A9: G*(i,j) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A10: LSeg(G*(i,j),G*(i,k)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
[i,k] in Indices G by A1,A2,A6,GOBOARD7:10;
then consider j1 be Nat such that
A11: j <= j1 & j1 <= k and
A12: G*(i,j1)`2 = w2 by A2,A5,A8,A10,JORDAN1F:2;
A13: 1 <= j1 & j1 <= width G by A2,A11,AXIOMS:22;
then A14: G*(i,j1)`1 = s by A1,GOBOARD5:3;
then A15: q = G*(i,j1) by A12,EUCLID:57;
take j1;
thus j <= j1 & j1 <= k by A11;
A16: q`2 <= e`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A9,PSCOMP_1:64,XBOOLE_0:def
3;
consider pp be set such that
A17: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A17;
pp in LSeg(NW-corner X, NE-corner X)/\X by A17,PSCOMP_1:def 39;
then A18: pp in X by XBOOLE_0:def 3;
then A19: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A20: pp in LSeg(G*(i,j),G*(i,k)) by A18,XBOOLE_0:def 3;
f`1 = e`1 by A1,A2,A4,A7,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A21: pp`1 = q`1 by A7,A14,A15,A20,SPRECT_3:20;
q`2 = N-bound X by A12,A15,SPRECT_1:50
.= (N-min X)`2 by PSCOMP_1:94
.= pp`2 by A17,PSCOMP_1:98;
then A22: q in L~Lower_Seq(C,n) by A19,A21,TOPREAL3:11;
for x be set holds
x in LSeg(e,q) /\ L~Lower_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(e,q) /\ L~Lower_Seq(C,n) implies x = q
proof
assume A23: x in LSeg(e,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A24: pp in LSeg(e,q) by A23,XBOOLE_0:def 3;
then A25: pp`1 = q`1 by A7,A14,A15,GOBOARD7:5;
A26: pp`2 >= q`2 by A16,A24,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A27: f`1 = q`1 by A1,A2,A4,A14,A15,GOBOARD5:3;
f`2 <= q`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
then A28: q in LSeg(e,f) by A7,A14,A15,A16,A27,GOBOARD7:8;
e in LSeg(f,e) by TOPREAL1:6;
then A29: LSeg(e,q) c= LSeg(f,e) by A28,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A30: E0 is bounded_above by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A23,XBOOLE_0:def 3;
then pp in EE by A24,A29,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then q`2 >= pp`2 by A12,A15,A30,SEQ_4:def 4;
then pp`2 = q`2 by A26,AXIOMS:21;
hence x = q by A25,TOPREAL3:11;
end;
assume A31: x = q;
then x in LSeg(e,q) by TOPREAL1:6;
hence x in LSeg(e,q) /\ L~Lower_Seq(C,n) by A22,A31,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} by A15,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w1 = inf(proj2.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set p = |[s,w1]|;
A4: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A5: G*(i,k) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A6: LSeg(G*(i,j),G*(i,k)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
A7: j <= width G by A2,AXIOMS:22;
then A8: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A9: k >= 1 by A2,AXIOMS:22;
then [i,k] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A10: j <= k1 & k1 <= k and
A11: G*(i,k1)`2 = w1 by A2,A4,A6,A8,JORDAN1F:1;
A12: 1 <= k1 & k1 <= width G by A2,A10,AXIOMS:22;
then A13: G*(i,k1)`1 = s by A1,GOBOARD5:3;
then A14: p = G*(i,k1) by A11,EUCLID:57;
take k1;
thus j <= k1 & k1 <= k by A10;
A15: f`2 <= p`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
A16: f`1 = p`1 by A1,A2,A7,A13,A14,GOBOARD5:3;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A5,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A17: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A17;
pp in LSeg(SW-corner X, SE-corner X)/\X by A17,PSCOMP_1:def 41;
then A18: pp in X by XBOOLE_0:def 3;
then A19: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A20: pp in LSeg(G*(i,j),G*(i,k)) by A18,XBOOLE_0:def 3;
f`1 = s by A1,A2,A7,GOBOARD5:3
.= e`1 by A1,A2,A9,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A21: pp`1 = p`1 by A16,A20,SPRECT_3:20;
p`2 = S-bound X by A11,A14,SPRECT_1:49
.= (S-min X)`2 by PSCOMP_1:114
.= pp`2 by A17,PSCOMP_1:118;
then A22: p in L~Upper_Seq(C,n) by A19,A21,TOPREAL3:11;
for x be set holds
x in LSeg(p,f) /\ L~Upper_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,f) /\ L~Upper_Seq(C,n) implies x = p
proof
assume A23: x in LSeg(p,f) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A24: pp in LSeg(p,f) by A23,XBOOLE_0:def 3;
then A25: pp`1 = p`1 by A16,GOBOARD7:5;
A26: pp`2 <= p`2 by A15,A24,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A27: f in LSeg(f,e) by TOPREAL1:6;
A28: f`1 = p`1 by A1,A2,A7,A13,A14,GOBOARD5:3;
A29: e`1 = p`1 by A1,A2,A9,A13,A14,GOBOARD5:3;
A30: f`2 <= p`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
p`2 <= e`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
then p in LSeg(f,e) by A28,A29,A30,GOBOARD7:8;
then A31: LSeg(p,f) c= LSeg(f,e) by A27,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A32: E0 is bounded_below by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A23,XBOOLE_0:def 3;
then pp in EE by A24,A31,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then p`2 <= pp`2 by A11,A14,A32,SEQ_4:def 5;
then pp`2 = p`2 by A26,AXIOMS:21;
hence x = p by A25,TOPREAL3:11;
end;
assume A33: x = p;
then x in LSeg(p,f) by TOPREAL1:6;
hence x in LSeg(p,f) /\ L~Upper_Seq(C,n) by A22,A33,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A14,TARSKI:def 1;
end;
theorem Th13:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) and
A4: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w1 = inf(proj2.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set p = |[s,w1]|;
set w2 = sup(proj2.:(LSeg(f,p) /\ L~Lower_Seq(C,n)));
set q = |[s,w2]|;
A5: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A6: G*(i,k) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A7: LSeg(G*(i,j),G*(i,k)) meets L~Upper_Seq(C,n) by A4,XBOOLE_0:3;
A8: j <= width G by A2,AXIOMS:22;
then A9: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A10: k >= 1 by A2,AXIOMS:22;
then [i,k] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A11: j <= k1 & k1 <= k and
A12: G*(i,k1)`2 = w1 by A2,A5,A7,A9,JORDAN1F:1;
A13: 1 <= k1 & k1 <= width G by A2,A11,AXIOMS:22;
then A14: G*(i,k1)`1 = s by A1,GOBOARD5:3;
then A15: p = G*(i,k1) by A12,EUCLID:57;
A16: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A17: G*(i,j) in LSeg(G*(i,j),G*(i,k1)) by TOPREAL1:6;
then A18: LSeg(G*(i,j),G*(i,k1)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
[i,k1] in Indices G by A1,A13,GOBOARD7:10;
then consider j1 be Nat such that
A19: j <= j1 & j1 <= k1 and
A20: G*(i,j1)`2 = w2 by A9,A11,A15,A16,A18,JORDAN1F:2;
A21: 1 <= j1 & j1 <= width G by A2,A13,A19,AXIOMS:22;
then A22: G*(i,j1)`1 = s by A1,GOBOARD5:3;
then A23: q = G*(i,j1) by A20,EUCLID:57;
take j1,k1;
thus j <= j1 & j1 <= k1 & k1 <= k by A11,A19;
A24: q`2 <= p`2 by A1,A13,A15,A19,A21,A23,SPRECT_3:24;
set X = LSeg(G*(i,j),G*(i,k1)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A17,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A25: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A25;
pp in LSeg(NW-corner X, NE-corner X)/\X by A25,PSCOMP_1:def 39;
then A26: pp in X by XBOOLE_0:def 3;
then A27: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A28: pp in LSeg(G*(i,j),G*(i,k1)) by A26,XBOOLE_0:def 3;
A29: f`1 = p`1 by A1,A2,A8,A14,A15,GOBOARD5:3;
then LSeg(f,p) is vertical by SPPOL_1:37;
then A30: pp`1 = q`1 by A14,A15,A22,A23,A28,SPRECT_3:20;
q`2 = N-bound X by A15,A20,A23,SPRECT_1:50
.= (N-min X)`2 by PSCOMP_1:94
.= pp`2 by A25,PSCOMP_1:98;
then A31: q in L~Lower_Seq(C,n) by A27,A30,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Lower_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(p,q) /\ L~Lower_Seq(C,n) implies x = q
proof
assume A32: x in LSeg(p,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A33: pp in LSeg(p,q) by A32,XBOOLE_0:def 3;
then A34: pp`1 = q`1 by A14,A15,A22,A23,GOBOARD7:5;
A35: pp`2 >= q`2 by A24,A33,TOPREAL1:10;
reconsider EE = LSeg(f,p) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A36: f`1 = q`1 by A1,A2,A8,A22,A23,GOBOARD5:3;
f`2 <= q`2 by A1,A2,A19,A21,A23,SPRECT_3:24;
then A37: q in LSeg(p,f) by A14,A15,A22,A23,A24,A36,GOBOARD7:8;
p in LSeg(f,p) by TOPREAL1:6;
then A38: LSeg(p,q) c= LSeg(f,p) by A37,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A39: E0 is bounded_above by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A32,XBOOLE_0:def 3;
then pp in EE by A33,A38,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then q`2 >= pp`2 by A20,A23,A39,SEQ_4:def 4;
then pp`2 = q`2 by A35,AXIOMS:21;
hence x = q by A34,TOPREAL3:11;
end;
assume A40: x = q;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Lower_Seq(C,n) by A31,A40,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),
Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} by A15,A23,TARSKI:def 1;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A4,A6,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A41: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A41;
pp in LSeg(SW-corner X, SE-corner X)/\X by A41,PSCOMP_1:def 41;
then A42: pp in X by XBOOLE_0:def 3;
then A43: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A44: pp in LSeg(G*(i,j),G*(i,k)) by A42,XBOOLE_0:def 3;
f`1 = s by A1,A2,A8,GOBOARD5:3
.= e`1 by A1,A2,A10,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A45: pp`1 = p`1 by A29,A44,SPRECT_3:20;
p`2 = S-bound X by A12,A15,SPRECT_1:49
.= (S-min X)`2 by PSCOMP_1:114
.= pp`2 by A41,PSCOMP_1:118;
then A46: p in L~Upper_Seq(C,n) by A43,A45,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Upper_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,q) /\ L~Upper_Seq(C,n) implies x = p
proof
assume A47: x in LSeg(p,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A48: pp in LSeg(p,q) by A47,XBOOLE_0:def 3;
then A49: pp`1 = p`1 by A14,A15,A22,A23,GOBOARD7:5;
A50: pp`2 <= p`2 by A24,A48,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A51: f`1 = q`1 by A1,A2,A8,A22,A23,GOBOARD5:3;
A52: e`1 = q`1 by A1,A2,A10,A22,A23,GOBOARD5:3;
A53: f`2 <= q`2 by A1,A2,A19,A21,A23,SPRECT_3:24;
j1 <= k by A11,A19,AXIOMS:22;
then q`2 <= e`2 by A1,A2,A21,A23,SPRECT_3:24;
then A54: q in LSeg(f,e) by A51,A52,A53,GOBOARD7:8;
A55: f`1 = p`1 by A1,A2,A8,A14,A15,GOBOARD5:3;
A56: e`1 = p`1 by A1,A2,A10,A14,A15,GOBOARD5:3;
A57: f`2 <= p`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
p`2 <= e`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
then p in LSeg(f,e) by A55,A56,A57,GOBOARD7:8;
then A58: LSeg(p,q) c= LSeg(f,e) by A54,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A59: E0 is bounded_below by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A47,XBOOLE_0:def 3;
then pp in EE by A48,A58,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then p`2 <= pp`2 by A12,A15,A59,SEQ_4:def 5;
then pp`2 = p`2 by A50,AXIOMS:21;
hence x = p by A49,TOPREAL3:11;
end;
assume A60: x = p;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Upper_Seq(C,n) by A46,A60,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),
Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A15,A23,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(j,i) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w2 = sup(proj1.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set q = |[w2,s]|;
A4: len G = width G by JORDAN8:def 1;
then A5: j <= width G by A1,AXIOMS:22;
then A6: [j,i] in Indices G by A1,A2,A4,GOBOARD7:10;
A7: k >= 1 by A1,AXIOMS:22;
then A8: G*(k,i)`2 = s by A1,A2,GOBOARD5:2;
A9: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A10: G*(j,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A11: LSeg(G*(j,i),G*(k,i)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
[k,i] in Indices G by A1,A2,A7,GOBOARD7:10;
then consider j1 be Nat such that
A12: j <= j1 & j1 <= k and
A13: G*(j1,i)`1 = w2 by A1,A6,A9,A11,JORDAN1F:4;
A14: 1 <= j1 & j1 <= width G by A1,A4,A12,AXIOMS:22;
then A15: G*(j1,i)`2 = s by A2,A4,GOBOARD5:2;
then A16: q = G*(j1,i) by A13,EUCLID:57;
take j1;
thus j <= j1 & j1 <= k by A12;
A17: q`1 <= e`1 by A1,A2,A12,A14,A16,SPRECT_3:25;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A10,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A18: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A18;
pp in LSeg(SE-corner X, NE-corner X)/\X by A18,PSCOMP_1:def 40;
then A19: pp in X by XBOOLE_0:def 3;
then A20: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A21: pp in LSeg(G*(j,i),G*(k,i)) by A19,XBOOLE_0:def 3;
f`2 = e`2 by A1,A2,A4,A5,A8,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A22: pp`2 = q`2 by A8,A15,A16,A21,SPRECT_3:19;
q`1 = E-bound X by A13,A16,SPRECT_1:51
.= (E-min X)`1 by PSCOMP_1:104
.= pp`1 by A18,PSCOMP_1:108;
then A23: q in L~Lower_Seq(C,n) by A20,A22,TOPREAL3:11;
for x be set holds
x in LSeg(e,q) /\ L~Lower_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(e,q) /\ L~Lower_Seq(C,n) implies x = q
proof
assume A24: x in LSeg(e,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A25: pp in LSeg(e,q) by A24,XBOOLE_0:def 3;
then A26: pp`2 = q`2 by A8,A15,A16,GOBOARD7:6;
A27: pp`1 >= q`1 by A17,A25,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A28: f`2 = q`2 by A1,A2,A4,A5,A15,A16,GOBOARD5:2;
f`1 <= q`1 by A1,A2,A4,A12,A14,A16,SPRECT_3:25;
then A29: q in LSeg(e,f) by A8,A15,A16,A17,A28,GOBOARD7:9;
e in LSeg(f,e) by TOPREAL1:6;
then A30: LSeg(e,q) c= LSeg(f,e) by A29,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A31: E0 is bounded_above by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A24,XBOOLE_0:def 3;
then pp in EE by A25,A30,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then q`1 >= pp`1 by A13,A16,A31,SEQ_4:def 4;
then pp`1 = q`1 by A27,AXIOMS:21;
hence x = q by A26,TOPREAL3:11;
end;
assume A32: x = q;
then x in LSeg(e,q) by TOPREAL1:6;
hence x in LSeg(e,q) /\ L~Lower_Seq(C,n) by A23,A32,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)} by A16,TARSKI:def 1;
end;
theorem Th15:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(k,i) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w1 = inf(proj1.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set p = |[w1,s]|;
A4: len G = width G by JORDAN8:def 1;
A5: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A6: G*(k,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A7: LSeg(G*(j,i),G*(k,i)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
A8: j <= width G by A1,A4,AXIOMS:22;
then A9: [j,i] in Indices G by A1,A2,A4,GOBOARD7:10;
A10: k >= 1 by A1,AXIOMS:22;
then [k,i] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A11: j <= k1 & k1 <= k and
A12: G*(k1,i)`1 = w1 by A1,A5,A7,A9,JORDAN1F:3;
A13: 1 <= k1 & k1 <= width G by A1,A4,A11,AXIOMS:22;
then A14: G*(k1,i)`2 = s by A2,A4,GOBOARD5:2;
then A15: p = G*(k1,i) by A12,EUCLID:57;
take k1;
thus j <= k1 & k1 <= k by A11;
A16: f`1 <= p`1 by A1,A2,A4,A11,A13,A15,SPRECT_3:25;
A17: f`2 = p`2 by A1,A2,A4,A8,A14,A15,GOBOARD5:2;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A6,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A18: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A18;
pp in LSeg(SW-corner X, NW-corner X)/\X by A18,PSCOMP_1:def 38;
then A19: pp in X by XBOOLE_0:def 3;
then A20: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A21: pp in LSeg(G*(j,i),G*(k,i)) by A19,XBOOLE_0:def 3;
f`2 = s by A1,A2,A4,A8,GOBOARD5:2
.= e`2 by A1,A2,A10,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A22: pp`2 = p`2 by A17,A21,SPRECT_3:19;
p`1 = W-bound X by A12,A15,SPRECT_1:48
.= (W-min X)`1 by PSCOMP_1:84
.= pp`1 by A18,PSCOMP_1:88;
then A23: p in L~Upper_Seq(C,n) by A20,A22,TOPREAL3:11;
for x be set holds
x in LSeg(p,f) /\ L~Upper_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,f) /\ L~Upper_Seq(C,n) implies x = p
proof
assume A24: x in LSeg(p,f) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A25: pp in LSeg(p,f) by A24,XBOOLE_0:def 3;
then A26: pp`2 = p`2 by A17,GOBOARD7:6;
A27: pp`1 <= p`1 by A16,A25,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A28: f in LSeg(f,e) by TOPREAL1:6;
A29: f`2 = p`2 by A1,A2,A4,A8,A14,A15,GOBOARD5:2;
A30: e`2 = p`2 by A1,A2,A10,A14,A15,GOBOARD5:2;
A31: f`1 <= p`1 by A1,A2,A4,A11,A13,A15,SPRECT_3:25;
p`1 <= e`1 by A1,A2,A11,A13,A15,SPRECT_3:25;
then p in LSeg(f,e) by A29,A30,A31,GOBOARD7:9;
then A32: LSeg(p,f) c= LSeg(f,e) by A28,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A33: E0 is bounded_below by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A24,XBOOLE_0:def 3;
then pp in EE by A25,A32,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then p`1 <= pp`1 by A12,A15,A33,SEQ_4:def 5;
then pp`1 = p`1 by A27,AXIOMS:21;
hence x = p by A26,TOPREAL3:11;
end;
assume A34: x = p;
then x in LSeg(p,f) by TOPREAL1:6;
hence x in LSeg(p,f) /\ L~Upper_Seq(C,n) by A23,A34,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)} by A15,TARSKI:def 1;
end;
theorem Th16:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)} &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) and
A4: Gauge(C,n)*(k,i) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w1 = inf(proj1.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set p = |[w1,s]|;
set w2 = sup(proj1.:(LSeg(f,p) /\ L~Lower_Seq(C,n)));
set q = |[w2,s]|;
A5: len G = width G by JORDAN8:def 1;
A6: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A7: G*(k,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A8: LSeg(G*(j,i),G*(k,i)) meets L~Upper_Seq(C,n) by A4,XBOOLE_0:3;
A9: j <= width G by A1,A5,AXIOMS:22;
then A10: [j,i] in Indices G by A1,A2,A5,GOBOARD7:10;
A11: k >= 1 by A1,AXIOMS:22;
then [k,i] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A12: j <= k1 & k1 <= k and
A13: G*(k1,i)`1 = w1 by A1,A6,A8,A10,JORDAN1F:3;
A14: 1 <= k1 & k1 <= width G by A1,A5,A12,AXIOMS:22;
then A15: G*(k1,i)`2 = s by A2,A5,GOBOARD5:2;
then A16: p = G*(k1,i) by A13,EUCLID:57;
A17: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A18: G*(j,i) in LSeg(G*(j,i),G*(k1,i)) by TOPREAL1:6;
then A19: LSeg(G*(j,i),G*(k1,i)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
[k1,i] in Indices G by A2,A5,A14,GOBOARD7:10;
then consider j1 be Nat such that
A20: j <= j1 & j1 <= k1 and
A21: G*(j1,i)`1 = w2 by A10,A12,A16,A17,A19,JORDAN1F:4;
A22: 1 <= j1 & j1 <= width G by A1,A14,A20,AXIOMS:22;
then A23: G*(j1,i)`2 = s by A2,A5,GOBOARD5:2;
then A24: q = G*(j1,i) by A21,EUCLID:57;
take j1,k1;
thus j <= j1 & j1 <= k1 & k1 <= k by A12,A20;
A25: q`1 <= p`1 by A2,A5,A14,A16,A20,A22,A24,SPRECT_3:25;
set X = LSeg(G*(j,i),G*(k1,i)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A18,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A26: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A26;
pp in LSeg(SE-corner X, NE-corner X)/\X by A26,PSCOMP_1:def 40;
then A27: pp in X by XBOOLE_0:def 3;
then A28: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A29: pp in LSeg(G*(j,i),G*(k1,i)) by A27,XBOOLE_0:def 3;
A30: f`2 = p`2 by A1,A2,A5,A9,A15,A16,GOBOARD5:2;
then LSeg(f,p) is horizontal by SPPOL_1:36;
then A31: pp`2 = q`2 by A15,A16,A23,A24,A29,SPRECT_3:19;
q`1 = E-bound X by A16,A21,A24,SPRECT_1:51
.= (E-min X)`1 by PSCOMP_1:104
.= pp`1 by A26,PSCOMP_1:108;
then A32: q in L~Lower_Seq(C,n) by A28,A31,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Lower_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(p,q) /\ L~Lower_Seq(C,n) implies x = q
proof
assume A33: x in LSeg(p,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A34: pp in LSeg(p,q) by A33,XBOOLE_0:def 3;
then A35: pp`2 = q`2 by A15,A16,A23,A24,GOBOARD7:6;
A36: pp`1 >= q`1 by A25,A34,TOPREAL1:9;
reconsider EE = LSeg(f,p) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A37: f`2 = q`2 by A1,A2,A5,A9,A23,A24,GOBOARD5:2;
f`1 <= q`1 by A1,A2,A5,A20,A22,A24,SPRECT_3:25;
then A38: q in LSeg(p,f) by A15,A16,A23,A24,A25,A37,GOBOARD7:9;
p in LSeg(f,p) by TOPREAL1:6;
then A39: LSeg(p,q) c= LSeg(f,p) by A38,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A40: E0 is bounded_above by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A33,XBOOLE_0:def 3;
then pp in EE by A34,A39,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then q`1 >= pp`1 by A21,A24,A40,SEQ_4:def 4;
then pp`1 = q`1 by A36,AXIOMS:21;
hence x = q by A35,TOPREAL3:11;
end;
assume A41: x = q;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Lower_Seq(C,n) by A32,A41,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)} by A16,A24,TARSKI:def 1;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A4,A7,PSCOMP_1:64,XBOOLE_0:def
3;
consider pp be set such that
A42: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A42;
pp in LSeg(SW-corner X, NW-corner X)/\X by A42,PSCOMP_1:def 38;
then A43: pp in X by XBOOLE_0:def 3;
then A44: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A45: pp in LSeg(G*(j,i),G*(k,i)) by A43,XBOOLE_0:def 3;
f`2 = s by A1,A2,A5,A9,GOBOARD5:2
.= e`2 by A1,A2,A11,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A46: pp`2 = p`2 by A30,A45,SPRECT_3:19;
p`1 = W-bound X by A13,A16,SPRECT_1:48
.= (W-min X)`1 by PSCOMP_1:84
.= pp`1 by A42,PSCOMP_1:88;
then A47: p in L~Upper_Seq(C,n) by A44,A46,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Upper_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,q) /\ L~Upper_Seq(C,n) implies x = p
proof
assume A48: x in LSeg(p,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A49: pp in LSeg(p,q) by A48,XBOOLE_0:def 3;
then A50: pp`2 = p`2 by A15,A16,A23,A24,GOBOARD7:6;
A51: pp`1 <= p`1 by A25,A49,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A52: f`2 = q`2 by A1,A2,A5,A9,A23,A24,GOBOARD5:2;
A53: e`2 = q`2 by A1,A2,A11,A23,A24,GOBOARD5:2;
A54: f`1 <= q`1 by A1,A2,A5,A20,A22,A24,SPRECT_3:25;
j1 <= k by A12,A20,AXIOMS:22;
then q`1 <= e`1 by A1,A2,A22,A24,SPRECT_3:25;
then A55: q in LSeg(f,e) by A52,A53,A54,GOBOARD7:9;
A56: f`2 = p`2 by A1,A2,A5,A9,A15,A16,GOBOARD5:2;
A57: e`2 = p`2 by A1,A2,A11,A15,A16,GOBOARD5:2;
A58: f`1 <= p`1 by A1,A2,A5,A12,A14,A16,SPRECT_3:25;
p`1 <= e`1 by A1,A2,A12,A14,A16,SPRECT_3:25;
then p in LSeg(f,e) by A56,A57,A58,GOBOARD7:9;
then A59: LSeg(p,q) c= LSeg(f,e) by A55,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A60: E0 is bounded_below by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A48,XBOOLE_0:def 3;
then pp in EE by A49,A59,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then p`1 <= pp`1 by A13,A16,A60,SEQ_4:def 5;
then pp`1 = p`1 by A51,AXIOMS:21;
hence x = p by A50,TOPREAL3:11;
end;
assume A61: x = p;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Upper_Seq(C,n) by A47,A61,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)} by A16,A24,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,j) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w2 = sup(proj2.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set q = |[s,w2]|;
A4: j <= width G by A2,AXIOMS:22;
then A5: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A6: k >= 1 by A2,AXIOMS:22;
then A7: G*(i,k)`1 = s by A1,A2,GOBOARD5:3;
A8: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A9: G*(i,j) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A10: LSeg(G*(i,j),G*(i,k)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
[i,k] in Indices G by A1,A2,A6,GOBOARD7:10;
then consider j1 be Nat such that
A11: j <= j1 & j1 <= k and
A12: G*(i,j1)`2 = w2 by A2,A5,A8,A10,JORDAN1F:2;
A13: 1 <= j1 & j1 <= width G by A2,A11,AXIOMS:22;
then A14: G*(i,j1)`1 = s by A1,GOBOARD5:3;
then A15: q = G*(i,j1) by A12,EUCLID:57;
take j1;
thus j <= j1 & j1 <= k by A11;
A16: q`2 <= e`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A9,PSCOMP_1:64,XBOOLE_0:def
3;
consider pp be set such that
A17: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A17;
pp in LSeg(NW-corner X, NE-corner X)/\X by A17,PSCOMP_1:def 39;
then A18: pp in X by XBOOLE_0:def 3;
then A19: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A20: pp in LSeg(G*(i,j),G*(i,k)) by A18,XBOOLE_0:def 3;
f`1 = e`1 by A1,A2,A4,A7,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A21: pp`1 = q`1 by A7,A14,A15,A20,SPRECT_3:20;
q`2 = N-bound X by A12,A15,SPRECT_1:50
.= (N-min X)`2 by PSCOMP_1:94
.= pp`2 by A17,PSCOMP_1:98;
then A22: q in L~Upper_Seq(C,n) by A19,A21,TOPREAL3:11;
for x be set holds
x in LSeg(e,q) /\ L~Upper_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(e,q) /\ L~Upper_Seq(C,n) implies x = q
proof
assume A23: x in LSeg(e,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A24: pp in LSeg(e,q) by A23,XBOOLE_0:def 3;
then A25: pp`1 = q`1 by A7,A14,A15,GOBOARD7:5;
A26: pp`2 >= q`2 by A16,A24,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A27: f`1 = q`1 by A1,A2,A4,A14,A15,GOBOARD5:3;
f`2 <= q`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
then A28: q in LSeg(e,f) by A7,A14,A15,A16,A27,GOBOARD7:8;
e in LSeg(f,e) by TOPREAL1:6;
then A29: LSeg(e,q) c= LSeg(f,e) by A28,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A30: E0 is bounded_above by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A23,XBOOLE_0:def 3;
then pp in EE by A24,A29,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then q`2 >= pp`2 by A12,A15,A30,SEQ_4:def 4;
then pp`2 = q`2 by A26,AXIOMS:21;
hence x = q by A25,TOPREAL3:11;
end;
assume A31: x = q;
then x in LSeg(e,q) by TOPREAL1:6;
hence x in LSeg(e,q) /\ L~Upper_Seq(C,n) by A22,A31,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} by A15,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w1 = inf(proj2.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set p = |[s,w1]|;
A4: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A5: G*(i,k) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A6: LSeg(G*(i,j),G*(i,k)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
A7: j <= width G by A2,AXIOMS:22;
then A8: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A9: k >= 1 by A2,AXIOMS:22;
then [i,k] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A10: j <= k1 & k1 <= k and
A11: G*(i,k1)`2 = w1 by A2,A4,A6,A8,JORDAN1F:1;
A12: 1 <= k1 & k1 <= width G by A2,A10,AXIOMS:22;
then A13: G*(i,k1)`1 = s by A1,GOBOARD5:3;
then A14: p = G*(i,k1) by A11,EUCLID:57;
take k1;
thus j <= k1 & k1 <= k by A10;
A15: f`2 <= p`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
A16: f`1 = p`1 by A1,A2,A7,A13,A14,GOBOARD5:3;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A5,PSCOMP_1:64,XBOOLE_0:def 3
;
consider pp be set such that
A17: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A17;
pp in LSeg(SW-corner X, SE-corner X)/\X by A17,PSCOMP_1:def 41;
then A18: pp in X by XBOOLE_0:def 3;
then A19: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A20: pp in LSeg(G*(i,j),G*(i,k)) by A18,XBOOLE_0:def 3;
f`1 = s by A1,A2,A7,GOBOARD5:3
.= e`1 by A1,A2,A9,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A21: pp`1 = p`1 by A16,A20,SPRECT_3:20;
p`2 = S-bound X by A11,A14,SPRECT_1:49
.= (S-min X)`2 by PSCOMP_1:114
.= pp`2 by A17,PSCOMP_1:118;
then A22: p in L~Lower_Seq(C,n) by A19,A21,TOPREAL3:11;
for x be set holds
x in LSeg(p,f) /\ L~Lower_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,f) /\ L~Lower_Seq(C,n) implies x = p
proof
assume A23: x in LSeg(p,f) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A24: pp in LSeg(p,f) by A23,XBOOLE_0:def 3;
then A25: pp`1 = p`1 by A16,GOBOARD7:5;
A26: pp`2 <= p`2 by A15,A24,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A27: f in LSeg(f,e) by TOPREAL1:6;
A28: f`1 = p`1 by A1,A2,A7,A13,A14,GOBOARD5:3;
A29: e`1 = p`1 by A1,A2,A9,A13,A14,GOBOARD5:3;
A30: f`2 <= p`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
p`2 <= e`2 by A1,A2,A10,A12,A14,SPRECT_3:24;
then p in LSeg(f,e) by A28,A29,A30,GOBOARD7:8;
then A31: LSeg(p,f) c= LSeg(f,e) by A27,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A32: E0 is bounded_below by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A23,XBOOLE_0:def 3;
then pp in EE by A24,A31,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then p`2 <= pp`2 by A11,A14,A32,SEQ_4:def 5;
then pp`2 = p`2 by A26,AXIOMS:21;
hence x = p by A25,TOPREAL3:11;
end;
assume A33: x = p;
then x in LSeg(p,f) by TOPREAL1:6;
hence x in LSeg(p,f) /\ L~Lower_Seq(C,n) by A22,A33,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A14,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= i & i <= len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(i,k) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(i,1)`1;
set f = G*(i,j);
set e = G*(i,k);
set w1 = inf(proj2.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set p = |[s,w1]|;
set w2 = sup(proj2.:(LSeg(f,p) /\ L~Upper_Seq(C,n)));
set q = |[s,w2]|;
A5: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A6: G*(i,k) in LSeg(G*(i,j),G*(i,k)) by TOPREAL1:6;
then A7: LSeg(G*(i,j),G*(i,k)) meets L~Lower_Seq(C,n) by A4,XBOOLE_0:3;
A8: j <= width G by A2,AXIOMS:22;
then A9: [i,j] in Indices G by A1,A2,GOBOARD7:10;
A10: k >= 1 by A2,AXIOMS:22;
then [i,k] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A11: j <= k1 & k1 <= k and
A12: G*(i,k1)`2 = w1 by A2,A5,A7,A9,JORDAN1F:1;
A13: 1 <= k1 & k1 <= width G by A2,A11,AXIOMS:22;
then A14: G*(i,k1)`1 = s by A1,GOBOARD5:3;
then A15: p = G*(i,k1) by A12,EUCLID:57;
A16: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A17: G*(i,j) in LSeg(G*(i,j),G*(i,k1)) by TOPREAL1:6;
then A18: LSeg(G*(i,j),G*(i,k1)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
[i,k1] in Indices G by A1,A13,GOBOARD7:10;
then consider j1 be Nat such that
A19: j <= j1 & j1 <= k1 and
A20: G*(i,j1)`2 = w2 by A9,A11,A15,A16,A18,JORDAN1F:2;
A21: 1 <= j1 & j1 <= width G by A2,A13,A19,AXIOMS:22;
then A22: G*(i,j1)`1 = s by A1,GOBOARD5:3;
then A23: q = G*(i,j1) by A20,EUCLID:57;
take j1,k1;
thus j <= j1 & j1 <= k1 & k1 <= k by A11,A19;
A24: q`2 <= p`2 by A1,A13,A15,A19,A21,A23,SPRECT_3:24;
set X = LSeg(G*(i,j),G*(i,k1)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A17,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A25: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A25;
pp in LSeg(NW-corner X, NE-corner X)/\X by A25,PSCOMP_1:def 39;
then A26: pp in X by XBOOLE_0:def 3;
then A27: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A28: pp in LSeg(G*(i,j),G*(i,k1)) by A26,XBOOLE_0:def 3;
A29: f`1 = p`1 by A1,A2,A8,A14,A15,GOBOARD5:3;
then LSeg(f,p) is vertical by SPPOL_1:37;
then A30: pp`1 = q`1 by A14,A15,A22,A23,A28,SPRECT_3:20;
q`2 = N-bound X by A15,A20,A23,SPRECT_1:50
.= (N-min X)`2 by PSCOMP_1:94
.= pp`2 by A25,PSCOMP_1:98;
then A31: q in L~Upper_Seq(C,n) by A27,A30,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Upper_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(p,q) /\ L~Upper_Seq(C,n) implies x = q
proof
assume A32: x in LSeg(p,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A33: pp in LSeg(p,q) by A32,XBOOLE_0:def 3;
then A34: pp`1 = q`1 by A14,A15,A22,A23,GOBOARD7:5;
A35: pp`2 >= q`2 by A24,A33,TOPREAL1:10;
reconsider EE = LSeg(f,p) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A36: f`1 = q`1 by A1,A2,A8,A22,A23,GOBOARD5:3;
f`2 <= q`2 by A1,A2,A19,A21,A23,SPRECT_3:24;
then A37: q in LSeg(p,f) by A14,A15,A22,A23,A24,A36,GOBOARD7:8;
p in LSeg(f,p) by TOPREAL1:6;
then A38: LSeg(p,q) c= LSeg(f,p) by A37,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A39: E0 is bounded_above by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A32,XBOOLE_0:def 3;
then pp in EE by A33,A38,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then q`2 >= pp`2 by A20,A23,A39,SEQ_4:def 4;
then pp`2 = q`2 by A35,AXIOMS:21;
hence x = q by A34,TOPREAL3:11;
end;
assume A40: x = q;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Upper_Seq(C,n) by A31,A40,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),
Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} by A15,A23,TARSKI:def 1;
set X = LSeg(G*(i,j),G*(i,k)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A4,A6,PSCOMP_1:64,XBOOLE_0:def 3
;
consider pp be set such that
A41: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A41;
pp in LSeg(SW-corner X, SE-corner X)/\X by A41,PSCOMP_1:def 41;
then A42: pp in X by XBOOLE_0:def 3;
then A43: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A44: pp in LSeg(G*(i,j),G*(i,k)) by A42,XBOOLE_0:def 3;
f`1 = s by A1,A2,A8,GOBOARD5:3
.= e`1 by A1,A2,A10,GOBOARD5:3;
then LSeg(f,e) is vertical by SPPOL_1:37;
then A45: pp`1 = p`1 by A29,A44,SPRECT_3:20;
p`2 = S-bound X by A12,A15,SPRECT_1:49
.= (S-min X)`2 by PSCOMP_1:114
.= pp`2 by A41,PSCOMP_1:118;
then A46: p in L~Lower_Seq(C,n) by A43,A45,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Lower_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,q) /\ L~Lower_Seq(C,n) implies x = p
proof
assume A47: x in LSeg(p,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A48: pp in LSeg(p,q) by A47,XBOOLE_0:def 3;
then A49: pp`1 = p`1 by A14,A15,A22,A23,GOBOARD7:5;
A50: pp`2 <= p`2 by A24,A48,TOPREAL1:10;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj2.:EE as compact Subset of REAL by JORDAN1A:28;
A51: f`1 = q`1 by A1,A2,A8,A22,A23,GOBOARD5:3;
A52: e`1 = q`1 by A1,A2,A10,A22,A23,GOBOARD5:3;
A53: f`2 <= q`2 by A1,A2,A19,A21,A23,SPRECT_3:24;
j1 <= k by A11,A19,AXIOMS:22;
then q`2 <= e`2 by A1,A2,A21,A23,SPRECT_3:24;
then A54: q in LSeg(f,e) by A51,A52,A53,GOBOARD7:8;
A55: f`1 = p`1 by A1,A2,A8,A14,A15,GOBOARD5:3;
A56: e`1 = p`1 by A1,A2,A10,A14,A15,GOBOARD5:3;
A57: f`2 <= p`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
p`2 <= e`2 by A1,A2,A11,A13,A15,SPRECT_3:24;
then p in LSeg(f,e) by A55,A56,A57,GOBOARD7:8;
then A58: LSeg(p,q) c= LSeg(f,e) by A54,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A59: E0 is bounded_below by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A47,XBOOLE_0:def 3;
then pp in EE by A48,A58,XBOOLE_0:def 3;
then proj2.pp in E0 by FUNCT_2:43;
then pp`2 in E0 by PSCOMP_1:def 29;
then p`2 <= pp`2 by A12,A15,A59,SEQ_4:def 5;
then pp`2 = p`2 by A50,AXIOMS:21;
hence x = p by A49,TOPREAL3:11;
end;
assume A60: x = p;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Lower_Seq(C,n) by A46,A60,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(i,j1),
Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A15,A23,TARSKI:def 1;
end;
theorem Th20:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(j,i) in L~Upper_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w2 = sup(proj1.:(LSeg(f,e) /\ L~Upper_Seq(C,n)));
set q = |[w2,s]|;
A4: len G = width G by JORDAN8:def 1;
then A5: j <= width G by A1,AXIOMS:22;
then A6: [j,i] in Indices G by A1,A2,A4,GOBOARD7:10;
A7: k >= 1 by A1,AXIOMS:22;
then A8: G*(k,i)`2 = s by A1,A2,GOBOARD5:2;
A9: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A10: G*(j,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A11: LSeg(G*(j,i),G*(k,i)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
[k,i] in Indices G by A1,A2,A7,GOBOARD7:10;
then consider j1 be Nat such that
A12: j <= j1 & j1 <= k and
A13: G*(j1,i)`1 = w2 by A1,A6,A9,A11,JORDAN1F:4;
A14: 1 <= j1 & j1 <= width G by A1,A4,A12,AXIOMS:22;
then A15: G*(j1,i)`2 = s by A2,A4,GOBOARD5:2;
then A16: q = G*(j1,i) by A13,EUCLID:57;
take j1;
thus j <= j1 & j1 <= k by A12;
A17: q`1 <= e`1 by A1,A2,A12,A14,A16,SPRECT_3:25;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A10,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A18: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A18;
pp in LSeg(SE-corner X, NE-corner X)/\X by A18,PSCOMP_1:def 40;
then A19: pp in X by XBOOLE_0:def 3;
then A20: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A21: pp in LSeg(G*(j,i),G*(k,i)) by A19,XBOOLE_0:def 3;
f`2 = e`2 by A1,A2,A4,A5,A8,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A22: pp`2 = q`2 by A8,A15,A16,A21,SPRECT_3:19;
q`1 = E-bound X by A13,A16,SPRECT_1:51
.= (E-min X)`1 by PSCOMP_1:104
.= pp`1 by A18,PSCOMP_1:108;
then A23: q in L~Upper_Seq(C,n) by A20,A22,TOPREAL3:11;
for x be set holds
x in LSeg(e,q) /\ L~Upper_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(e,q) /\ L~Upper_Seq(C,n) implies x = q
proof
assume A24: x in LSeg(e,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A25: pp in LSeg(e,q) by A24,XBOOLE_0:def 3;
then A26: pp`2 = q`2 by A8,A15,A16,GOBOARD7:6;
A27: pp`1 >= q`1 by A17,A25,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A28: f`2 = q`2 by A1,A2,A4,A5,A15,A16,GOBOARD5:2;
f`1 <= q`1 by A1,A2,A4,A12,A14,A16,SPRECT_3:25;
then A29: q in LSeg(e,f) by A8,A15,A16,A17,A28,GOBOARD7:9;
e in LSeg(f,e) by TOPREAL1:6;
then A30: LSeg(e,q) c= LSeg(f,e) by A29,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A31: E0 is bounded_above by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A24,XBOOLE_0:def 3;
then pp in EE by A25,A30,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then q`1 >= pp`1 by A13,A16,A31,SEQ_4:def 4;
then pp`1 = q`1 by A27,AXIOMS:21;
hence x = q by A26,TOPREAL3:11;
end;
assume A32: x = q;
then x in LSeg(e,q) by TOPREAL1:6;
hence x in LSeg(e,q) /\ L~Upper_Seq(C,n) by A23,A32,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)} by A16,TARSKI:def 1;
end;
theorem
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(k,i) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w1 = inf(proj1.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set p = |[w1,s]|;
A4: len G = width G by JORDAN8:def 1;
A5: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A6: G*(k,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A7: LSeg(G*(j,i),G*(k,i)) meets L~Lower_Seq(C,n) by A3,XBOOLE_0:3;
A8: j <= width G by A1,A4,AXIOMS:22;
then A9: [j,i] in Indices G by A1,A2,A4,GOBOARD7:10;
A10: k >= 1 by A1,AXIOMS:22;
then [k,i] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A11: j <= k1 & k1 <= k and
A12: G*(k1,i)`1 = w1 by A1,A5,A7,A9,JORDAN1F:3;
A13: 1 <= k1 & k1 <= width G by A1,A4,A11,AXIOMS:22;
then A14: G*(k1,i)`2 = s by A2,A4,GOBOARD5:2;
then A15: p = G*(k1,i) by A12,EUCLID:57;
take k1;
thus j <= k1 & k1 <= k by A11;
A16: f`1 <= p`1 by A1,A2,A4,A11,A13,A15,SPRECT_3:25;
A17: f`2 = p`2 by A1,A2,A4,A8,A14,A15,GOBOARD5:2;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A6,PSCOMP_1:64,XBOOLE_0:def
3;
consider pp be set such that
A18: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A18;
pp in LSeg(SW-corner X, NW-corner X)/\X by A18,PSCOMP_1:def 38;
then A19: pp in X by XBOOLE_0:def 3;
then A20: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A21: pp in LSeg(G*(j,i),G*(k,i)) by A19,XBOOLE_0:def 3;
f`2 = s by A1,A2,A4,A8,GOBOARD5:2
.= e`2 by A1,A2,A10,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A22: pp`2 = p`2 by A17,A21,SPRECT_3:19;
p`1 = W-bound X by A12,A15,SPRECT_1:48
.= (W-min X)`1 by PSCOMP_1:84
.= pp`1 by A18,PSCOMP_1:88;
then A23: p in L~Lower_Seq(C,n) by A20,A22,TOPREAL3:11;
for x be set holds
x in LSeg(p,f) /\ L~Lower_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,f) /\ L~Lower_Seq(C,n) implies x = p
proof
assume A24: x in LSeg(p,f) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A25: pp in LSeg(p,f) by A24,XBOOLE_0:def 3;
then A26: pp`2 = p`2 by A17,GOBOARD7:6;
A27: pp`1 <= p`1 by A16,A25,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A28: f in LSeg(f,e) by TOPREAL1:6;
A29: f`2 = p`2 by A1,A2,A4,A8,A14,A15,GOBOARD5:2;
A30: e`2 = p`2 by A1,A2,A10,A14,A15,GOBOARD5:2;
A31: f`1 <= p`1 by A1,A2,A4,A11,A13,A15,SPRECT_3:25;
p`1 <= e`1 by A1,A2,A11,A13,A15,SPRECT_3:25;
then p in LSeg(f,e) by A29,A30,A31,GOBOARD7:9;
then A32: LSeg(p,f) c= LSeg(f,e) by A28,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A33: E0 is bounded_below by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A24,XBOOLE_0:def 3;
then pp in EE by A25,A32,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then p`1 <= pp`1 by A12,A15,A33,SEQ_4:def 5;
then pp`1 = p`1 by A27,AXIOMS:21;
hence x = p by A26,TOPREAL3:11;
end;
assume A34: x = p;
then x in LSeg(p,f) by TOPREAL1:6;
hence x in LSeg(p,f) /\ L~Lower_Seq(C,n) by A23,A34,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)} by A15,TARSKI:def 1;
end;
theorem Th22:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)} &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)}
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(k,i) in L~Lower_Seq(C,n);
set G = Gauge(C,n);
set s = G*(1,i)`2;
set f = G*(j,i);
set e = G*(k,i);
set w1 = inf(proj1.:(LSeg(f,e) /\ L~Lower_Seq(C,n)));
set p = |[w1,s]|;
set w2 = sup(proj1.:(LSeg(f,p) /\ L~Upper_Seq(C,n)));
set q = |[w2,s]|;
A5: len G = width G by JORDAN8:def 1;
A6: Lower_Seq(C,n) is_sequence_on G by JORDAN1G:5;
A7: G*(k,i) in LSeg(G*(j,i),G*(k,i)) by TOPREAL1:6;
then A8: LSeg(G*(j,i),G*(k,i)) meets L~Lower_Seq(C,n) by A4,XBOOLE_0:3;
A9: j <= width G by A1,A5,AXIOMS:22;
then A10: [j,i] in Indices G by A1,A2,A5,GOBOARD7:10;
A11: k >= 1 by A1,AXIOMS:22;
then [k,i] in Indices G by A1,A2,GOBOARD7:10;
then consider k1 be Nat such that
A12: j <= k1 & k1 <= k and
A13: G*(k1,i)`1 = w1 by A1,A6,A8,A10,JORDAN1F:3;
A14: 1 <= k1 & k1 <= width G by A1,A5,A12,AXIOMS:22;
then A15: G*(k1,i)`2 = s by A2,A5,GOBOARD5:2;
then A16: p = G*(k1,i) by A13,EUCLID:57;
A17: Upper_Seq(C,n) is_sequence_on G by JORDAN1G:4;
A18: G*(j,i) in LSeg(G*(j,i),G*(k1,i)) by TOPREAL1:6;
then A19: LSeg(G*(j,i),G*(k1,i)) meets L~Upper_Seq(C,n) by A3,XBOOLE_0:3;
[k1,i] in Indices G by A2,A5,A14,GOBOARD7:10;
then consider j1 be Nat such that
A20: j <= j1 & j1 <= k1 and
A21: G*(j1,i)`1 = w2 by A10,A12,A16,A17,A19,JORDAN1F:4;
A22: 1 <= j1 & j1 <= width G by A1,A14,A20,AXIOMS:22;
then A23: G*(j1,i)`2 = s by A2,A5,GOBOARD5:2;
then A24: q = G*(j1,i) by A21,EUCLID:57;
take j1,k1;
thus j <= j1 & j1 <= k1 & k1 <= k by A12,A20;
A25: q`1 <= p`1 by A2,A5,A14,A16,A20,A22,A24,SPRECT_3:25;
set X = LSeg(G*(j,i),G*(k1,i)) /\ L~Upper_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A3,A18,PSCOMP_1:64,XBOOLE_0:
def 3;
consider pp be set such that
A26: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A26;
pp in LSeg(SE-corner X, NE-corner X)/\X by A26,PSCOMP_1:def 40;
then A27: pp in X by XBOOLE_0:def 3;
then A28: pp in L~Upper_Seq(C,n) by XBOOLE_0:def 3;
A29: pp in LSeg(G*(j,i),G*(k1,i)) by A27,XBOOLE_0:def 3;
A30: f`2 = p`2 by A1,A2,A5,A9,A15,A16,GOBOARD5:2;
then LSeg(f,p) is horizontal by SPPOL_1:36;
then A31: pp`2 = q`2 by A15,A16,A23,A24,A29,SPRECT_3:19;
q`1 = E-bound X by A16,A21,A24,SPRECT_1:51
.= (E-min X)`1 by PSCOMP_1:104
.= pp`1 by A26,PSCOMP_1:108;
then A32: q in L~Upper_Seq(C,n) by A28,A31,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Upper_Seq(C,n) iff x = q
proof
let x be set;
thus x in LSeg(p,q) /\ L~Upper_Seq(C,n) implies x = q
proof
assume A33: x in LSeg(p,q) /\ L~Upper_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A34: pp in LSeg(p,q) by A33,XBOOLE_0:def 3;
then A35: pp`2 = q`2 by A15,A16,A23,A24,GOBOARD7:6;
A36: pp`1 >= q`1 by A25,A34,TOPREAL1:9;
reconsider EE = LSeg(f,p) /\ L~Upper_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A37: f`2 = q`2 by A1,A2,A5,A9,A23,A24,GOBOARD5:2;
f`1 <= q`1 by A1,A2,A5,A20,A22,A24,SPRECT_3:25;
then A38: q in LSeg(p,f) by A15,A16,A23,A24,A25,A37,GOBOARD7:9;
p in LSeg(f,p) by TOPREAL1:6;
then A39: LSeg(p,q) c= LSeg(f,p) by A38,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A40: E0 is bounded_above by SEQ_4:def 3;
pp in L~Upper_Seq(C,n) by A33,XBOOLE_0:def 3;
then pp in EE by A34,A39,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then q`1 >= pp`1 by A21,A24,A40,SEQ_4:def 4;
then pp`1 = q`1 by A36,AXIOMS:21;
hence x = q by A35,TOPREAL3:11;
end;
assume A41: x = q;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Upper_Seq(C,n) by A32,A41,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)} by A16,A24,TARSKI:def 1;
set X = LSeg(G*(j,i),G*(k,i)) /\ L~Lower_Seq(C,n);
reconsider X1=X as non empty compact Subset of TOP-REAL 2
by A4,A7,PSCOMP_1:64,XBOOLE_0:def
3;
consider pp be set such that
A42: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp as Point of TOP-REAL 2 by A42;
pp in LSeg(SW-corner X, NW-corner X)/\X by A42,PSCOMP_1:def 38;
then A43: pp in X by XBOOLE_0:def 3;
then A44: pp in L~Lower_Seq(C,n) by XBOOLE_0:def 3;
A45: pp in LSeg(G*(j,i),G*(k,i)) by A43,XBOOLE_0:def 3;
f`2 = s by A1,A2,A5,A9,GOBOARD5:2
.= e`2 by A1,A2,A11,GOBOARD5:2;
then LSeg(f,e) is horizontal by SPPOL_1:36;
then A46: pp`2 = p`2 by A30,A45,SPRECT_3:19;
p`1 = W-bound X by A13,A16,SPRECT_1:48
.= (W-min X)`1 by PSCOMP_1:84
.= pp`1 by A42,PSCOMP_1:88;
then A47: p in L~Lower_Seq(C,n) by A44,A46,TOPREAL3:11;
for x be set holds
x in LSeg(p,q) /\ L~Lower_Seq(C,n) iff x = p
proof
let x be set;
thus x in LSeg(p,q) /\ L~Lower_Seq(C,n) implies x = p
proof
assume A48: x in LSeg(p,q) /\ L~Lower_Seq(C,n);
then reconsider pp = x as Point of TOP-REAL 2;
A49: pp in LSeg(p,q) by A48,XBOOLE_0:def 3;
then A50: pp`2 = p`2 by A15,A16,A23,A24,GOBOARD7:6;
A51: pp`1 <= p`1 by A25,A49,TOPREAL1:9;
reconsider EE = LSeg(f,e) /\ L~Lower_Seq(C,n)
as compact Subset of TOP-REAL 2 by PSCOMP_1:64;
reconsider E0 = proj1.:EE as compact Subset of REAL by Th4;
A52: f`2 = q`2 by A1,A2,A5,A9,A23,A24,GOBOARD5:2;
A53: e`2 = q`2 by A1,A2,A11,A23,A24,GOBOARD5:2;
A54: f`1 <= q`1 by A1,A2,A5,A20,A22,A24,SPRECT_3:25;
j1 <= k by A12,A20,AXIOMS:22;
then q`1 <= e`1 by A1,A2,A22,A24,SPRECT_3:25;
then A55: q in LSeg(f,e) by A52,A53,A54,GOBOARD7:9;
A56: f`2 = p`2 by A1,A2,A5,A9,A15,A16,GOBOARD5:2;
A57: e`2 = p`2 by A1,A2,A11,A15,A16,GOBOARD5:2;
A58: f`1 <= p`1 by A1,A2,A5,A12,A14,A16,SPRECT_3:25;
p`1 <= e`1 by A1,A2,A12,A14,A16,SPRECT_3:25;
then p in LSeg(f,e) by A56,A57,A58,GOBOARD7:9;
then A59: LSeg(p,q) c= LSeg(f,e) by A55,TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A60: E0 is bounded_below by SEQ_4:def 3;
pp in L~Lower_Seq(C,n) by A48,XBOOLE_0:def 3;
then pp in EE by A49,A59,XBOOLE_0:def 3;
then proj1.pp in E0 by FUNCT_2:43;
then pp`1 in E0 by PSCOMP_1:def 28;
then p`1 <= pp`1 by A13,A16,A60,SEQ_4:def 5;
then pp`1 = p`1 by A51,AXIOMS:21;
hence x = p by A50,TOPREAL3:11;
end;
assume A61: x = p;
then x in LSeg(p,q) by TOPREAL1:6;
hence x in LSeg(p,q) /\ L~Lower_Seq(C,n) by A47,A61,XBOOLE_0:def 3;
end;
hence LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)} by A16,A24,TARSKI:def 1;
end;
theorem Th23:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n);
consider j1,k1 be Nat such that
A5: j <= j1 and
A6: j1 <= k1 and
A7: k1 <= k and
A8: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} and
A9: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A1,A2,A3,A4,Th13;
1 <= j1 & k1 <= width Gauge(C,n) by A2,A5,A7,AXIOMS:22;
then A10: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) meets Lower_Arc C
by A1,A6,A8,A9,JORDAN1J:58;
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) c=
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) by A1,A2,A5,A6,A7,Th7;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A10,XBOOLE_1:63;
end;
theorem Th24:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(i,j) in L~Lower_Seq(C,n);
consider j1,k1 be Nat such that
A5: j <= j1 and
A6: j1 <= k1 and
A7: k1 <= k and
A8: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} and
A9: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)} by A1,A2,A3,A4,Th13;
1 <= j1 & k1 <= width Gauge(C,n) by A2,A5,A7,AXIOMS:22;
then A10: LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) meets Upper_Arc C
by A1,A6,A8,A9,JORDAN1J:59;
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) c=
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) by A1,A2,A5,A6,A7,Th7;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A10,XBOOLE_1:63;
end;
theorem Th25:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) and
A5: Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n);
A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C
by A1,A2,A4,A5,A6,Th23;
end;
theorem Th26:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
assume that
A1: 1 < i & i < len Gauge(C,n) and
A2: 1 <= j & j <= k & k <= width Gauge(C,n) and
A3: n > 0 and
A4: Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) and
A5: Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n);
A6: L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n) by A3,JORDAN1G:63;
L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n) by A3,JORDAN1G:64;
hence LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C
by A1,A2,A4,A5,A6,Th24;
end;
theorem
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= width Gauge(C,n+1) and
A2: Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) and
A3: Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1);
n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: len Gauge(C,n+1) >= 4 by JORDAN8:13;
then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22;
len Gauge(C,n+1) >= 2 by A5,AXIOMS:22;
then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15;
Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16;
hence LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C
by A1,A2,A3,A4,A7,Th25;
end;
theorem
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let j,k be Nat;
assume that
A1: 1 <= j & j <= k & k <= width Gauge(C,n+1) and
A2: Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) and
A3: Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1);
n+1 >= 0+1 by NAT_1:29;
then A4: n+1 > 0 by NAT_1:38;
A5: len Gauge(C,n+1) >= 4 by JORDAN8:13;
then A6: len Gauge(C,n+1) >= 3 by AXIOMS:22;
len Gauge(C,n+1) >= 2 by A5,AXIOMS:22;
then A7: 1 < Center Gauge(C,n+1) by JORDAN1B:15;
Center Gauge(C,n+1) < len Gauge(C,n+1) by A6,JORDAN1B:16;
hence LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C
by A1,A2,A3,A4,A7,Th26;
end;
theorem Th29:
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 < j & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds j <> k
proof
let C be compact connected non vertical non horizontal
Subset of TOP-REAL 2;
let i,j,k be Nat;
assume that
A1: 1 < j & k < len Gauge(C,n) and
A2: 1 <= i & i <= width Gauge(C,n) and
A3: Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) and
A4: Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) and
A5: j = k;
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n)
by A3,A4,A5,XBOOLE_0:def 3;
then A7: Gauge(C,n)*(k,i) in {W-min L~Cage(C,n),E-max L~Cage(C,n)}
by JORDAN1E:20;
A8: [j,i] in Indices Gauge(C,n) by A1,A2,A5,GOBOARD7:10;
len Gauge(C,n) >= 4 by JORDAN8:13;
then A9: len Gauge(C,n) >= 1 by AXIOMS:22;
then A10: [len Gauge(C,n),i] in Indices Gauge(C,n) by A2,GOBOARD7:10;
A11: [1,i] in Indices Gauge(C,n) by A2,A9,GOBOARD7:10;
per cases by A7,TARSKI:def 2;
suppose A12: Gauge(C,n)*(k,i) = W-min L~Cage(C,n);
Gauge(C,n)*(1,i)`1 = W-bound L~Cage(C,n) by A2,A6,JORDAN1A:94;
then (W-min L~Cage(C,n))`1 <> W-bound L~Cage(C,n)
by A1,A5,A8,A11,A12,JORDAN1G:7;
hence contradiction by PSCOMP_1:84;
suppose A13: Gauge(C,n)*(k,i) = E-max L~Cage(C,n);
Gauge(C,n)*(len Gauge(C,n),i)`1 = E-bound L~Cage(C,n)
by A2,A6,JORDAN1A:92;
then (E-max L~Cage(C,n))`1 <> E-bound L~Cage(C,n)
by A1,A5,A8,A10,A13,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
theorem Th30:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
set Ga = Gauge(C,n);
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
set LA = Lower_Arc C;
set Wmin = W-min L~Cage(C,n);
set Emax = E-max L~Cage(C,n);
set Wbo = W-bound L~Cage(C,n);
set Ebo = E-bound L~Cage(C,n);
set Gij = Ga*(j,i);
set Gik = Ga*(k,i);
assume that
A1: 1 < j & j <= k & k < len Ga and
A2: 1 <= i & i <= width Ga and
A3: LSeg(Gij,Gik) /\ L~US = {Gik} and
A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A5: LSeg(Gij,Gik) misses LA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
A8: len Ga = width Ga by JORDAN8:def 1;
A9: j <> k by A1,A2,A6,A7,Th29;
A10: 1 <= j & j <= width Ga by A1,A8,AXIOMS:22;
A11: 1 <= k & k <= width Ga by A1,AXIOMS:22,JORDAN8:def 1;
A12: [j,i] in Indices Ga by A2,A8,A10,GOBOARD7:10;
A13: [k,i] in Indices Ga by A2,A8,A11,GOBOARD7:10;
A14: US is_sequence_on Ga by JORDAN1G:4;
A15: LS is_sequence_on Ga by JORDAN1G:5;
set go = R_Cut(US,Gik);
set do = L_Cut(LS,Gij);
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A8,A11,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A11,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A13,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: [1,j] in Indices Ga by A10,A19,GOBOARD7:10;
A23: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A24: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A25: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A26: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A8,A11,JORDAN1A:94;
A27: [j,i] in Indices Ga by A2,A8,A10,GOBOARD7:10;
then A28: Gij <> LS.len LS by A1,A20,A25,A26,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A29: [len Ga,k] in Indices Ga by A11,A19,GOBOARD7:10;
A30: LS.1 = LS/.1 by A24,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A8,A11,JORDAN1A:92;
then A31: Gij <> LS.1 by A1,A27,A29,A30,JORDAN1G:7;
A32: len go >= 1+1 by TOPREAL1:def 10;
A33: Gik in rng US by A2,A7,A8,A11,A14,JORDAN1J:40;
then A34: go is_sequence_on Ga by A14,JORDAN1J:38;
A35: len do >= 1+1 by TOPREAL1:def 10;
A36: Gij in rng LS by A2,A6,A8,A10,A15,JORDAN1J:40;
then A37: do is_sequence_on Ga by A15,JORDAN1J:39;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A32,A34,JGRAPH_1:16,
JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A35,A37,JGRAPH_1:16,
JORDAN8:8;
A38: len go > 1 by A32,NAT_1:38;
then A39: len go in dom go by FINSEQ_3:27;
then A40: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A35,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A41: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A39,FINSEQ_3:28;
A42: m+1 = len go by XCMPLX_1:27;
then A43: len go-'1 = m by BINARITH:39;
A44: LSeg(go,m) c= L~go by TOPREAL3:26;
A45: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A44,XBOOLE_1:1;
then A46: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A32,REAL_1:84;
then A47: LSeg(go,m) = LSeg(go/.m,Gik) by A40,A42,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A48: x = Gik by TARSKI:def 1;
A49: Gik in LSeg(go,m) by A47,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A48,A49,XBOOLE_0:def 3;
end;
then A50: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A46,XBOOLE_0:def 10;
A51: LSeg(do,1) c= L~do by TOPREAL3:26;
A52: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A51,XBOOLE_1:1;
then A53: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A54: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A35,A41,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A55: x = Gij by TARSKI:def 1;
A56: Gij in LSeg(do,1) by A54,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A55,A56,XBOOLE_0:def 3;
end;
then A57: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A53,XBOOLE_0:def 10;
A58: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A59: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,JORDAN1J:35;
A60: rng go c= L~go & rng do c= L~do by A32,A35,SPPOL_2:18;
A61: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A59,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A60,XBOOLE_0:def 3;
end;
A62: LS.1 = LS/.1 by A24,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A63: [len Ga,j] in Indices Ga by A10,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A64: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A45,A52,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A65: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A66: Emax = Gij by A6,A62,A64,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A8,A10,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A12,A63,A66,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A58,A65,TARSKI:def 1;
end;
then A67: L~go /\ L~do = {go/.1} by A61,XBOOLE_0:def 10;
set W2 = go/.2;
A68: 2 in dom go by A32,FINSEQ_3:27;
A69: Gik..US >= 1 by A33,FINSEQ_4:31;
A70: now assume Gij`1 = Wbo;
then Ga*(1,j)`1 = Ga*(j,i)`1 by A8,A10,JORDAN1A:94;
hence contradiction by A1,A12,A22,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A33,JORDAN1G:57
.= US|(Gik..US) by A69,JORDAN3:25;
then A71: W2 = US/.2 by A68,TOPREAL1:1;
A72: Wmin in rng go by A58,FINSEQ_6:46;
set pion = <*Gik,Gij*>;
A73: now let n be Nat;
assume n in dom pion;
then n in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then n = 1 or n = 2 by TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex j,i be Nat st [j,i] in Indices Ga & pion/.n = Ga*(j,i)
by A12,A13;
end;
A74: Gik <> Gij by A9,A12,A13,GOBOARD1:21;
Gik`2 = Ga*(1,i)`2 by A2,A8,A11,GOBOARD5:2
.= Gij`2 by A2,A8,A10,GOBOARD5:2;
then LSeg(Gik,Gij) is horizontal by SPPOL_1:36;
then pion is_S-Seq by A74,JORDAN1B:9;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A75: pion1 is_sequence_on Ga and
A76: pion1 is_S-Seq and
A77: L~pion = L~pion1 and
A78: pion/.1 = pion1/.1 and
A79: pion/.len pion = pion1/.len pion1 and
A80: len pion <= len pion1 by A73,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A76;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A81: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A82: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A83: len (go^'pion1) >= 1+1 by A32,AXIOMS:22;
then A84: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A85: 1+1 <= len godo by A83,AXIOMS:22;
A86: US is_sequence_on Ga by JORDAN1G:4;
A87: go/.len go = pion1/.1 by A40,A78,FINSEQ_4:26;
then A88: go^'pion1 is_sequence_on Ga by A34,A75,TOPREAL8:12;
A89: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A79,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A41,FINSEQ_4:26;
then A90: godo is_sequence_on Ga by A37,A88,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A77,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A91: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik}
by A43,A50,XBOOLE_1:27;
A92: len pion1 >= 1+1 by A80,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A93: x = Gik by TARSKI:def 1;
A94: Gik in LSeg(go,m) by A47,TOPREAL1:6;
Gik in LSeg(pion1,1) by A40,A87,A92,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A93,A94,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A40,A43,A91,XBOOLE_0:def 10;
then A95: go^'pion1 is unfolded by A87,TOPREAL8:34;
len pion1 >= 2+0 by A80,FINSEQ_1:61;
then A96: len pion1-2 >= 0 by REAL_1:84;
A97: len (go^'pion1)-1 >= 0 by A84,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A96,BINARITH:def 3;
then A98: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A97,BINARITH:def 3;
A99: len pion1-1 >= 1 by A92,REAL_1:84;
then A100: len pion1-1 >= 0 by AXIOMS:22;
then A101: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A102: len pion1-'2+1 = len pion1-2+1 by A96,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A100,BINARITH:def 3;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A103: len pion1-'1 < len pion1 by A101,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A77,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A104: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij}
by A57,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A105: x = Gij by TARSKI:def 1;
A106: Gij in LSeg(do,1) by A54,TOPREAL1:6;
A107: len pion1-'1+1 = len pion1 by A101,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A79,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A99,A101,A107,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
by A105,A106,XBOOLE_0:def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A104,XBOOLE_0:def 10
;
then A108: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A41,A87,A89,A102,A103,TOPREAL8:31;
A109: (go^'pion1) is non trivial by A83,SPPOL_1:2;
A110: rng pion1 c= L~pion1 by A92,SPPOL_2:18;
A111: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A87,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A60,A110,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A45,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A40,A77,A87,SPPOL_2:21;
end;
then A112: L~go /\ L~pion1 = {pion1/.1} by A111,XBOOLE_0:def 10;
then A113: (go^'pion1) is s.n.c. by A87,JORDAN1J:54;
rng go /\ rng pion1 c= {pion1/.1} by A60,A110,A112,XBOOLE_1:27;
then A114: go^'pion1 is one-to-one by JORDAN1J:55;
A115: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A41,FINSEQ_4:26;
A116: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A79,A115,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A60,A110,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A52,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A41,A77,A79,A115,SPPOL_2:21;
end;
then A117: L~do /\ L~pion1 = {pion1/.len pion1} by A116,XBOOLE_0:def 10;
A118: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A87,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A67,A79,A115,A117,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
do/.len do = (go^'pion1)/.1 by A59,AMISTD_1:5;
then reconsider godo as non constant standard special_circular_sequence
by A85,A89,A90,A95,A98,A108,A109,A113,A114,A118,JORDAN8:7,8,TOPREAL8:11,
33,34;
A119: LA is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then A120: LA is connected by JORDAN6:11;
A121: W-min C in LA & E-max C in LA by A119,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A122: ff/.1 = Wmin by FINSEQ_6:98;
A123: L~ff = L~Cage(C,n) by REVROT_1:33;
then A124: (W-max L~ff)..ff > 1 by A122,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A122,A123,SPRECT_5:24;
then A125: (N-min L~ff)..ff > 1 by A124,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A122,A123,SPRECT_5:25;
then A126: (N-max L~ff)..ff > 1 by A125,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A122,A123,SPRECT_5:26;
then A127: Emax..ff > 1 by A123,A126,AXIOMS:22;
A128: now assume A129: Gik..US <= 1;
Gik..US >= 1 by A33,FINSEQ_4:31;
then Gik..US = 1 by A129,AXIOMS:21;
then Gik = US/.1 by A33,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A130: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A131: ff is_sequence_on Ga by REVROT_1:34;
A132: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A85,A90,JORDAN9:29;
A133: L~godo = L~(go^'pion1) \/ L~do by A89,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A87,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A134: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A135: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n)
by A45,A52,XBOOLE_1:1;
A136: W-min C in C by SPRECT_1:15;
A137: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A138: now assume W-min C in L~godo;
then A139: W-min C in L~go \/ L~pion1 or W-min C in L~do by A133,XBOOLE_0:
def 2;
per cases by A139,XBOOLE_0:def 2;
suppose W-min C in L~go;
then C meets L~Cage(C,n) by A135,A136,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
suppose W-min C in L~pion1;
hence contradiction by A5,A77,A121,A137,XBOOLE_0:3;
suppose W-min C in L~do;
then C meets L~Cage(C,n) by A135,A136,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
right_cell(Rotate(Cage(C,n),Wmin),1) =
right_cell(ff,1,GoB ff) by A82,JORDAN1H:29
.= right_cell(ff,1,GoB Cage(C,n)) by REVROT_1:28
.= right_cell(ff,1,Ga) by JORDAN1H:52
.= right_cell(ff-:Emax,1,Ga) by A127,A131,JORDAN1J:53
.= right_cell(US,1,Ga) by JORDAN1E:def 1
.= right_cell(R_Cut(US,Gik),1,Ga) by A33,A86,A128,JORDAN1J:52
.= right_cell(go^'pion1,1,Ga) by A38,A88,JORDAN1J:51
.= right_cell(godo,1,Ga) by A84,A90,JORDAN1J:51;
then W-min C in right_cell(godo,1,Ga) by JORDAN1I:8;
then A140: W-min C in right_cell(godo,1,Ga)\L~godo by A138,XBOOLE_0:def 4;
A141: godo/.1 = (go^'pion1)/.1 by AMISTD_1:5
.= Wmin by A58,AMISTD_1:5;
A142: len US >= 2 by A16,AXIOMS:22;
A143: godo/.2 = (go^'pion1)/.2 by A83,AMISTD_1:9
.= US/.2 by A32,A71,AMISTD_1:9
.= (US^'LS)/.2 by A142,AMISTD_1:9
.= Rotate(Cage(C,n),Wmin)/.2 by JORDAN1E:15;
A144: L~go \/ L~do is compact by COMPTS_1:19;
A145: L~go \/ L~do c= L~Cage(C,n) by A135,XBOOLE_1:8;
Wmin in L~go \/ L~do by A60,A72,XBOOLE_0:def 2;
then A146: W-min (L~go \/ L~do) = Wmin by A144,A145,JORDAN1J:21;
A147: (W-min (L~go \/ L~do))`1 = W-bound (L~go \/ L~do) & Wmin`1 = Wbo
by PSCOMP_1:84;
A148: Gij`1 <= Gik`1 by A1,A2,SPRECT_3:25;
then W-bound LSeg(Gik,Gij) = Gij`1 by SPRECT_1:62;
then A149: W-bound L~pion1 = Gij`1 by A77,SPPOL_2:21;
Gij`1 >= Wbo by A6,A134,PSCOMP_1:71;
then Gij`1 > Wbo by A70,REAL_1:def 5;
then W-min (L~go\/L~do\/L~pion1) = W-min (L~go \/ L~do)
by A144,A146,A147,A149,JORDAN1J:
33;
then A150: W-min L~godo = Wmin by A133,A146,XBOOLE_1:4;
A151: rng godo c= L~godo by A85,SPPOL_2:18;
2 in dom godo by A85,FINSEQ_3:27;
then A152: godo/.2 in rng godo by PARTFUN2:4;
godo/.2 in W-most L~Cage(C,n) by A143,JORDAN1I:27;
then (godo/.2)`1 = (W-min L~godo)`1 by A150,PSCOMP_1:88
.= W-bound L~godo by PSCOMP_1:84;
then godo/.2 in W-most L~godo by A151,A152,SPRECT_2:16;
then Rotate(godo,W-min L~godo)/.2 in W-most L~godo by A141,A150,FINSEQ_6:95
;
then reconsider godo as clockwise_oriented non constant standard
special_circular_sequence by JORDAN1I:27;
len US in dom US by FINSEQ_5:6;
then A153: US.len US = US/.len US by FINSEQ_4:def 4
.= Emax by JORDAN1F:7;
A154: E-max C in E-most C by PSCOMP_1:111;
A155: east_halfline E-max C misses L~go
proof
assume east_halfline E-max C meets L~go;
then consider p be set such that
A156: p in east_halfline E-max C and
A157: p in L~go by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A156;
p in L~US by A45,A157;
then p in east_halfline E-max C /\ L~Cage(C,n) by A134,A156,XBOOLE_0:def 3
;
then A158: p`1 = Ebo by A154,JORDAN1A:104;
then A159: p = Emax by A45,A157,JORDAN1J:46;
then Emax = Gik by A7,A153,A157,JORDAN1J:43;
then Gik`1 = Ga*(len Ga,k)`1 by A8,A11,A158,A159,JORDAN1A:92;
hence contradiction by A1,A13,A29,JORDAN1G:7;
end;
now assume east_halfline E-max C meets L~godo;
then A160: east_halfline E-max C meets (L~go \/ L~pion1) or
east_halfline E-max C meets L~do by A133,XBOOLE_1:70;
per cases by A160,XBOOLE_1:70;
suppose east_halfline E-max C meets L~go;
hence contradiction by A155;
suppose east_halfline E-max C meets L~pion1;
then consider p be set such that
A161: p in east_halfline E-max C and
A162: p in L~pion1 by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A161;
A163: p`1 <= Gik`1 by A77,A137,A148,A162,TOPREAL1:9;
k+1 <= len Ga by A1,NAT_1:38;
then k+1-1 <= len Ga-1 by REAL_1:49;
then A164: k <= len Ga-1 by XCMPLX_1:26;
then len Ga-1 > 0 by A1,AXIOMS:22;
then A165: k <= len Ga-'1 by A164,BINARITH:def 3;
len Ga-'1 <= len Ga by GOBOARD9:2;
then Gik`1 <= Ga*(len Ga-'1,1)`1 by A2,A8,A11,A19,A165,JORDAN1A:39;
then p`1 <= Ga*(len Ga-'1,1)`1 by A163,AXIOMS:22;
then p`1 <= E-bound C by A19,JORDAN8:15;
then A166: p`1 <= (E-max C)`1 by PSCOMP_1:104;
p`1 >= (E-max C)`1 by A161,JORDAN1A:def 3;
then A167: p`1 = (E-max C)`1 by A166,AXIOMS:21;
p`2 = (E-max C)`2 by A161,JORDAN1A:def 3;
then p = E-max C by A167,TOPREAL3:11;
hence contradiction by A5,A77,A121,A137,A162,XBOOLE_0:3;
suppose east_halfline E-max C meets L~do;
then consider p be set such that
A168: p in east_halfline E-max C and
A169: p in L~do by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A168;
p in L~LS by A52,A169;
then p in east_halfline E-max C /\ L~Cage(C,n)
by A134,A168,XBOOLE_0:def 3;
then A170: p`1 = Ebo by A154,JORDAN1A:104;
A171: (E-max C)`2 = p`2 by A168,JORDAN1A:def 3;
set RC = Rotate(Cage(C,n),Emax);
A172: E-max C in right_cell(RC,1) by JORDAN1I:9;
A173: 1+1 <= len LS by A23,AXIOMS:22;
LS = RC-:Wmin by JORDAN1G:26;
then A174: LSeg(LS,1) = LSeg(RC,1) by A173,SPPOL_2:9;
A175: L~RC = L~Cage(C,n) by REVROT_1:33;
A176: len RC = len Cage(C,n) by REVROT_1:14;
A177: GoB RC = GoB Cage(C,n) by REVROT_1:28
.= Ga by JORDAN1H:52;
A178: Emax in rng Cage(C,n) by SPRECT_2:50;
A179: RC is_sequence_on Ga by A130,REVROT_1:34;
A180: RC/.1 = E-max L~RC by A175,A178,FINSEQ_6:98;
then consider ii,jj be Nat such that
A181: [ii,jj+1] in Indices Ga and
A182: [ii,jj] in Indices Ga and
A183: RC/.1 = Ga*(ii,jj+1) and
A184: RC/.(1+1) = Ga*(ii,jj) by A81,A176,A179,JORDAN1I:25;
consider jj2 be Nat such that
A185: 1 <= jj2 & jj2 <= width Ga and
A186: Emax = Ga*(len Ga,jj2) by JORDAN1D:29;
A187: len Ga >= 4 by JORDAN8:13;
then len Ga >= 1 by AXIOMS:22;
then [len Ga,jj2] in Indices Ga by A185,GOBOARD7:10;
then A188: ii = len Ga by A175,A180,A181,A183,A186,GOBOARD1:21;
A189: 1 <= ii & ii <= len Ga & 1 <= jj+1 & jj+1 <= width Ga
by A181,GOBOARD5:1;
A190: 1 <= ii & ii <= len Ga & 1 <= jj & jj <= width Ga
by A182,GOBOARD5:1;
A191: ii+1 <> ii by NAT_1:38;
jj+1 > jj by NAT_1:38;
then jj+1+1 <> jj by NAT_1:38;
then A192: right_cell(RC,1) = cell(Ga,ii-'1,jj)
by A81,A176,A177,A181,A182,A183,A184,A191,GOBOARD5:
def 6;
A193: ii-'1+1 = ii by A189,AMI_5:4;
A194: ii-1 >= 4-1 by A187,A188,REAL_1:49;
then A195: ii-1 >= 1 by AXIOMS:22;
ii-1 >= 0 by A194,AXIOMS:22;
then A196: 1 <= ii-'1 by A195,BINARITH:def 3;
then A197: Ga*(ii-'1,jj)`2 <= p`2 & p`2 <= Ga*(ii-'1,jj+1)`2
by A171,A172,A189,A190,A192,A193,JORDAN9:19;
A198: ii-'1 < len Ga by A189,A193,NAT_1:38;
then A199: Ga*(ii-'1,jj)`2 = Ga*(1,jj)`2 by A190,A196,GOBOARD5:2
.= Ga*(ii,jj)`2 by A190,GOBOARD5:2;
A200: Ga*(ii-'1,jj+1)`2 = Ga*(1,jj+1)`2 by A189,A196,A198,GOBOARD5:2
.= Ga*(ii,jj+1)`2 by A189,GOBOARD5:2;
Ga*(len Ga,jj)`1 = Ebo & Ebo = Ga*(len Ga,jj+1)`1
by A8,A189,A190,JORDAN1A:92;
then p in LSeg(RC/.1,RC/.(1+1))
by A170,A183,A184,A188,A197,A199,A200,GOBOARD7:8;
then A201: p in LSeg(LS,1) by A81,A174,A176,TOPREAL1:def 5;
A202: p in LSeg(do,Index(p,do)) by A169,JORDAN3:42;
A203: do = mid(LS,Gij..LS,len LS) by A36,JORDAN1J:37;
A204: 1<=Gij..LS & Gij..LS<=len LS by A36,FINSEQ_4:31;
Gij..LS <> len LS by A28,A36,FINSEQ_4:29;
then A205: Gij..LS < len LS by A204,REAL_1:def 5;
A206: 1<=Index(p,do) & Index(p,do) < len do by A169,JORDAN3:41;
A207: Index(Gij,LS)+1 = Gij..LS by A31,A36,JORDAN1J:56;
consider t be Nat such that
A208: t in dom LS and
A209: LS.t = Gij by A36,FINSEQ_2:11;
A210: 1 <= t & t <= len LS by A208,FINSEQ_3:27;
then 1 < t by A31,A209,REAL_1:def 5;
then Index(Gij,LS)+1 = t by A209,A210,JORDAN3:45;
then A211: len L_Cut(LS,Gij) = len LS-Index(Gij,LS)
by A6,A28,A209,JORDAN3:61;
set tt = Index(p,do)+(Gij..LS)-'1;
A212: 1<=Index(Gij,LS) & 0+Index(Gij,LS) < len LS by A6,JORDAN3:41;
then A213: len LS-Index(Gij,LS) > 0 by REAL_1:86;
then Index(p,do) < len LS-'Index(Gij,LS) by A206,A211,BINARITH:def 3;
then Index(p,do)+1 <= len LS-'Index(Gij,LS) by NAT_1:38;
then Index(p,do) <= len LS-'Index(Gij,LS)-1 by REAL_1:84;
then Index(p,do) <= len LS-Index(Gij,LS)-1 by A213,BINARITH:def 3;
then A214: Index(p,do) <= len LS-Gij..LS by A207,XCMPLX_1:36;
then len LS-Gij..LS >= 1 by A206,AXIOMS:22;
then len LS-Gij..LS >= 0 by AXIOMS:22;
then Index(p,do) <= len LS-'Gij..LS by A214,BINARITH:def 3;
then Index(p,do) < len LS-'(Gij..LS)+1 by NAT_1:38;
then A215: LSeg(mid(LS,Gij..LS,len LS),Index(p,do)) =
LSeg(LS,Index(p,do)+(Gij..LS)-'1) by A204,A205,A206,JORDAN4:31;
A216: 1+1 <= Gij..LS by A207,A212,REAL_1:55;
then Index(p,do)+Gij..LS >= 1+1+1 by A206,REAL_1:55;
then A217: Index(p,do)+Gij..LS-1 >= 1+1+1-1 by REAL_1:49;
then A218: Index(p,do)+Gij..LS-1 >= 0 by AXIOMS:22;
then A219: tt >= 1+1 by A217,BINARITH:def 3;
A220: 2 in dom LS by A173,FINSEQ_3:27;
now per cases by A219,REAL_1:def 5;
suppose tt > 1+1;
then LSeg(LS,1) misses LSeg(LS,tt) by TOPREAL1:def 9;
hence contradiction by A201,A202,A203,A215,XBOOLE_0:3;
suppose A221: tt = 1+1;
then LSeg(LS,1) /\ LSeg(LS,tt) = {LS/.2} by A23,TOPREAL1:def 8;
then p in {LS/.2} by A201,A202,A203,A215,XBOOLE_0:def 3;
then A222: p = LS/.2 by TARSKI:def 1;
then A223: p..LS = 2 by A220,FINSEQ_5:44;
1+1 = Index(p,do)+(Gij..LS)-1 by A218,A221,BINARITH:def 3;
then 1+1+1 = Index(p,do)+(Gij..LS) by XCMPLX_1:27;
then A224: Gij..LS = 2 by A206,A216,JORDAN1E:10;
p in rng LS by A220,A222,PARTFUN2:4;
then p = Gij by A36,A223,A224,FINSEQ_5:10;
then Gij`1 = Ebo by A222,JORDAN1G:40;
then Gij`1 = Ga*(len Ga,j)`1 by A8,A10,JORDAN1A:92;
hence contradiction by A1,A12,A63,JORDAN1G:7;
end;
hence contradiction;
end;
then east_halfline E-max C c= (L~godo)` by SUBSET_1:43;
then consider W be Subset of TOP-REAL 2 such that
A225: W is_a_component_of (L~godo)` and
A226: east_halfline E-max C c= W by GOBOARD9:5;
east_halfline E-max C is not Bounded by JORDAN1C:9;
then W is not Bounded by A226,JORDAN2C:16;
then W is_outside_component_of L~godo by A225,JORDAN2C:def 4;
then W c= UBD L~godo by JORDAN2C:27;
then A227: east_halfline E-max C c= UBD L~godo by A226,XBOOLE_1:1;
E-max C in east_halfline E-max C by JORDAN1C:7;
then E-max C in UBD L~godo by A227;
then E-max C in LeftComp godo by GOBRD14:46;
then LA meets L~godo by A120,A121,A132,A140,JORDAN1J:36;
then A228: LA meets (L~go \/ L~pion1) or LA meets L~do by A133,XBOOLE_1:70;
A229: LA c= C by JORDAN1A:16;
per cases by A228,XBOOLE_1:70;
suppose LA meets L~go;
then LA meets L~Cage(C,n) by A135,XBOOLE_1:63;
then C meets L~Cage(C,n) by A229,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
suppose LA meets L~pion1;
hence contradiction by A5,A77,A137;
suppose LA meets L~do;
then LA meets L~Cage(C,n) by A135,XBOOLE_1:63;
then C meets L~Cage(C,n) by A229,XBOOLE_1:63;
hence contradiction by JORDAN10:5;
end;
theorem Th31:
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i,j,k be Nat;
set Ga = Gauge(C,n);
set US = Upper_Seq(C,n);
set LS = Lower_Seq(C,n);
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 Gij = Ga*(j,i);
set Gik = Ga*(k,i);
assume that
A1: 1 < j & j <= k & k < len Ga and
A2: 1 <= i & i <= width Ga and
A3: LSeg(Gij,Gik) /\ L~US = {Gik} and
A4: LSeg(Gij,Gik) /\ L~LS = {Gij} and
A5: LSeg(Gij,Gik) misses UA;
Gij in {Gij} by TARSKI:def 1;
then A6: Gij in L~LS by A4,XBOOLE_0:def 3;
Gik in {Gik} by TARSKI:def 1;
then A7: Gik in L~US by A3,XBOOLE_0:def 3;
A8: len Ga = width Ga by JORDAN8:def 1;
A9: j <> k by A1,A2,A6,A7,Th29;
A10: 1 <= j & j <= width Ga by A1,A8,AXIOMS:22;
A11: 1 <= k & k <= width Ga by A1,AXIOMS:22,JORDAN8:def 1;
A12: [j,i] in Indices Ga by A2,A8,A10,GOBOARD7:10;
A13: [k,i] in Indices Ga by A2,A8,A11,GOBOARD7:10;
A14: US is_sequence_on Ga by JORDAN1G:4;
A15: LS is_sequence_on Ga by JORDAN1G:5;
set go = R_Cut(US,Gik);
set do = L_Cut(LS,Gij);
A16: len US >= 3 by JORDAN1E:19;
then len US >= 1 by AXIOMS:22;
then 1 in dom US by FINSEQ_3:27;
then A17: US.1 = US/.1 by FINSEQ_4:def 4
.= Wmin by JORDAN1F:5;
A18: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A8,A11,JORDAN1A:94;
len Ga >= 4 by JORDAN8:13;
then A19: len Ga >= 1 by AXIOMS:22;
then A20: [1,k] in Indices Ga by A11,GOBOARD7:10;
then A21: Gik <> US.1 by A1,A13,A17,A18,JORDAN1G:7;
then reconsider go as being_S-Seq FinSequence of TOP-REAL 2
by A7,JORDAN3:70;
A22: [1,j] in Indices Ga by A10,A19,GOBOARD7:10;
A23: len LS >= 1+2 by JORDAN1E:19;
then len LS >= 1 by AXIOMS:22;
then A24: 1 in dom LS & len LS in dom LS by FINSEQ_3:27;
then A25: LS.len LS = LS/.len LS by FINSEQ_4:def 4
.= Wmin by JORDAN1F:8;
A26: Wmin`1 = Wbo by PSCOMP_1:84
.= Ga*(1,k)`1 by A8,A11,JORDAN1A:94;
A27: [j,i] in Indices Ga by A2,A8,A10,GOBOARD7:10;
then A28: Gij <> LS.len LS by A1,A20,A25,A26,JORDAN1G:7;
then reconsider do as being_S-Seq FinSequence of TOP-REAL 2
by A6,JORDAN3:69;
A29: [len Ga,k] in Indices Ga by A11,A19,GOBOARD7:10;
A30: LS.1 = LS/.1 by A24,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
Emax`1 = Ebo by PSCOMP_1:104
.= Ga*(len Ga,k)`1 by A8,A11,JORDAN1A:92;
then A31: Gij <> LS.1 by A1,A27,A29,A30,JORDAN1G:7;
A32: len go >= 1+1 by TOPREAL1:def 10;
A33: Gik in rng US by A2,A7,A8,A11,A14,JORDAN1J:40;
then A34: go is_sequence_on Ga by A14,JORDAN1J:38;
A35: len do >= 1+1 by TOPREAL1:def 10;
A36: Gij in rng LS by A2,A6,A8,A10,A15,JORDAN1J:40;
then A37: do is_sequence_on Ga by A15,JORDAN1J:39;
reconsider go as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A32,A34,JGRAPH_1:16,
JORDAN8:8;
reconsider do as non constant s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2) by A35,A37,JGRAPH_1:16,
JORDAN8:8;
A38: len go > 1 by A32,NAT_1:38;
then A39: len go in dom go by FINSEQ_3:27;
then A40: go/.len go = go.len go by FINSEQ_4:def 4
.= Gik by A7,JORDAN3:59;
len do >= 1 by A35,AXIOMS:22;
then 1 in dom do by FINSEQ_3:27;
then A41: do/.1 = do.1 by FINSEQ_4:def 4
.= Gij by A6,JORDAN3:58;
reconsider m = len go - 1 as Nat by A39,FINSEQ_3:28;
A42: m+1 = len go by XCMPLX_1:27;
then A43: len go-'1 = m by BINARITH:39;
A44: LSeg(go,m) c= L~go by TOPREAL3:26;
A45: L~go c= L~US by A7,JORDAN3:76;
then LSeg(go,m) c= L~US by A44,XBOOLE_1:1;
then A46: LSeg(go,m) /\ LSeg(Gik,Gij) c= {Gik} by A3,XBOOLE_1:26;
m >= 1 by A32,REAL_1:84;
then A47: LSeg(go,m) = LSeg(go/.m,Gik) by A40,A42,TOPREAL1:def 5;
{Gik} c= LSeg(go,m) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gik};
then A48: x = Gik by TARSKI:def 1;
A49: Gik in LSeg(go,m) by A47,TOPREAL1:6;
Gik in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(go,m) /\ LSeg(Gik,Gij) by A48,A49,XBOOLE_0:def 3;
end;
then A50: LSeg(go,m) /\ LSeg(Gik,Gij) = {Gik} by A46,XBOOLE_0:def 10;
A51: LSeg(do,1) c= L~do by TOPREAL3:26;
A52: L~do c= L~LS by A6,JORDAN3:77;
then LSeg(do,1) c= L~LS by A51,XBOOLE_1:1;
then A53: LSeg(do,1) /\ LSeg(Gik,Gij) c= {Gij} by A4,XBOOLE_1:26;
A54: LSeg(do,1) = LSeg(Gij,do/.(1+1)) by A35,A41,TOPREAL1:def 5;
{Gij} c= LSeg(do,1) /\ LSeg(Gik,Gij)
proof
let x be set;
assume x in {Gij};
then A55: x = Gij by TARSKI:def 1;
A56: Gij in LSeg(do,1) by A54,TOPREAL1:6;
Gij in LSeg(Gik,Gij) by TOPREAL1:6;
hence x in LSeg(do,1) /\ LSeg(Gik,Gij) by A55,A56,XBOOLE_0:def 3;
end;
then A57: LSeg(Gik,Gij) /\ LSeg(do,1) = {Gij} by A53,XBOOLE_0:def 10;
A58: go/.1 = US/.1 by A7,SPRECT_3:39
.= Wmin by JORDAN1F:5;
then A59: go/.1 = LS/.len LS by JORDAN1F:8
.= do/.len do by A6,JORDAN1J:35;
A60: rng go c= L~go & rng do c= L~do by A32,A35,SPPOL_2:18;
A61: {go/.1} c= L~go /\ L~do
proof
let x be set;
assume x in {go/.1};
then x = go/.1 by TARSKI:def 1;
then x in rng go & x in rng do by A59,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~do by A60,XBOOLE_0:def 3;
end;
A62: LS.1 = LS/.1 by A24,FINSEQ_4:def 4
.= Emax by JORDAN1F:6;
A63: [len Ga,j] in Indices Ga by A10,A19,GOBOARD7:10;
L~go /\ L~do c= {go/.1}
proof
let x be set;
assume x in L~go /\ L~do;
then A64: x in L~go & x in L~do by XBOOLE_0:def 3;
then x in L~US /\ L~LS by A45,A52,XBOOLE_0:def 3;
then x in {Wmin,Emax} by JORDAN1E:20;
then A65: x = Wmin or x = Emax by TARSKI:def 2;
now assume x = Emax;
then A66: Emax = Gij by A6,A62,A64,JORDAN1E:11;
Ga*(len Ga,j)`1 = Ebo by A8,A10,JORDAN1A:92;
then Emax`1 <> Ebo by A1,A12,A63,A66,JORDAN1G:7;
hence contradiction by PSCOMP_1:104;
end;
hence x in {go/.1} by A58,A65,TARSKI:def 1;
end;
then A67: L~go /\ L~do = {go/.1} by A61,XBOOLE_0:def 10;
set W2 = go/.2;
A68: 2 in dom go by A32,FINSEQ_3:27;
A69: Gik..US >= 1 by A33,FINSEQ_4:31;
A70: now assume Gij`1 = Wbo;
then Ga*(1,j)`1 = Ga*(j,i)`1 by A8,A10,JORDAN1A:94;
hence contradiction by A1,A12,A22,JORDAN1G:7;
end;
go = mid(US,1,Gik..US) by A33,JORDAN1G:57
.= US|(Gik..US) by A69,JORDAN3:25;
then A71: W2 = US/.2 by A68,TOPREAL1:1;
A72: Wmin in rng go by A58,FINSEQ_6:46;
set pion = <*Gik,Gij*>;
A73: now let n be Nat;
assume n in dom pion;
then n in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then n = 1 or n = 2 by TARSKI:def 2;
then pion/.n = Gik or pion/.n = Gij by FINSEQ_4:26;
hence ex j,i be Nat st [j,i] in Indices Ga & pion/.n = Ga*(j,i)
by A12,A13;
end;
A74: Gik <> Gij by A9,A12,A13,GOBOARD1:21;
Gik`2 = Ga*(1,i)`2 by A2,A8,A11,GOBOARD5:2
.= Gij`2 by A2,A8,A10,GOBOARD5:2;
then LSeg(Gik,Gij) is horizontal by SPPOL_1:36;
then pion is_S-Seq by A74,JORDAN1B:9;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A75: pion1 is_sequence_on Ga and
A76: pion1 is_S-Seq and
A77: L~pion = L~pion1 and
A78: pion/.1 = pion1/.1 and
A79: pion/.len pion = pion1/.len pion1 and
A80: len pion <= len pion1 by A73,GOBOARD3:2;
reconsider pion1 as being_S-Seq FinSequence of TOP-REAL 2 by A76;
set godo = go^'pion1^'do;
len Cage(C,n) > 4 by GOBOARD7:36;
then A81: 1+1 <= len Cage(C,n) by AXIOMS:22;
then A82: 1+1 <= len Rotate(Cage(C,n),Wmin) by REVROT_1:14;
len (go^'pion1) >= len go by TOPREAL8:7;
then A83: len (go^'pion1) >= 1+1 by A32,AXIOMS:22;
then A84: len (go^'pion1) > 1+0 by NAT_1:38;
len godo >= len (go^'pion1) by TOPREAL8:7;
then A85: 1+1 <= len godo by A83,AXIOMS:22;
A86: US is_sequence_on Ga by JORDAN1G:4;
A87: go/.len go = pion1/.1 by A40,A78,FINSEQ_4:26;
then A88: go^'pion1 is_sequence_on Ga by A34,A75,TOPREAL8:12;
A89: (go^'pion1)/.len (go^'pion1) = pion/.len pion by A79,AMISTD_1:6
.= pion/.2 by FINSEQ_1:61
.= do/.1 by A41,FINSEQ_4:26;
then A90: godo is_sequence_on Ga by A37,A88,TOPREAL8:12;
LSeg(pion1,1) c= L~<*Gik,Gij*> by A77,TOPREAL3:26;
then LSeg(pion1,1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A91: LSeg(go,len go-'1) /\ LSeg(pion1,1) c= {Gik}
by A43,A50,XBOOLE_1:27;
A92: len pion1 >= 1+1 by A80,FINSEQ_1:61;
{Gik} c= LSeg(go,m) /\ LSeg(pion1,1)
proof
let x be set;
assume x in {Gik};
then A93: x = Gik by TARSKI:def 1;
A94: Gik in LSeg(go,m) by A47,TOPREAL1:6;
Gik in LSeg(pion1,1) by A40,A87,A92,TOPREAL1:27;
hence x in LSeg(go,m) /\ LSeg(pion1,1) by A93,A94,XBOOLE_0:def 3;
end;
then LSeg(go,len go-'1) /\ LSeg(pion1,1) = { go/.len go }
by A40,A43,A91,XBOOLE_0:def 10;
then A95: go^'pion1 is unfolded by A87,TOPREAL8:34;
len pion1 >= 2+0 by A80,FINSEQ_1:61;
then A96: len pion1-2 >= 0 by REAL_1:84;
A97: len (go^'pion1)-1 >= 0 by A84,REAL_1:84;
len (go^'pion1)+1-1 = len go+len pion1-1 by GRAPH_2:13;
then len (go^'pion1)-1 = len go+len pion1-1-1 by XCMPLX_1:26
.= len go + len pion1-(1+1) by XCMPLX_1:36
.= len go + (len pion1-2) by XCMPLX_1:29
.= len go + (len pion1-'2) by A96,BINARITH:def 3;
then A98: len (go^'pion1)-'1 = len go + (len pion1-'2)
by A97,BINARITH:def 3;
A99: len pion1-1 >= 1 by A92,REAL_1:84;
then A100: len pion1-1 >= 0 by AXIOMS:22;
then A101: len pion1-'1 = len pion1-1 by BINARITH:def 3;
A102: len pion1-'2+1 = len pion1-2+1 by A96,BINARITH:def 3
.= len pion1-(2-1) by XCMPLX_1:37
.= len pion1-'1 by A100,BINARITH:def 3;
len pion1-1+1 <= len pion1 by XCMPLX_1:27;
then A103: len pion1-'1 < len pion1 by A101,NAT_1:38;
LSeg(pion1,len pion1-'1) c= L~<*Gik,Gij*> by A77,TOPREAL3:26;
then LSeg(pion1,len pion1-'1) c= LSeg(Gik,Gij) by SPPOL_2:21;
then A104: LSeg(pion1,len pion1-'1) /\ LSeg(do,1) c= {Gij}
by A57,XBOOLE_1:27;
{Gij} c= LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
proof
let x be set;
assume x in {Gij};
then A105: x = Gij by TARSKI:def 1;
A106: Gij in LSeg(do,1) by A54,TOPREAL1:6;
A107: len pion1-'1+1 = len pion1 by A101,XCMPLX_1:27;
then pion1/.(len pion1-'1+1) = pion/.2 by A79,FINSEQ_1:61
.= Gij by FINSEQ_4:26;
then Gij in LSeg(pion1,len pion1-'1) by A99,A101,A107,TOPREAL1:27;
hence x in LSeg(pion1,len pion1-'1) /\ LSeg(do,1)
by A105,A106,XBOOLE_0:def 3;
end;
then LSeg(pion1,len pion1-'1) /\ LSeg(do,1) = {Gij} by A104,XBOOLE_0:def 10
;
then A108: LSeg(go^'pion1,len go+(len pion1-'2)) /\ LSeg(do,1) =
{(go^'pion1)/.len (go^'pion1)} by A41,A87,A89,A102,A103,TOPREAL8:31;
A109: (go^'pion1) is non trivial by A83,SPPOL_1:2;
A110: rng pion1 c= L~pion1 by A92,SPPOL_2:18;
A111: {pion1/.1} c= L~go /\ L~pion1
proof
let x be set;
assume x in {pion1/.1};
then x = pion1/.1 by TARSKI:def 1;
then x in rng go & x in rng pion1 by A87,FINSEQ_6:46,REVROT_1:3;
hence x in L~go /\ L~pion1 by A60,A110,XBOOLE_0:def 3;
end;
L~go /\ L~pion1 c= {pion1/.1}
proof
let x be set;
assume x in L~go /\ L~pion1;
then x in L~go & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~US by A45,XBOOLE_0:def 3;
hence x in {pion1/.1} by A3,A40,A77,A87,SPPOL_2:21;
end;
then A112: L~go /\ L~pion1 = {pion1/.1} by A111,XBOOLE_0:def 10;
then A113: (go^'pion1) is s.n.c. by A87,JORDAN1J:54;
rng go /\ rng pion1 c= {pion1/.1} by A60,A110,A112,XBOOLE_1:27;
then A114: go^'pion1 is one-to-one by JORDAN1J:55;
A115: pion/.len pion = pion/.2 by FINSEQ_1:61
.= do/.1 by A41,FINSEQ_4:26;
A116: {pion1/.len pion1} c= L~do /\ L~pion1
proof
let x be set;
assume x in {pion1/.len pion1};
then x = pion1/.len pion1 by TARSKI:def 1;
then x in rng do & x in rng pion1 by A79,A115,FINSEQ_6:46,REVROT_1:3;
hence x in L~do /\ L~pion1 by A60,A110,XBOOLE_0:def 3;
end;
L~do /\ L~pion1 c= {pion1/.len pion1}
proof
let x be set;
assume x in L~do /\ L~pion1;
then x in L~do & x in L~pion1 by XBOOLE_0:def 3;
then x in L~pion1 /\ L~LS by A52,XBOOLE_0:def 3;
hence x in {pion1/.len pion1} by A4,A41,A77,A79,A115,SPPOL_2:21;
end;
then A117: L~do /\ L~pion1 = {pion1/.len pion1} by A116,XBOOLE_0:def 10;
A118: L~(go^'pion1) /\ L~do = (L~go \/ L~pion1) /\ L~do by A87,TOPREAL8:35
.= {go/.1} \/ {do/.1} by A67,A79,A115,A117,XBOOLE_1:23
.= {(go^'pion1)/.1} \/ {do/.1} by AMISTD_1:5
.= {(go^'pion1)/.1,do/.1} by ENUMSET1:41;
do/.len do = (go^'pion1)/.1 by A59,AMISTD_1:5;
then reconsider godo as non constant standard special_circular_sequence
by A85,A89,A90,A95,A98,A108,A109,A113,A114,A118,JORDAN8:7,8,TOPREAL8
:11,33,34;
A119: UA is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
then A120: UA is connected by JORDAN6:11;
A121: W-min C in UA & E-max C in UA by A119,TOPREAL1:4;
set ff = Rotate(Cage(C,n),Wmin);
Wmin in rng Cage(C,n) by SPRECT_2:47;
then A122: ff/.1 = Wmin by FINSEQ_6:98;
A123: L~ff = L~Cage(C,n) by REVROT_1:33;
then A124: (W-max L~ff)..ff > 1 by A122,SPRECT_5:23;
(W-max L~ff)..ff <= (N-min L~ff)..ff by A122,A123,SPRECT_5:24;
then A125: (N-min L~ff)..ff > 1 by A124,AXIOMS:22;
(N-min L~ff)..ff < (N-max L~ff)..ff by A122,A123,SPRECT_5:25;
then A126: (N-max L~ff)..ff > 1 by A125,AXIOMS:22;
(N-max L~ff)..ff <= (E-max L~ff)..ff by A122,A123,SPRECT_5:26;
then A127: Emax..ff > 1 by A123,A126,AXIOMS:22;
A128: now assume A129: Gik..US <= 1;
Gik..US >= 1 by A33,FINSEQ_4:31;
then Gik..US = 1 by A129,AXIOMS:21;
then Gik = US/.1 by A33,FINSEQ_5:41;
hence contradiction by A17,A21,JORDAN1F:5;
end;
A130: Cage(C,n) is_sequence_on Ga by JORDAN9:def 1;
then A131: ff is_sequence_on Ga by REVROT_1:34;
A132: right_cell(godo,1,Ga)\L~godo c= RightComp godo by A85,A90,JORDAN9:29;
A133: L~godo = L~(go^'pion1) \/ L~do by A89,TOPREAL8:35
.= L~go \/ L~pion1 \/ L~do by A87,TOPREAL8:35;
L~Cage(C,n) = L~US \/ L~LS by JORDAN1E:17;
then A134: L~US c= L~Cage(C,n) & L~LS c= L~Cage(C,n) by XBOOLE_1:7;
then A135: L~go c= L~Cage(C,n) & L~do c= L~Cage(C,n)
by A45,A52,XBOOLE_1:1;
A136: W-min C in C by SPRECT_1:15;
A137: L~pion = LSeg(Gik,Gij) by SPPOL_2:21;
A138: now assume W-min C in L~godo;
then A139: W-min C in L~