:: Properties of the Internal Approximation of {J}ordan's Curve
:: by Robert Milewski
::
:: Received June 27, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, GOBOARD5, JORDAN2C, TOPREAL1, GOBOARD9,
CONNSP_1, SUBSET_1, GOBOARD1, FINSEQ_1, EUCLID, XXREAL_0, ARYTM_3,
RCOMP_1, MATRIX_1, PARTFUN1, RELAT_1, ARYTM_1, PRE_TOPC, TREES_1, TOPS_1,
MCART_1, REAL_1, RELAT_2, TOPREAL2, JORDAN8, JORDAN1H, JORDAN11, TARSKI,
RLTOPSP1, JORDAN13, XBOOLE_0, CARD_1, GOBRD13, ORDINAL4, STRUCT_0,
PSCOMP_1, SPPOL_1, NEWTON, COMPLEX1, JORDAN14, CONVEX1, XXREAL_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, XREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, PARTFUN1, FINSEQ_1,
SEQM_3, STRUCT_0, MATRIX_0, PRE_TOPC, TOPREAL2, TOPS_1, COMPTS_1,
CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, SPPOL_1,
PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, GOBRD13, JORDAN1H, JORDAN11,
JORDAN13, XXREAL_0;
constructors REAL_1, FINSEQ_4, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPREAL4,
JORDAN1, PSCOMP_1, GOBOARD9, JORDAN2C, JORDAN8, JORDAN1H, JORDAN11,
JORDAN13, CONVEX1, RELSET_1, GOBRD13;
registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0,
PRE_TOPC, TOPS_1, COMPTS_1, TOPREAL1, TOPREAL2, TOPREAL5, SPRECT_2,
SPRECT_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD14, EUCLID, RLTOPSP1,
JORDAN1, XREAL_0, NAT_1, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2,
TARSKI, PSCOMP_1, FINSEQ_5, GOBOARD7, TOPREAL1, JORDAN5B, GOBOARD5,
GOBOARD9, SUBSET_1, GOBRD11, SPRECT_3, GOBOARD6, TOPS_1, JORDAN8,
GOBRD13, SPRECT_4, CONNSP_1, XBOOLE_0, XBOOLE_1, NEWTON, GOBRD14,
TOPREAL6, INT_1, JORDAN2C, PRE_TOPC, JORDAN9, JORDAN1H, TSEP_1, GOBRD12,
JORDAN1A, JORDAN1C, JORDAN11, JORDAN13, XREAL_1, XXREAL_0, CARD_1,
MATRIX_0, NAT_D, XREAL_0, RLTOPSP1, SEQM_3;
schemes NAT_1;
begin
theorem Th1:
for f be non constant standard special_circular_sequence holds
BDD L~f = RightComp f or BDD L~f = LeftComp f
proof
let f be non constant standard special_circular_sequence;
BDD L~f is_inside_component_of L~f by JORDAN2C:108;
then BDD L~f is_a_component_of (L~f)` by JORDAN2C:def 2;
hence thesis by JORDAN1H:24;
end;
theorem
for f be non constant standard special_circular_sequence holds UBD L~f
= RightComp f or UBD L~f = LeftComp f
proof
let f be non constant standard special_circular_sequence;
UBD L~f is_outside_component_of L~f by JORDAN2C:68;
then UBD L~f is_a_component_of (L~f)` by JORDAN2C:def 3;
hence thesis by JORDAN1H:24;
end;
theorem
for G be Go-board for f be FinSequence of TOP-REAL 2
for k be Nat holds 1 <= k & k+1 <= len f & f is_sequence_on G
implies left_cell(f,k,G) is closed
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
let k be Nat;
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: f is_sequence_on G;
consider i1,j1,i2,j2 be Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) and
A6: [i2,j2] in Indices G and
A7: f/.(k+1) = G*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
i1 = i2 & j1 = j2+1 by A1,A2,A3,JORDAN8:3;
i1 = i2 & j1+1 = j2 & left_cell(f,k,G) = cell(G,i1-'1,j1) or i1+1 = i2 &
j1 = j2 & left_cell(f,k,G) = cell(G,i1,j1) or i1 = i2+1 & j1 = j2 & left_cell(f
,k,G) = cell(G,i2,j2-'1) or i1 = i2 & j1 = j2+1 & left_cell(f,k,G) = cell(G,i1,
j2) by A1,A2,A3,A4,A5,A6,A7,A8,GOBRD13:def 3;
hence thesis by GOBRD11:33;
end;
theorem Th4:
for G be Go-board for p be Point of TOP-REAL 2
for i,j be Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
holds p in Int cell(G
,i,j) iff G*(i,j)`1 < p`1 & p`1 < G*(i+1,j)`1 & G*(i,j)`2 < p`2 & p`2 < G*(i,j+
1)`2
proof
let G be Go-board;
let p be Point of TOP-REAL 2;
let i,j be Nat;
assume that
A1: 1 <= i and
A2: i+1 <= len G and
A3: 1 <= j and
A4: j+1 <= width G;
set Z = {|[r,s]| where r,s is Real
: G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,
j)`2 < s & s < G*(1,j+1)`2};
A5: j < width G by A4,NAT_1:13;
i+1 >= 1 by NAT_1:11;
then
A6: G*(i+1,1)`1 = G*(i+1,j)`1 by A2,A3,A5,GOBOARD5:2;
A7: i < len G by A2,NAT_1:13;
then
A8: G*(1,j)`2 = G*(i,j)`2 by A1,A3,A5,GOBOARD5:1;
j+1 >= 1 by NAT_1:11;
then
A9: G*(1,j+1)`2 = G*(i,j+1)`2 by A1,A4,A7,GOBOARD5:1;
A10: G*(i,1)`1 = G*(i,j)`1 by A1,A3,A7,A5,GOBOARD5:2;
thus p in Int cell(G,i,j) implies G*(i,j)`1 < p`1 & p`1 < G*(i+1,j)`1 & G*(i
,j)`2 < p`2 & p`2 < G*(i,j+1)`2
proof
assume p in Int cell(G,i,j);
then p in Z by A1,A3,A7,A5,GOBOARD6:26;
then
ex r,s be Real st p = |[r,s]| & G*(i,1)`1 < r & r < G*(i +1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2;
hence thesis by A10,A6,A8,A9,EUCLID:52;
end;
assume that
A11: G*(i,j)`1 < p`1 and
A12: p`1 < G*(i+1,j)`1 and
A13: G*(i,j)`2 < p`2 and
A14: p`2 < G*(i,j+1)`2;
p = |[p`1,p`2]| by EUCLID:53;
then p in Z by A10,A6,A8,A9,A11,A12,A13,A14;
hence thesis by A1,A3,A7,A5,GOBOARD6:26;
end;
theorem Th5:
for f be non constant standard special_circular_sequence holds
BDD L~f is connected
proof
let f be non constant standard special_circular_sequence;
BDD L~f = RightComp f or BDD L~f = LeftComp f by Th1;
hence thesis;
end;
registration
let f be non constant standard special_circular_sequence;
cluster BDD L~f -> connected;
coherence by Th5;
end;
definition
let C be Simple_closed_curve;
let n be Nat;
func SpanStart(C,n) -> Point of TOP-REAL 2 equals
Gauge(C,n)*(X-SpanStart(C,
n),Y-SpanStart(C,n));
coherence;
end;
theorem Th6:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds SpanStart(C,n) in BDD C
proof
let C be Simple_closed_curve;
let n be Nat;
A1: 1 <= X-SpanStart(C,n)-'1 by JORDAN1H:50;
A2: X-SpanStart(C,n)-'1 < len Gauge(C,n) by JORDAN1H:50;
assume
A3: n is_sufficiently_large_for C;
then
A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) c= BDD C by
JORDAN11:6;
A5: Y-SpanStart(C,n) <= width Gauge(C,n) by A3,JORDAN11:7;
1 < Y-SpanStart(C,n) by A3,JORDAN11:7;
then LSeg(Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*(
X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n))) c= cell(Gauge(C,n),X-SpanStart(C,n)-'1
,Y-SpanStart(C,n)) by A1,A2,A5,GOBOARD5:22;
then
A6: LSeg(Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*(
X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n))) c= BDD C by A4;
A7: 2 < X-SpanStart(C,n) by JORDAN1H:49;
Gauge(C,n)*(X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n)) in LSeg(Gauge(C,n)*
(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)), Gauge(C,n)*(X-SpanStart(C,n)-'1+1,
Y-SpanStart(C,n))) by RLTOPSP1:68;
then Gauge(C,n)*(X-SpanStart(C,n)-'1+1,Y-SpanStart(C,n)) in BDD C by A6;
hence thesis by A7,XREAL_1:235,XXREAL_0:2;
end;
theorem Th7:
for C be Simple_closed_curve for n,k be Nat st n
is_sufficiently_large_for C holds 1 <= k & k+1 <= len Span(C,n) implies
right_cell(Span(C,n),k,Gauge(C,n)) misses C & left_cell(Span(C,n),k,Gauge(C,n))
meets C
proof
let C be Simple_closed_curve;
let n,k be Nat;
set G = Gauge(C,n);
set f = Span(C,n);
defpred P[Nat] means
for m be Nat st 1 <= m & m+1 <=
len(f|$1) holds right_cell(f|$1,m,G) misses C & left_cell(f|$1,m,G) meets C;
A1: f|len f = f by FINSEQ_1:58;
assume
A2: n is_sufficiently_large_for C;
then
A3: f is_sequence_on G by JORDAN13:def 1;
A4: f/.2 = G*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) by A2,JORDAN13:def 1;
A5: f/.1 = G*(X-SpanStart(C,n),Y-SpanStart(C,n)) by A2,JORDAN13:def 1;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: for m be Nat st 1 <= m & m+1 <= len(f|k) holds
right_cell(f|k,m,G) misses C & left_cell(f|k,m,G) meets C;
A8: f|(k+1) is_sequence_on G by A3,GOBOARD1:22;
A9: f|k is_sequence_on G by A3,GOBOARD1:22;
per cases;
suppose
A10: k >= len f;
then
A11: f|(k+1) = f by FINSEQ_1:58,NAT_1:12;
f|k = f by A10,FINSEQ_1:58;
hence thesis by A7,A11;
end;
suppose
A12: k < len f;
let m be Nat;
assume that
A13: 1 <= m and
A14: m+1 <= len(f|(k+1));
A15: k+1 <= len f by A12,NAT_1:13;
then
A16: len(f|(k+1)) = k+1 by FINSEQ_1:59;
A17: len(f|k) = k by A12,FINSEQ_1:59;
now
per cases by NAT_1:25;
suppose
A18: k = 0;
1 <= m+1 by NAT_1:12;
then m+1 = 0+1 by A14,A18,XXREAL_0:1;
hence thesis by A13;
end;
suppose
A19: k = 1;
set j = Y-SpanStart(C,n);
set i = X-SpanStart(C,n);
A20: f|(k+1) = <*G*(i,j),G*(i-'1,j)*> by A5,A4,A15,A19,FINSEQ_5:81;
then
A21: (f|(k+1))/.1 = G*(i,j) by FINSEQ_4:17;
1+1 <= m+1 by A13,XREAL_1:6;
then
A22: m+1 = 1+1 by A16,A14,A19,XXREAL_0:1;
A23: [i-'1,j] in Indices G by A2,JORDAN11:9;
A24: [i,j] in Indices G by A2,JORDAN11:8;
i-'1 <= i by NAT_D:35;
then
A25: i+1 <> i-'1 by NAT_1:13;
A26: j <> j+1;
A27: (f|(k+1))/.2 = G*(i-'1,j) by A20,FINSEQ_4:17;
then right_cell(f|(k+1),m,G) = cell(G,i-'1,j) by A8,A14,A21,A24,A23
,A22,A26,A25,GOBRD13:def 2;
hence right_cell(f|(k+1),m,G) misses C by A2,JORDAN11:11;
left_cell(f|(k+1),m,G) = cell(G,i-'1,j-'1) by A8,A14,A21,A27,A24,A23
,A22,A26,A25,GOBRD13:def 3;
hence left_cell(f|(k+1),m,G) meets C by A2,JORDAN11:10;
end;
suppose
A28: k > 1;
A29: len(f|k) <= len f by FINSEQ_5:16;
A30: 1 <= (len(f|k))-'1 by A17,A28,NAT_D:49;
A31: (len(f|k))-'1+1 = len(f|k) by A17,A28,XREAL_1:235;
then
A32: (len(f|k))-'1+(1+1) = (len(f|k))+1;
now
per cases;
suppose
A33: m+1 = len(f|(k+1));
left_cell(f|k,(len(f|k))-'1,G) meets C by A7,A30,A31;
then
A34: left_cell(f,(len(f|k))-'1,G) meets C by A3,A17,A30,A31,A29,
GOBRD13:31;
consider i1,j1,i2,j2 be Nat such that
A35: [i1,j1] in Indices G and
A36: f/.(len(f|k)-'1) = G*(i1,j1) and
A37: [i2,j2] in Indices G and
A38: f/.(len(f|k)) = G*(i2,j2) and
i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1
= j2 or i1 = i2 & j1 = j2+1 by A3,A12,A17,A30,A31,JORDAN8:3;
1 <= i2 by A37,MATRIX_0:32;
then
A39: i2-'1+1 = i2 by XREAL_1:235;
A40: 1 <= j2 by A37,MATRIX_0:32;
then
A41: j2-'1+1 = j2 by XREAL_1:235;
right_cell(f|k,(len(f|k))-'1,G) misses C by A7,A30,A31;
then
A42: right_cell(f,(len(f|k))-'1,G) misses C by A3,A17,A30,A31,A29,
GOBRD13:31;
now
per cases;
suppose
A43: front_right_cell(f,(len(f|k))-'1,G) misses C &
front_left_cell(f,(len(f|k))-'1,G) misses C;
then
A44: f turns_left (len(f|k))-'1,G by A2,A15,A17,A30,A32,
JORDAN13:def 1;
now
per cases by A31,A35,A36,A37,A38,A44,GOBRD13:def 7;
suppose that
A45: i1 = i2 & j1+1 = j2 and
A46: [i2-'1,j2] in Indices G and
A47: f/.((len(f|k))-'1+2) = G*(i2-'1,j2);
cell(G,i1-'1,j1+1) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A43,A45,GOBRD13:34;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A39,A45,A46,A47,GOBRD13:26;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
A48: j1+1-'1 = j1 by NAT_D:34;
cell(G,i1-'1,j1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A34,A45,GOBRD13:21;
then
left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33
,A37,A38,A39,A45,A46,A47,A48,GOBRD13:25;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A49: i1+1 = i2 & j1 = j2 and
A50: [i2,j2+1] in Indices G and
A51: f/.((len(f|k))-'1+2) = G*(i2,j2+1);
cell(G,i2,j2) misses C by A3,A30,A31,A29,A35,A36,A37,A38
,A43,A49,GOBRD13:36;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A50,A51,GOBRD13:22;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
A52: i1+1-'1 = i1 by NAT_D:34;
cell(G,i1,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37
,A38,A34,A49,GOBRD13:23;
then
left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33
,A37,A38,A49,A50,A51,A52,GOBRD13:21;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A53: i1 = i2+1 & j1 = j2 and
A54: [i2,j2-'1] in Indices G and
A55: f/.((len(f|k))-'1+2) = G*(i2,j2-'1);
cell(G,i2-'1,j2-'1) misses C by A3,A30,A31,A29,A35,A36
,A37,A38,A43,A53,GOBRD13:38;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A41,A54,A55,GOBRD13:28;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A34,A53,GOBRD13:25;
then
left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33
,A37,A38,A41,A54,A55,GOBRD13:27;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A56: i1 = i2 & j1 = j2+1 and
A57: [i2+1,j2] in Indices G and
A58: f/.((len(f|k))-'1+2) = G*(i2+1,j2);
cell(G,i1,j2-'1) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A43,A56,GOBRD13:40;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A56,A57,A58,GOBRD13:24;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i1,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37
,A38,A34,A56,GOBRD13:27;
then
left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31,A33
,A37,A38,A56,A57,A58,GOBRD13:23;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
end;
hence thesis;
end;
suppose
A59: front_right_cell(f,(len(f|k))-'1,G) misses C &
front_left_cell(f,(len(f|k))-'1,G) meets C;
then
A60: f goes_straight (len(f|k))-'1,G by A2,A15,A17,A30,A32,
JORDAN13:def 1;
now
per cases by A31,A35,A36,A37,A38,A60,GOBRD13:def 8;
suppose that
A61: i1 = i2 & j1+1 = j2 and
A62: [i2,j2+1] in Indices G and
A63: f/.((len(f|k))-'1+2) = G*(i2,j2+1);
cell(G,i1,j1+1) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A59,A61,GOBRD13:35;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A61,A62,A63,GOBRD13:22;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2-'1,j2) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A59,A61,GOBRD13:34;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A62,A63,GOBRD13:21;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A64: i1+1 = i2 & j1 = j2 and
A65: [i2+1,j2] in Indices G and
A66: f/.((len(f|k))-'1+2) = G*(i2+1,j2);
cell(G,i1+1,j1-'1) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A59,A64,GOBRD13:37;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A64,A65,A66,GOBRD13:24;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i1+1,j1) meets C by A3,A12,A17,A30,A31,A35,A36,A37
,A38,A59,A64,GOBRD13:36;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A64,A65,A66,GOBRD13:23;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A67: i1 = i2+1 & j1 = j2 and
A68: [i2-'1,j2] in Indices G and
A69: f/.((len(f|k))-'1+2) = G*(i2-'1,j2);
cell(G,i2-'1,j2) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A59,A67,GOBRD13:39;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A39,A68,A69,GOBRD13:26;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2-'1,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A59,A67,GOBRD13:38;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A39,A68,A69,GOBRD13:25;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A70: i1 = i2 & j1 = j2+1 and
A71: [i2,j2-'1] in Indices G and
A72: f/.((len(f|k))-'1+2) = G*(i2,j2-'1);
A73: j2-'1+1=j2 by A40,XREAL_1:235;
cell(G,i2-'1,j2-'1) misses C by A3,A30,A31,A29,A35,A36
,A37,A38,A59,A70,GOBRD13:41;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A71,A72,A73,GOBRD13:28;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A59,A70,GOBRD13:40;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A41,A71,A72,GOBRD13:27;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
end;
hence thesis;
end;
suppose
A74: front_right_cell(f,(len(f|k))-'1,G) meets C;
then
A75: f turns_right (len(f|k))-'1,G by A2,A15,A17,A30,A32,
JORDAN13:def 1;
now
per cases by A31,A35,A36,A37,A38,A75,GOBRD13:def 6;
suppose that
A76: i1 = i2 & j1+1 = j2 and
A77: [i2+1,j2] in Indices G and
A78: f/.((len(f|k))-'1+2) = G*(i2+1,j2);
A79: j1+1-'1 = j1 by NAT_D:34;
cell(G,i1,j1) misses C by A3,A30,A31,A29,A35,A36,A37,A38
,A42,A76,GOBRD13:22;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A76,A77,A78,A79,GOBRD13:24;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2,j2) meets C by A3,A12,A17,A30,A31,A35,A36,A37
,A38,A74,A76,GOBRD13:35;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A77,A78,GOBRD13:23;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A80: i1+1 = i2 & j1 = j2 and
A81: [i2,j2-'1] in Indices G and
A82: f/.((len(f|k))-'1+2) = G*(i2,j2-'1);
A83: i1+1-'1 = i1 by NAT_D:34;
cell(G,i1,j1-'1) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A42,A80,GOBRD13:24;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A41,A80,A81,A82,A83,GOBRD13:28;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A74,A80,GOBRD13:37;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A41,A81,A82,GOBRD13:27;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A84: i1 = i2+1 & j1 = j2 and
A85: [i2,j2+1] in Indices G and
A86: f/.((len(f|k))-'1+2) = G*(i2,j2+1);
cell(G,i2,j2) misses C by A3,A30,A31,A29,A35,A36,A37,A38
,A42,A84,GOBRD13:26;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A85,A86,GOBRD13:22;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2-'1,j2) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A74,A84,GOBRD13:39;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A85,A86,GOBRD13:21;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
suppose that
A87: i1 = i2 & j1 = j2+1 and
A88: [i2-'1,j2] in Indices G and
A89: f/.((len(f|k))-'1+2) = G*(i2-'1,j2);
cell(G,i2-'1,j2) misses C by A3,A30,A31,A29,A35,A36,A37
,A38,A42,A87,GOBRD13:28;
then right_cell(f,m,G) misses C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A39,A88,A89,GOBRD13:26;
hence
right_cell(f|(k+1),m,G) misses C by A3,A15,A16,A13,A33,
GOBRD13:31;
cell(G,i2-'1,j2-'1) meets C by A3,A12,A17,A30,A31,A35,A36
,A37,A38,A74,A87,GOBRD13:41;
then left_cell(f,m,G) meets C by A3,A15,A16,A17,A28,A31
,A33,A37,A38,A39,A88,A89,GOBRD13:25;
hence left_cell(f|(k+1),m,G) meets C by A3,A15,A16,A13
,A33,GOBRD13:31;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
m+1 <> len(f|(k+1));
then m+1 < len(f|(k+1)) by A14,XXREAL_0:1;
then
A90: m+1 <= len(f|k) by A16,A17,NAT_1:13;
then consider i1,j1,i2,j2 be Nat such that
A91: [i1,j1] in Indices G and
A92: (f|k)/.m = G*(i1,j1) and
A93: [i2,j2] in Indices G and
A94: (f|k)/.(m+1) = G*(i2,j2) and
A95: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+
1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A9,A13,JORDAN8:3;
A96: right_cell(f|k,m,G) misses C by A7,A13,A90;
A97: f|(k+1) = (f|k)^<*f/.(k+1)*> by A15,FINSEQ_5:82;
1 <= m+1 by NAT_1:12;
then m+1 in dom(f|k) by A90,FINSEQ_3:25;
then
A98: (f|(k+1))/.(m+1) = G*(i2,j2) by A94,A97,FINSEQ_4:68;
A99: left_cell(f|k,m,G) meets C by A7,A13,A90;
m <= len(f|k) by A90,NAT_1:13;
then m in dom(f|k) by A13,FINSEQ_3:25;
then
A100: (f|(k+1))/.m = G*(i1,j1) by A92,A97,FINSEQ_4:68;
now
per cases by A95;
suppose
A101: i1 = i2 & j1+1 = j2;
then
A102: left_cell(f|k,m,G) = cell(G,i1-'1,j1) by A9,A13,A90,A91,A92
,A93,A94,GOBRD13:21;
right_cell(f|k,m,G) = cell(G,i1,j1) by A9,A13,A90,A91,A92,A93
,A94,A101,GOBRD13:22;
hence
thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A101,A102,
GOBRD13:21,22;
end;
suppose
A103: i1+1 = i2 & j1 = j2;
then
A104: left_cell(f|k,m,G) = cell(G,i1,j1) by A9,A13,A90,A91,A92,A93
,A94,GOBRD13:23;
right_cell(f|k,m,G) = cell(G,i1,j1-'1) by A9,A13,A90,A91,A92
,A93,A94,A103,GOBRD13:24;
hence
thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A103,A104,
GOBRD13:23,24;
end;
suppose
A105: i1 = i2+1 & j1 = j2;
then
A106: left_cell(f|k,m,G) = cell(G,i2,j2-'1) by A9,A13,A90,A91,A92
,A93,A94,GOBRD13:25;
right_cell(f|k,m,G) = cell(G,i2,j2) by A9,A13,A90,A91,A92,A93
,A94,A105,GOBRD13:26;
hence
thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A105,A106,
GOBRD13:25,26;
end;
suppose
A107: i1 = i2 & j1 = j2+1;
then
A108: left_cell(f|k,m,G) = cell(G,i1,j2) by A9,A13,A90,A91,A92,A93
,A94,GOBRD13:27;
right_cell(f|k,m,G) = cell(G,i2-'1,j2) by A9,A13,A90,A91,A92
,A93,A94,A107,GOBRD13:28;
hence
thesis by A8,A13,A14,A91,A93,A96,A99,A100,A98,A107,A108,
GOBRD13:27,28;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A109: P[0]
by CARD_1:27;
for k be Nat holds P[k] from NAT_1:sch 2(A109,A6);
hence thesis by A1;
end;
theorem Th8:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds C misses L~Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
set G = Gauge(C,n);
set f = Span(C,n);
assume not thesis;
then consider c be object such that
A2: c in C and
A3: c in L~f by XBOOLE_0:3;
L~f = union { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f
} by TOPREAL1:def 4;
then consider Z be set such that
A4: c in Z and
A5: Z in { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f }
by A3,TARSKI:def 4;
consider i be Nat such that
A6: Z = LSeg(f,i) and
A7: 1 <= i and
A8: i+1 <= len f by A5;
f is_sequence_on G by A1,JORDAN13:def 1;
then LSeg(f,i) = left_cell(f,i,G) /\ right_cell(f,i,G) by A7,A8,GOBRD13:29;
then
A9: c in right_cell(f,i,G) by A4,A6,XBOOLE_0:def 4;
right_cell(f,i,G) misses C by A1,A7,A8,Th7;
hence contradiction by A2,A9,XBOOLE_0:3;
end;
registration
let C be Simple_closed_curve;
let n be Nat;
cluster Cl RightComp Span(C,n) -> compact;
coherence by GOBRD14:32;
end;
theorem Th9:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds C meets LeftComp Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
then
A2: Span(C,n) is_sequence_on Gauge(C,n) by JORDAN13:def 1;
A3: 1+1 <= len Span(C,n) by GOBOARD7:34,XXREAL_0:2;
then left_cell(Span(C,n),1,Gauge(C,n)) meets C by A1,Th7;
then left_cell(Span(C,n),1,Gauge(C,n))\L~Span(C,n) meets C by A1,Th8,
XBOOLE_1:84;
hence thesis by A3,A2,JORDAN9:27,XBOOLE_1:63;
end;
theorem Th10:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds C misses RightComp Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
set f = Span(C,n);
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then
A1: ex L be Subset of (TOP-REAL 2)|(L~f)` st L = RightComp f & L
is a_component by CONNSP_1:def 6;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then
A2: ex R be Subset of (TOP-REAL 2)|(L~f)` st R = LeftComp f & R
is a_component by CONNSP_1:def 6;
assume
A3: n is_sufficiently_large_for C;
then
A4: C misses L~f by Th8;
C c= the carrier of (TOP-REAL 2)|(L~f)`
proof
let c be object;
assume
A5: c in C;
then not c in L~f by A4,XBOOLE_0:3;
then c in (L~f)` by A5,SUBSET_1:29;
hence thesis by PRE_TOPC:8;
end;
then reconsider C1 = C as Subset of (TOP-REAL 2)|(L~f)`;
assume
A6: C meets RightComp f;
A7: C1 is connected by CONNSP_1:23;
C meets LeftComp f by A3,Th9;
hence contradiction by A6,A1,A2,A7,JORDAN2C:92,SPRECT_4:6;
end;
theorem Th11:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds C c= LeftComp Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
let c be object;
set f = Span(C,n);
assume
A2: c in C;
C misses L~f by A1,Th8;
then
A3: not c in L~f by A2,XBOOLE_0:3;
C misses RightComp f by A1,Th10;
then not c in RightComp f by A2,XBOOLE_0:3;
hence thesis by A2,A3,GOBRD14:18;
end;
theorem Th12:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds C c= UBD L~Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume n is_sufficiently_large_for C;
then
A1: C c= LeftComp Span(C,n) by Th11;
LeftComp Span(C,n) c= UBD L~Span(C,n) by GOBRD14:34,JORDAN2C:23;
hence thesis by A1;
end;
theorem Th13:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds BDD L~Span(C,n) c= BDD C
proof
let C be Simple_closed_curve;
let n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: not BDD L~Span(C,n) c= BDD C;
set f = Span(C,n);
A3: Cl BDD L~f = Cl RightComp f by GOBRD14:37
.= (RightComp f) \/ L~f by GOBRD14:21;
len f >= 1 by GOBOARD7:34,XXREAL_0:2;
then
A4: 1 in dom f by FINSEQ_3:25;
len f > 4 by GOBOARD7:34;
then f/.1 in L~f by A4,GOBOARD1:1,XXREAL_0:2;
then SpanStart(C,n) in L~f by A1,JORDAN13:def 1;
then
A5: SpanStart(C,n) in Cl BDD L~f by A3,XBOOLE_0:def 3;
SpanStart(C,n) in BDD C by A1,Th6;
then
A6: BDD L~f meets BDD C by A5,PRE_TOPC:def 7;
BDD C misses UBD C by JORDAN2C:24;
then
A7: BDD C,UBD C are_separated by TSEP_1:37;
BDD L~f misses UBD L~f by JORDAN2C:24;
then C misses BDD L~f by A1,Th12,XBOOLE_1:63;
then
A8: BDD L~f c= C` by SUBSET_1:23;
BDD C \/ UBD C = C` by JORDAN2C:27;
then BDD L~f c= UBD C by A2,A8,A7,CONNSP_1:16;
then BDD C meets UBD C by A6,XBOOLE_1:63;
hence contradiction by JORDAN2C:24;
end;
theorem Th14:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds UBD C c= UBD L~Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
let x be object;
A2: BDD C misses UBD C by JORDAN2C:24;
assume
A3: x in UBD C;
then reconsider p = x as Point of TOP-REAL 2;
A4: Cl BDD L~Span(C,n) c= Cl BDD C by A1,Th13,PRE_TOPC:19;
A5: now
assume x in L~Span(C,n);
then p in (RightComp Span(C,n)) \/ L~Span(C,n) by XBOOLE_0:def 3;
then p in Cl RightComp Span(C,n) by GOBRD14:21;
then p in Cl BDD L~Span(C,n) by GOBRD14:37;
hence contradiction by A4,A2,A3,PRE_TOPC:def 7;
end;
BDD L~Span(C,n) c= BDD C by A1,Th13;
then not x in BDD L~Span(C,n) by A2,A3,XBOOLE_0:3;
then not x in RightComp Span(C,n) by GOBRD14:37;
then p in LeftComp Span(C,n) by A5,GOBRD14:17;
hence thesis by GOBRD14:36;
end;
theorem
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds RightComp Span(C,n) c= BDD C
proof
let C be Simple_closed_curve;
let n be Nat;
assume n is_sufficiently_large_for C;
then BDD L~Span(C,n) c= BDD C by Th13;
hence thesis by GOBRD14:37;
end;
theorem Th16:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds UBD C c= LeftComp Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume n is_sufficiently_large_for C;
then UBD C c= UBD L~Span(C,n) by Th14;
hence thesis by GOBRD14:36;
end;
theorem Th17:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds UBD C misses BDD L~Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: UBD C meets BDD L~Span(C,n);
UBD L~Span(C,n) meets BDD L~Span(C,n) by A1,A2,Th14,XBOOLE_1:63;
hence contradiction by JORDAN2C:24;
end;
theorem
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds UBD C misses RightComp Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume n is_sufficiently_large_for C;
then UBD C misses BDD L~Span(C,n) by Th17;
hence thesis by GOBRD14:37;
end;
theorem Th19:
for C be Simple_closed_curve for P be Subset of TOP-REAL 2 for n
be Nat st n is_sufficiently_large_for C holds P
is_outside_component_of C implies P misses L~Span(C,n)
proof
let C be Simple_closed_curve;
let P be Subset of TOP-REAL 2;
let n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: P is_outside_component_of C and
A3: P meets L~Span(C,n);
A4: UBD C c= LeftComp Span(C,n) by A1,Th16;
consider x be object such that
A5: x in P and
A6: x in L~Span(C,n) by A3,XBOOLE_0:3;
P c= UBD C by A2,JORDAN2C:23;
then x in UBD C by A5;
hence contradiction by A6,A4,GOBRD14:17;
end;
theorem Th20:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds UBD C misses L~Span(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
assume UBD C meets L~Span(C,n);
then consider x be object such that
A2: x in UBD C and
A3: x in L~Span(C,n) by XBOOLE_0:3;
UBD C = union {B where B is Subset of TOP-REAL 2: B
is_outside_component_of C} by JORDAN2C:def 5;
then consider Z be set such that
A4: x in Z and
A5: Z in {B where B is Subset of TOP-REAL 2: B is_outside_component_of C
} by A2,TARSKI:def 4;
consider B be Subset of TOP-REAL 2 such that
A6: Z = B and
A7: B is_outside_component_of C by A5;
B misses L~Span(C,n) by A1,A7,Th19;
hence thesis by A3,A4,A6,XBOOLE_0:3;
end;
theorem Th21:
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds L~Span(C,n) c= BDD C
proof
let C be Simple_closed_curve;
let n be Nat;
assume
A1: n is_sufficiently_large_for C;
then C misses L~Span(C,n) by Th8;
then L~Span(C,n) c= C` by SUBSET_1:23;
then
A2: L~Span(C,n) c= BDD C \/ UBD C by JORDAN2C:27;
UBD C misses L~Span(C,n) by A1,Th20;
hence thesis by A2,XBOOLE_1:73;
end;
theorem Th22:
for C be Simple_closed_curve for i,j,k,n be Nat st n
is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices
Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds i > 1
proof
let C be Simple_closed_curve;
let i,j,k,n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len Span(C,n) and
A4: [i,j] in Indices Gauge(C,n) and
A5: Span(C,n)/.k = Gauge(C,n)*(i,j);
A6: len Span(C,n) > 4 by GOBOARD7:34;
SpanStart(C,n) in BDD C by A1,Th6;
then
A7: W-bound C <= W-bound BDD C by JORDAN1C:6;
A8: j <= width Gauge(C,n) by A4,MATRIX_0:32;
k in dom Span(C,n) by A2,A3,FINSEQ_3:25;
then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2;
then
A9: W-bound L~Span(C,n) <= Gauge(C,n)*(i,j)`1 by A5,PSCOMP_1:24;
A10: BDD C c= Cl BDD C by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then
A12: Cl BDD C is compact by TOPREAL6:79;
SpanStart(C,n) in BDD C by A1,Th6;
then
A13: W-bound BDD C = W-bound Cl BDD C by A11,TOPREAL6:85;
L~Span(C,n) c= BDD C by A1,Th21;
then W-bound L~Span(C,n) >= W-bound Cl BDD C by A12,A10,PSCOMP_1:69
,XBOOLE_1:1;
then
A14: W-bound BDD C <= Gauge(C,n)*(i,j)`1 by A13,A9,XXREAL_0:2;
len Gauge(C,n) >= 4 by JORDAN8:10;
then
A15: len Gauge(C,n) >= 2 by XXREAL_0:2;
A16: 1 <= i by A4,MATRIX_0:32;
A17: 1 <= j by A4,MATRIX_0:32;
len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then Gauge(C,n)*(2,j)`1 = W-bound C by A17,A8,JORDAN8:11;
then Gauge(C,n)*(2,j)`1 <= Gauge(C,n)*(i,j)`1 by A7,A14,XXREAL_0:2;
then i >= 1+1 by A16,A17,A8,A15,GOBOARD5:3;
hence thesis by NAT_1:13;
end;
theorem Th23:
for C be Simple_closed_curve for i,j,k,n be Nat st n
is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices
Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds i < len Gauge(C,n)
proof
let C be Simple_closed_curve;
let i,j,k,n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len Span(C,n) and
A4: [i,j] in Indices Gauge(C,n) and
A5: Span(C,n)/.k = Gauge(C,n)*(i,j);
A6: len Span(C,n) > 4 by GOBOARD7:34;
SpanStart(C,n) in BDD C by A1,Th6;
then
A7: E-bound C >= E-bound BDD C by JORDAN1C:7;
A8: 1 <= j by A4,MATRIX_0:32;
k in dom Span(C,n) by A2,A3,FINSEQ_3:25;
then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2;
then
A9: E-bound L~Span(C,n) >= Gauge(C,n)*(i,j)`1 by A5,PSCOMP_1:24;
A10: BDD C c= Cl BDD C by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then
A12: Cl BDD C is compact by TOPREAL6:79;
SpanStart(C,n) in BDD C by A1,Th6;
then
A13: E-bound BDD C = E-bound Cl BDD C by A11,TOPREAL6:86;
L~Span(C,n) c= BDD C by A1,Th21;
then E-bound L~Span(C,n) <= E-bound Cl BDD C by A12,A10,PSCOMP_1:67
,XBOOLE_1:1;
then
A14: E-bound BDD C >= Gauge(C,n)*(i,j)`1 by A13,A9,XXREAL_0:2;
A15: len Gauge(C,n) >= 4 by JORDAN8:10;
then len Gauge(C,n) >= 1+1 by XXREAL_0:2;
then
A16: len Gauge(C,n)-1 >= 1 by XREAL_1:19;
A17: len Gauge(C,n)-'1 >= 1 by A16,XREAL_0:def 2;
A18: j <= width Gauge(C,n) by A4,MATRIX_0:32;
len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then Gauge(C,n)*(len Gauge(C,n)-'1,j)`1 = E-bound C by A8,A18,JORDAN8:12;
then
A19: Gauge(C,n)*(len Gauge(C,n)-'1,j)`1 >= Gauge(C,n)*(i,j)`1 by A7,A14,
XXREAL_0:2;
i <= len Gauge(C,n) by A4,MATRIX_0:32;
then i <= len Gauge(C,n)-'1 by A8,A18,A17,A19,GOBOARD5:3;
then i < len Gauge(C,n)-'1+1 by NAT_1:13;
hence thesis by A15,XREAL_1:235,XXREAL_0:2;
end;
theorem Th24:
for C be Simple_closed_curve for i,j,k,n be Nat st n
is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices
Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds j > 1
proof
let C be Simple_closed_curve;
let i,j,k,n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len Span(C,n) and
A4: [i,j] in Indices Gauge(C,n) and
A5: Span(C,n)/.k = Gauge(C,n)*(i,j);
A6: len Span(C,n) > 4 by GOBOARD7:34;
SpanStart(C,n) in BDD C by A1,Th6;
then
A7: S-bound C <= S-bound BDD C by JORDAN1C:8;
A8: i <= len Gauge(C,n) by A4,MATRIX_0:32;
k in dom Span(C,n) by A2,A3,FINSEQ_3:25;
then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2;
then
A9: S-bound L~Span(C,n) <= Gauge(C,n)*(i,j)`2 by A5,PSCOMP_1:24;
A10: BDD C c= Cl BDD C by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then
A12: Cl BDD C is compact by TOPREAL6:79;
SpanStart(C,n) in BDD C by A1,Th6;
then
A13: S-bound BDD C = S-bound Cl BDD C by A11,TOPREAL6:88;
L~Span(C,n) c= BDD C by A1,Th21;
then S-bound L~Span(C,n) >= S-bound Cl BDD C by A12,A10,PSCOMP_1:68
,XBOOLE_1:1;
then
A14: S-bound BDD C <= Gauge(C,n)*(i,j)`2 by A13,A9,XXREAL_0:2;
len Gauge(C,n) >= 4 by JORDAN8:10;
then
A15: len Gauge(C,n) >= 2 by XXREAL_0:2;
A16: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A17: 1 <= i by A4,MATRIX_0:32;
then Gauge(C,n)*(i,2)`2 = S-bound C by A8,JORDAN8:13;
then
A18: Gauge(C,n)*(i,2)`2 <= Gauge(C,n)*(i,j)`2 by A7,A14,XXREAL_0:2;
1 <= j by A4,MATRIX_0:32;
then j >= 1+1 by A17,A8,A16,A15,A18,GOBOARD5:4;
hence thesis by NAT_1:13;
end;
theorem Th25:
for C be Simple_closed_curve for i,j,k,n be Nat st n
is_sufficiently_large_for C & 1 <= k & k <= len Span(C,n) & [i,j] in Indices
Gauge(C,n) & Span(C,n)/.k = Gauge(C,n)*(i,j) holds j < width Gauge(C,n)
proof
let C be Simple_closed_curve;
let i,j,k,n be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len Span(C,n) and
A4: [i,j] in Indices Gauge(C,n) and
A5: Span(C,n)/.k = Gauge(C,n)*(i,j);
A6: len Span(C,n) > 4 by GOBOARD7:34;
k in dom Span(C,n) by A2,A3,FINSEQ_3:25;
then Span(C,n)/.k in L~Span(C,n) by A6,GOBOARD1:1,XXREAL_0:2;
then
A7: N-bound L~Span(C,n) >= Gauge(C,n)*(i,j)`2 by A5,PSCOMP_1:24;
A8: BDD C c= Cl BDD C by PRE_TOPC:18;
A9: BDD C is bounded by JORDAN2C:106;
then
A10: Cl BDD C is compact by TOPREAL6:79;
SpanStart(C,n) in BDD C by A1,Th6;
then
A11: N-bound BDD C = N-bound Cl BDD C by A9,TOPREAL6:87;
L~Span(C,n) c= BDD C by A1,Th21;
then N-bound L~Span(C,n) <= N-bound Cl BDD C by A10,A8,PSCOMP_1:66,XBOOLE_1:1
;
then
A12: N-bound BDD C >= Gauge(C,n)*(i,j)`2 by A11,A7,XXREAL_0:2;
A13: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A14: len Gauge(C,n) >= 4 by JORDAN8:10;
then len Gauge(C,n) >= 1+1 by XXREAL_0:2;
then
A15: len Gauge(C,n)-1 >= 1 by XREAL_1:19;
SpanStart(C,n) in BDD C by A1,Th6;
then
A16: N-bound C >= N-bound BDD C by JORDAN1C:9;
A17: i <= len Gauge(C,n) by A4,MATRIX_0:32;
A18: 1 <= i by A4,MATRIX_0:32;
then Gauge(C,n)*(i,len Gauge(C,n)-'1)`2 = N-bound C by A17,JORDAN8:14;
then
A19: Gauge(C,n)*(i,len Gauge(C,n)-'1)`2 >= Gauge(C,n)*(i,j)`2 by A16,A12,
XXREAL_0:2;
A20: len Gauge(C,n)-'1 >= 1 by A15,XREAL_0:def 2;
j <= width Gauge(C,n) by A4,MATRIX_0:32;
then j <= len Gauge(C,n)-'1 by A18,A17,A20,A19,GOBOARD5:4;
then j < len Gauge(C,n)-'1+1 by NAT_1:13;
hence thesis by A13,A14,XREAL_1:235,XXREAL_0:2;
end;
theorem
for C be Simple_closed_curve for n be Nat st n
is_sufficiently_large_for C holds Y-SpanStart(C,n) < width Gauge(C,n)
proof
let C be Simple_closed_curve;
let n be Nat;
A1: len Span(C,n) > 1 by GOBOARD7:34,XXREAL_0:2;
assume
A2: n is_sufficiently_large_for C;
then
A3: Span(C,n)/.1 = Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) by
JORDAN13:def 1;
[X-SpanStart(C,n),Y-SpanStart(C,n)] in Indices Gauge(C,n) by A2,JORDAN11:8;
hence thesis by A2,A1,A3,Th25;
end;
theorem Th27:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n,m be Nat st m >= n & n >= 1 holds X-SpanStart(C,m) = 2|^(m-'
n)*(X-SpanStart(C,n)-2)+2
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n,m be Nat;
A1: X-SpanStart(C,n) = 2|^(n-'1) + 2 by JORDAN1H:def 2;
assume
A2: m >=n;
assume
A3: n >= 1;
then (m-'n)+(n-'1) = (m-'n)+(n-1) by XREAL_1:233
.= (m-'n)+ n-1
.= m-1 by A2,XREAL_1:235
.= m-'1 by A2,A3,XREAL_1:233,XXREAL_0:2;
then 2|^(m-'1) = 2|^(m-'n)*(X-SpanStart(C,n)-2) by A1,NEWTON:8;
hence thesis by JORDAN1H:def 2;
end;
theorem Th28:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n,m be Nat st n <= m & n is_sufficiently_large_for C holds m
is_sufficiently_large_for C
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n,m be Nat;
assume that
A1: n <= m and
A2: n is_sufficiently_large_for C;
consider j be Nat such that
A3: j < width Gauge(C,n) and
A4: cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C by A2,JORDAN1H:def 3;
set iin = X-SpanStart(C,n);
set iim = X-SpanStart(C,m);
n >= 1 by A2,JORDAN1H:51;
then
A5: iim = 2|^(m-'n)*(iin-2)+2 by A1,Th27;
A6: j > 1
proof
A7: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:50;
assume
A8: j <= 1;
per cases by A8,NAT_1:25;
suppose
A9: j = 0;
width Gauge(C,n) >= 0;
then
A10: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A7,JORDAN1A:24;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A7,JORDAN1A:49;
hence contradiction by A4,A9,A10,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
A11: j = 1;
set i1 = X-SpanStart(C,n);
A12: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,n) by JORDAN1H:49;
then
A13: i1-'1 < len Gauge(C,n) by A12,XXREAL_0:2;
BDD C c= C` by JORDAN2C:25;
then
A14: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A4,A11;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A15: UBD C is_a_component_of C` by JORDAN2C:def 3;
width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A16: 0+1 <= width Gauge(C,n) by NAT_1:14;
then
A17: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A7,JORDAN1A:24;
A18: 1 <= i1-'1 by JORDAN1H:50;
0 < width Gauge(C,n) by A16;
then
cell(Gauge(C,n),i1-'1,0)/\cell(Gauge(C,n),i1-'1,0+1) = LSeg(Gauge(C
,n)*(i1-'1,0+1),Gauge(C,n)*(i1-'1+1,0+1)) by A13,A18,GOBOARD5:26;
then
A19: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0+1) by
XBOOLE_0:def 7;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A7,JORDAN1A:49;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A16,A13,A19,A15
,A14,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A4,A11,A17,JORDAN2C:24,XBOOLE_1:68;
end;
end;
then 2|^(m-'n)*(j-2)+2 > 1 by A1,A3,JORDAN1A:32;
then reconsider j1 = 2|^(m-'n)*(j-2)+2 as Element of NAT by INT_1:3;
iin > 2 by JORDAN1H:49;
then
A20: iin >= 2+1 by NAT_1:13;
A21: j+1 < width Gauge(C,n)
proof
assume j+1 >= width Gauge(C,n);
then
A22: j+1 > width Gauge(C,n) or j+1 = width Gauge(C,n) by XXREAL_0:1;
A23: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by JORDAN1H:50;
per cases by A3,A22,NAT_1:13;
suppose
A24: j = width Gauge(C,n);
A25: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A23,
JORDAN1A:50;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) is non empty by A23,A24,
JORDAN1A:24;
hence contradiction by A4,A24,A25,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
j + 1 = width Gauge(C,n);
then
A26: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= BDD C
by A4,NAT_D:34;
BDD C c= C` by JORDAN2C:25;
then
A27: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= C` by A26;
A28: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A23,
JORDAN1A:50;
set i1 = X-SpanStart(C,n);
A29: i1-'1 <= i1 by NAT_D:44;
i1 < len Gauge(C,n) by JORDAN1H:49;
then
A30: i1-'1 < len Gauge(C,n) by A29,XXREAL_0:2;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A31: UBD C is_a_component_of C` by JORDAN2C:def 3;
width Gauge(C,n)-'1 <= width Gauge(C,n) by NAT_D:44;
then
A32: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is non
empty by A23,JORDAN1A:24;
A33: width Gauge(C,n)-1 < width Gauge(C,n) by XREAL_1:146;
A34: 1 <= i1-'1 by JORDAN1H:50;
A35: width Gauge(C,n)<>0 by MATRIX_0:def 10;
then width Gauge(C,n)-'1+1 = width Gauge(C,n) by NAT_1:14,XREAL_1:235;
then cell(Gauge(C,n),i1-'1,width Gauge(C,n))/\ cell(Gauge(C,n),i1-'1,
width Gauge(C,n)-'1) = LSeg(Gauge(C,n)*(i1-'1,width Gauge(C,n)), Gauge(C,n)*(i1
-'1+1,width Gauge(C,n))) by A30,A33,A34,GOBOARD5:26;
then
A36: cell(Gauge(C,n),i1-'1,width Gauge(C,n)) meets cell(Gauge(C,n),i1-'1
,width Gauge(C,n)-'1) by XBOOLE_0:def 7;
width Gauge(C,n)-'1 < width Gauge(C,n) by A35,A33,NAT_1:14,XREAL_1:233;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= UBD C
by A28,A30,A36,A31,A27,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A26,A32,JORDAN2C:24,XBOOLE_1:68;
end;
end;
iin < len Gauge(C,n) by JORDAN1H:49;
then cell(Gauge(C,m),iim-'1,j1) c= cell(Gauge(C,n),iin-'1,j) by A1,A5,A20,A6
,A21,JORDAN1A:48;
then
A37: cell(Gauge(C,m),X-SpanStart(C,m)-'1,j1) c= BDD C by A4;
j1 < width Gauge(C,m) by A1,A3,A6,JORDAN1A:32;
hence thesis by A37,JORDAN1H:def 3;
end;
theorem Th29:
for G be Go-board for f be FinSequence of TOP-REAL 2 for i,j be
Nat holds f is_sequence_on G & f is special & i <= len G & j <=
width G implies cell(G,i,j)\L~f is connected
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
let i,j be Nat;
assume that
A1: f is_sequence_on G and
A2: f is special and
A3: i<=len G and
A4: j<=width G;
Int cell(G,i,j) misses L~f by A1,A2,A3,A4,JORDAN9:14;
then
A5: Int cell(G,i,j) c= (L~f)` by SUBSET_1:23;
cell(G,i,j)\L~f c= cell(G,i,j) by XBOOLE_1:36;
then
A6: cell(G,i,j)\L~f c= Cl Int cell(G,i,j) by A3,A4,GOBRD11:35;
A7: Int cell(G,i,j) c= cell(G,i,j) by TOPS_1:16;
A8: Int cell(G,i,j) is convex by A3,A4,GOBOARD9:17;
cell(G,i,j)\L~f = cell(G,i,j) /\ (L~f)` by SUBSET_1:13;
then Int cell(G,i,j) c= cell(G,i,j)\L~f by A5,A7,XBOOLE_1:19;
hence thesis by A6,A8,CONNSP_1:18;
end;
theorem Th30:
for C be Simple_closed_curve for n,k be Nat st n
is_sufficiently_large_for C & Y-SpanStart(C,n) <= k & k <= 2|^(n-'ApproxIndex C
)*(Y-InitStart C-'2)+2 holds cell(Gauge(C,n),X-SpanStart(C,n)-'1,k)\L~Span(C,n)
c= BDD L~Span(C,n)
proof
let C be Simple_closed_curve;
let n,k be Nat;
set G = Gauge(C,n);
set f = Span(C,n);
set AI = ApproxIndex C;
set YI = Y-InitStart C;
set XS = X-SpanStart(C,n);
set YS = Y-SpanStart(C,n);
assume that
A1: n is_sufficiently_large_for C and
A2: YS <= k and
A3: k <= 2|^(n-'AI)*(YI-'2)+2;
A4: f is_sequence_on G by A1,JORDAN13:def 1;
reconsider ro = k-YS as Element of NAT by A2,INT_1:5;
A5: ro <= 2|^(n-'AI)*(YI-'2)+2-YS by A3,XREAL_1:9;
A6: k = YS+ro;
defpred P[Nat] means
$1 <= 2|^(n-'AI)*(YI-'2)+2-YS implies cell(G
,XS-'1,YS+$1)\L~f c= BDD L~f;
A7: 1 <= XS-'1 by JORDAN1H:50;
XS > 2 by JORDAN1H:49;
then
A8: XS-'1+1 = XS by XREAL_1:235,XXREAL_0:2;
A9: XS-'1 < len G by JORDAN1H:50;
A10: for t being Nat st P[t] holds P[t+1]
proof
let t be Nat;
assume
A11: t <= 2|^(n-'AI)*(YI-'2)+2-YS implies cell(G,XS-'1,YS+t)\L~f c= BDD L~f;
set Ls = LSeg(G*(XS-'1,YS+(t+1)),G*(XS,YS+(t+1)));
A12: t < t+1 by NAT_1:13;
set p = (1/2)*(G*(XS-'1,YS+(t+1))+G*(XS,YS+(t+1)));
A13: cell(G,XS-'1,YS+(t+1))\L~f c= (L~f)`
proof
let y be object;
assume
A14: y in cell(G,XS-'1,YS+(t+1))\L~f;
then not y in L~f by XBOOLE_0:def 5;
hence thesis by A14,SUBSET_1:29;
end;
A15: p in Ls by RLTOPSP1:69;
A16: YS+t+1 = YS+(t+1);
then
A17: 1 <= YS+(t+1) by NAT_1:11;
A18: YI > 1 by JORDAN11:2;
then YI >= 1+1+0 by NAT_1:13;
then YI-2 >= 0 by XREAL_1:19;
then
A19: YI-'2 = YI-2 by XREAL_0:def 2;
assume
A20: t+1 <= 2|^(n-'AI)*(YI-'2)+2-YS;
then
A21: t+1+YS <= 2|^(n-'AI)*(YI-'2)+2 by XREAL_1:19;
assume not cell(G,XS-'1,YS+(t+1))\L~f c= BDD L~f;
then consider x be object such that
A22: x in cell(G,XS-'1,YS+(t+1))\L~f and
A23: not x in BDD L~f;
not x in L~f by A22,XBOOLE_0:def 5;
then x in (L~f)` by A22,SUBSET_1:29;
then x in (BDD L~f) \/ (UBD L~f) by JORDAN2C:27;
then x in UBD L~f by A23,XBOOLE_0:def 3;
then
A24: cell(G,XS-'1,YS+(t+1))\L~f meets UBD L~f by A22,XBOOLE_0:3;
A25: YI < width Gauge(C,AI) by JORDAN11:def 2;
AI <= n by A1,JORDAN11:def 1;
then 2|^(n-'AI)*(YI-2)+2 < width Gauge(C,n) by A18,A25,JORDAN1A:32;
then
A26: YS+t+1 <= width G by A19,A21,XXREAL_0:2;
A27: YS+t+1 <= 2|^(n-'AI)*(YI-'2)+2 by A21;
A28: now
A29: YS <= YS+(t+1) by NAT_1:11;
A30: XS < len G by JORDAN1H:49;
assume p in L~f;
then consider i be Nat such that
A31: 1 <= i and
A32: i+1 <= len f and
A33: p in LSeg(f,i) by SPPOL_2:13;
A34: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A31,A32,TOPREAL1:def 3;
consider i1,j1,i2,j2 be Nat such that
A35: [i1,j1] in Indices G and
A36: f/.i = G*(i1,j1) and
A37: [i2,j2] in Indices G and
A38: f/.(i+1) = G*(i2,j2) and
A39: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 =
j2 or i1 = i2 & j1 = j2+1 by A4,A31,A32,JORDAN8:3;
A40: 1 <= i1 by A35,MATRIX_0:32;
A41: i2 <= len G by A37,MATRIX_0:32;
A42: 1 <= i2 by A37,MATRIX_0:32;
A43: j1 <= width G by A35,MATRIX_0:32;
A44: 1 <= j2 by A37,MATRIX_0:32;
A45: i1 <= len G by A35,MATRIX_0:32;
A46: j2 <= width G by A37,MATRIX_0:32;
A47: 1 <= j1 by A35,MATRIX_0:32;
per cases by A39;
suppose
i1 = i2 & j1+1 = j2;
hence contradiction by A7,A8,A26,A17,A33,A34,A36,A38,A40,A45,A47,A46
,A30,GOBOARD7:27;
end;
suppose
A48: i1+1 = i2 & j1 = j2;
then
A49: YS+(t+1) = j1 by A7,A8,A26,A17,A33,A34,A36,A38,A40,A47,A43,A41,A30,
GOBOARD7:26;
A50: cell(G,XS-'1,YS+(t+1)) c= BDD C by A1,A21,A29,JORDAN11:def 3;
A51: left_cell(f,i,G) = cell(G,i1,j1) by A4,A31,A32,A35,A36,A37,A38,A48,
GOBRD13:23;
XS-'1 = i1 by A7,A8,A26,A17,A33,A34,A36,A38,A40,A47,A43,A41,A30,A48,
GOBOARD7:26;
then cell(G,XS-'1,YS+(t+1)) meets C by A1,A31,A32,A49,A51,Th7;
hence contradiction by A50,JORDAN1A:7,XBOOLE_1:63;
end;
suppose
A52: i1 = i2+1 & j1 = j2;
then
A53: left_cell(f,i,G) = cell(G,i2,j2-'1) by A4,A31,A32,A35,A36,A37,A38,
GOBRD13:25;
A54: YS+(t+1) = j2 by A7,A8,A26,A17,A33,A34,A36,A38,A45,A47,A43,A42,A30,A52,
GOBOARD7:26;
XS-'1 = i2 by A7,A8,A26,A17,A33,A34,A36,A38,A45,A47,A43,A42,A30,A52,
GOBOARD7:26;
then cell(G,XS-'1,YS+(t+1)-'1) meets C by A1,A31,A32,A54,A53,Th7;
then
A55: cell(G,XS-'1,YS+t) meets C by A16,NAT_D:34;
A56: YS <= YS+t by NAT_1:11;
YS+t <= 2|^(n-'AI)*(YI-'2)+2 by A27,NAT_1:13;
then cell(G,XS-'1,YS+t) c= BDD C by A1,A56,JORDAN11:def 3;
hence contradiction by A55,JORDAN1A:7,XBOOLE_1:63;
end;
suppose
i1 = i2 & j1 = j2+1;
hence contradiction by A7,A8,A26,A17,A33,A34,A36,A38,A40,A45,A43,A44
,A30,GOBOARD7:27;
end;
end;
YS+t < width G by A26,NAT_1:13;
then Ls c= cell(G,XS-'1,YS+t) by A7,A9,A8,A16,GOBOARD5:21;
then
A57: p in cell(G,XS-'1,YS+t)\L~f by A28,A15,XBOOLE_0:def 5;
Ls c= cell(G,XS-'1,YS+(t+1)) by A7,A9,A8,A26,A17,GOBOARD5:22;
then
A58: p in cell(G,XS-'1,YS+(t+1))\L~f by A28,A15,XBOOLE_0:def 5;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then UBD L~f is_a_component_of (L~f)` by GOBRD14:36;
then cell(G,XS-'1,YS+(t+1))\L~f c= UBD L~f by A4,A9,A26,A24,A13,Th29,
GOBOARD9:4;
then BDD L~f meets UBD L~f by A11,A20,A12,A57,A58,XBOOLE_0:3,XXREAL_0:2;
hence contradiction by JORDAN2C:24;
end;
A59: P[0]
proof
assume 0 <= 2|^(n-'AI)*(YI-'2)+2-YS;
A60: f/.(1+1) = G*(XS-'1,YS) by A1,JORDAN13:def 1;
A61: [XS,YS] in Indices Gauge(C,n) by A1,JORDAN11:8;
A62: [XS-'1,YS] in Indices Gauge(C,n) by A1,JORDAN11:9;
A63: len f >= 1+1 by GOBOARD7:34,XXREAL_0:2;
then
A64: right_cell(f,1,G)\L~f c= RightComp f by A4,JORDAN9:27;
f/.1 = G*(XS,YS) by A1,JORDAN13:def 1;
then right_cell(f,1,G) = cell(G,XS-'1,YS) by A4,A8,A63,A60,A61,A62,
GOBRD13:26;
hence thesis by A64,GOBRD14:37;
end;
for t be Nat holds P[t] from NAT_1:sch 2(A59,A10);
hence thesis by A6,A5;
end;
theorem Th31:
for C be Subset of TOP-REAL 2 for n,m,i be Nat st m
<= n & 1 < i & i+1 < len Gauge(C,m) holds 2|^(n-'m)*(i-2)+2+1 < len Gauge(C,n)
proof
let C be Subset of TOP-REAL 2;
let n,m,i be Nat;
assume that
A1: m <= n and
A2: 1 < i and
A3: i+1 < len Gauge(C,m);
1+1 <= i by A2,NAT_1:13;
then reconsider i2 = i-2 as Element of NAT by INT_1:5;
A4: 2|^(n-'m) > 0 by NEWTON:83;
len Gauge(C,m) = 2|^m + (2+1) by JORDAN8:def 1
.= 2|^m + 2+1;
then i < 2|^m + 2 by A3,XREAL_1:7;
then i2 < 2|^m by XREAL_1:19;
then 2|^(n-'m)*i2 < 2|^(n-'m)*2|^m by A4,XREAL_1:68;
then 2|^(n-'m)*i2 < 2|^(n-'m+m) by NEWTON:8;
then 2|^(n-'m)*i2 < 2|^n by A1,XREAL_1:235;
then 2|^(n-'m)*(i2)+2 < 2|^n + 2 by XREAL_1:8;
then 2|^(n-'m)*(i-2)+2+1 < 2|^n + 2+1 by XREAL_1:8;
then 2|^(n-'m)*(i-2)+2+1 < 2|^n + (1+2);
hence thesis by JORDAN8:def 1;
end;
theorem Th32:
for C be Simple_closed_curve for n,m be Nat st n
is_sufficiently_large_for C & n <= m holds RightComp Span(C,n) meets RightComp
Span(C,m)
proof
let C be Simple_closed_curve;
let n,m be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m;
set i1 = X-SpanStart(C,m);
set G1 = Gauge(C,m);
set YI = Y-InitStart C;
set AI = ApproxIndex C;
A3: m is_sufficiently_large_for C by A1,A2,Th28;
then
A4: AI <= m by JORDAN11:def 1;
set i = X-SpanStart(C,n);
set G = Gauge(C,n);
A5: 1 <= i1-'1 by JORDAN1H:50;
set j1 = Y-SpanStart(C,m);
set f1 = Span(C,m);
j1 <= 2|^(m-'AI)*(YI-'2)+2 by A3,JORDAN11:5;
then
A6: cell(G1,i1-'1,2|^(m-'AI)*(YI-'2)+2)\L~f1 c= BDD L~f1 by A1,A2,Th28,Th30;
A7: i < len G by JORDAN1H:49;
then i+1 <= len G by NAT_1:13;
then
A8: i <= len G - 1 by XREAL_1:19;
set XSAI = X-SpanStart(C,AI);
set p2 = Gauge(C,AI)*(XSAI,YI);
A9: 1 < XSAI by JORDAN1H:49,XXREAL_0:2;
A10: YI + 1 < width Gauge(C,AI) by JORDAN11:3;
then
A11: YI < width Gauge(C,AI) by NAT_1:13;
set j4 = 2|^(n-'AI)*(YI-'2)+2;
A12: i1 < len G1 by JORDAN1H:49;
set j = Y-SpanStart(C,n);
set f = Span(C,n);
j <= 2|^(n-'AI)*(YI-'2)+2 by A1,JORDAN11:5;
then
A13: cell(G,i-'1,2|^(n-'AI)*(YI-'2)+2)\L~f c= BDD L~f by A1,Th30;
A14: Int cell(G,i-'1,j4) c= cell(G,i-'1,j4) by TOPS_1:16;
A15: 2 < i by JORDAN1H:49;
then
A16: i-'1+1 = i by XREAL_1:235,XXREAL_0:2;
then
A17: i-'1 >= 1+1 by A15,NAT_1:13;
set j3 = 2|^(m-'AI)*(YI-'2)+2;
A18: i < len G by JORDAN1H:49;
A19: YI > 1 by JORDAN11:2;
then YI >= 1+1+0 by NAT_1:13;
then
A20: YI-2 >= 0 by XREAL_1:19;
then
A21: 2|^(n-'AI)*(YI-'2)+2 = 2|^(n-'AI)*(YI-2)+2 by XREAL_0:def 2;
A22: 2|^(m-'AI)*(YI-'2)+2 = 2|^(m-'AI)*(YI-2)+2 by A20,XREAL_0:def 2;
then
A23: 1 < 2|^(m-'AI)*(YI-'2)+2 by A4,A11,A19,JORDAN1A:32;
set p3 = 1/2*(G1*(i1-'1,j3)+G1*(i1,j3+1));
A24: i1-'1 < len G1 by JORDAN1H:50;
A25: 2|^(m-'AI)*(YI-'2)+2 < width G1 by A4,A11,A19,A22,JORDAN1A:32;
then
A26: j3+1 <= width G1 by NAT_1:13;
2 < i1 by JORDAN1H:49;
then
A27: i1-'1+1 = i1 by XREAL_1:235,XXREAL_0:2;
then
A28: p3 in Int cell(G1,i1-'1,j3) by A12,A23,A5,A26,GOBOARD6:31;
then
A29: G1*(i1-'1,j3)`2 < p3`2 by A12,A23,A27,A5,A26,Th4;
A30: p3`2 < G1*(i1-'1,j3+1)`2 by A12,A23,A27,A5,A26,A28,Th4;
A31: G1*(i1-'1,j3)`1 < p3`1 by A12,A23,A27,A5,A26,A28,Th4;
A32: 1 < i1 by JORDAN1H:49,XXREAL_0:2;
then
A33: G1*(i1,j3)`2 = G1*(1,j3)`2 by A12,A23,A25,GOBOARD5:1
.= G1*(i1-'1,j3)`2 by A23,A25,A5,A24,GOBOARD5:1;
A34: j3+1 >= 1 by NAT_1:11;
then
A35: G1*(i1,j3+1)`2 = G1*(1,j3+1)`2 by A12,A32,A26,GOBOARD5:1
.= G1*(i1-'1,j3+1)`2 by A5,A24,A26,A34,GOBOARD5:1;
A36: 1 <= i-'1 by JORDAN1H:50;
A37: AI <= n by A1,JORDAN11:def 1;
then
A38: 1 < 2|^(n-'AI)*(YI-'2)+2 by A11,A19,A21,JORDAN1A:32;
YI+1 < len Gauge(C,AI) by A10,JORDAN8:def 1;
then 2|^(n-'AI)*(YI-'2)+2+1 < len G by A37,A21,Th31,JORDAN11:2;
then 2|^(n-'AI)*(YI-'2)+2+1+1 <= len G by NAT_1:13;
then
A39: j4+1 <= len G - 1 by XREAL_1:19;
A40: i-'1 < len G by JORDAN1H:50;
then i-'1+1 <= len G by NAT_1:13;
then
A41: i-'1 <= len G - 1 by XREAL_1:19;
A42: 2|^(n-'AI)*(YI-'2)+2 < width G by A37,A11,A19,A21,JORDAN1A:32;
then
A43: j4+1 <= width G by NAT_1:13;
j4 < len G by A42,JORDAN8:def 1;
then j4+1 <= len G by NAT_1:13;
then
A44: j4 <= len G - 1 by XREAL_1:19;
A45: XSAI < len Gauge(C,AI) by JORDAN1H:49;
i1 = 2|^(m-'AI)*(XSAI-2)+2 by A1,A2,Th28,JORDAN11:4;
then
A46: p2 = G1*(i1,2|^(m-'AI)*(YI-'2)+2) by A4,A9,A45,A11,A19,A22,JORDAN1A:33;
A47: i = 2|^(n-'AI)*(XSAI-2)+2 by A1,JORDAN11:4;
then
A48: p2 = G*(i,2|^(n-'AI)*(YI-'2)+2) by A37,A9,A45,A11,A19,A21,JORDAN1A:33;
A49: 1 < i by JORDAN1H:49,XXREAL_0:2;
then G*(i,j4)`2 = G*(1,j4)`2 by A18,A38,A42,GOBOARD5:1
.= G*(i-'1,j4)`2 by A38,A42,A36,A40,GOBOARD5:1;
then
A50: G*(i-'1,j4)`2 < p3`2 by A47,A37,A9,A45,A11,A19,A21,A46,A29,A33,JORDAN1A:33
;
p3`1 < G1*(i1,j3)`1 by A12,A23,A27,A5,A26,A28,Th4;
then
A51: p3`1 < G*(i,j4)`1 by A47,A37,A9,A45,A11,A19,A21,A46,JORDAN1A:33;
j4 >= 1+1 by A38,NAT_1:13;
then ex c,d be Nat st 2 <= c & c <= len G1 - 1 & 2 <= d & d
<= len G1 - 1 & [c,d] in Indices G1 & G*(i-'1,j4) = G1*(c,d) & c = 2 + 2|^(m
-'n)*(i-'1-'2) & d = 2 + 2|^(m-'n)*(j4-'2) by A2,A17,A41,A44,GOBRD14:8;
then G*(i-'1,j4) in {G1*(ii,jj) where ii,jj is Nat: [ii,jj] in
Indices G1};
then G*(i-'1,j4) in Values G1 by MATRIX_0:39;
then
G*(i-'1,j4)`1 <= G1*(i1-'1,j3)`1 by A48,A46,A49,A18,A38,A42,A12,A32,A23,A25,
GOBRD13:14;
then
A52: G*(i-'1,j4)`1 < p3`1 by A31,XXREAL_0:2;
j4+1 > 1+1 by A38,XREAL_1:6;
then ex c, d be Nat st 2 <= c & c <= len G1 - 1 & 2 <= d & d
<= len G1 - 1 & [c,d] in Indices G1 & G*(i,j4+1) = G1*(c,d) & c = 2 + 2|^(m
-'n)*(i-'2) & d = 2 + 2|^(m-'n)*(j4+1-'2) by A2,A15,A8,A39,GOBRD14:8;
then G*(i,j4+1) in {G1*(ii,jj) where ii,jj is Nat: [ii,jj] in
Indices G1};
then G*(i,j4+1) in Values G1 by MATRIX_0:39;
then
A53: G1*(i1,j3+1)`2 <= G*(i,j4+1)`2 by A48,A46,A49,A18,A38,A42,A12,A32,A23,A25,
GOBRD13:15;
A54: j4+1 >= 1 by NAT_1:11;
then G*(i,j4+1)`2 = G*(1,j4+1)`2 by A49,A18,A43,GOBOARD5:1
.= G*(i-'1,j4+1)`2 by A36,A40,A43,A54,GOBOARD5:1;
then p3`2 < G*(i-'1,j4+1)`2 by A30,A35,A53,XXREAL_0:2;
then
A55: p3 in Int cell(G,i-'1,j4) by A7,A38,A16,A36,A52,A51,A43,A50,Th4;
f is_sequence_on G by A1,JORDAN13:def 1;
then Int cell(G,i-'1,j4) misses L~f by A42,A40,JORDAN9:14;
then not p3 in L~f by A55,XBOOLE_0:3;
then p3 in cell(G,i-'1,j4)\L~f by A55,A14,XBOOLE_0:def 5;
then p3 in BDD L~f by A13;
then
A56: p3 in RightComp Span(C,n) by GOBRD14:37;
f1 is_sequence_on G1 by A3,JORDAN13:def 1;
then Int cell(G1,i1-'1,j3) misses L~f1 by A25,A24,JORDAN9:14;
then
A57: not p3 in L~f1 by A28,XBOOLE_0:3;
Int cell(G1,i1-'1,j3) c= cell(G1,i1-'1,j3) by TOPS_1:16;
then p3 in cell(G1,i1-'1,j3)\L~f1 by A28,A57,XBOOLE_0:def 5;
then p3 in BDD L~f1 by A6;
then p3 in RightComp Span(C,m) by GOBRD14:37;
hence thesis by A56,XBOOLE_0:3;
end;
theorem Th33:
for G be Go-board for f be FinSequence of TOP-REAL 2 st f
is_sequence_on G & f is special for i,j be Nat st i <= len G & j <=
width G holds Int cell(G,i,j) c= (L~f)`
by JORDAN9:14,SUBSET_1:23;
theorem Th34:
for C be Simple_closed_curve for n,m be Nat st n
is_sufficiently_large_for C & n <= m holds L~Span(C,m) c= Cl LeftComp(Span(C,n)
)
proof
let C be Simple_closed_curve;
let i,j be Nat;
assume that
A1: i is_sufficiently_large_for C and
A2: i <= j and
A3: not L~Span(C,j) c= Cl LeftComp(Span(C,i));
A4: j is_sufficiently_large_for C by A1,A2,Th28;
then
A5: Span(C,j) is_sequence_on Gauge(C,j) by JORDAN13:def 1;
set G = Gauge(C,j);
set f = Span(C,j);
consider p be Point of TOP-REAL 2 such that
A6: p in L~Span(C,j) and
A7: not p in Cl LeftComp(Span(C,i)) by A3;
consider i1 be Nat such that
A8: 1 <= i1 and
A9: i1+1 <= len Span(C,j) and
A10: p in LSeg(Span(C,j),i1) by A6,SPPOL_2:13;
A11: i1 < len Span(C,j) by A9,NAT_1:13;
A12: Span(C,i) is_sequence_on Gauge(C,i) by A1,JORDAN13:def 1;
now
ex i2,j2 be Nat st 1 <= i2 & i2+1 <= len Gauge(C,i) & 1 <=
j2 & j2+1 <= width Gauge(C,i) & left_cell(Span(C,j),i1,G) c= cell(Gauge(C,i),i2
,j2)
proof
A13: 1 <= i1+1 by NAT_1:11;
then
A14: i1+1 in dom f by A9,FINSEQ_3:25;
then consider i5,j5 be Nat such that
A15: [i5,j5] in Indices Gauge(C,j) and
A16: f/.(i1+1) = (Gauge(C,j))*(i5,j5) by A5,GOBOARD1:def 9;
A17: 1 <= i5 by A15,MATRIX_0:32;
A18: j5 <= width Gauge(C,j) by A15,MATRIX_0:32;
A19: i5 <= len Gauge(C,j) by A15,MATRIX_0:32;
A20: 1 <= j5 by A15,MATRIX_0:32;
A21: i1 in dom f by A8,A11,FINSEQ_3:25;
then consider i4,j4 be Nat such that
A22: [i4,j4] in Indices Gauge(C,j) and
A23: f/.i1 = (Gauge(C,j))*(i4,j4) by A5,GOBOARD1:def 9;
A24: 1 <= i4 by A22,MATRIX_0:32;
|.i4-i5.|+|.j4-j5.| = 1 by A5,A21,A22,A23,A14,A15,A16,GOBOARD1:def 9;
then
A25: |.i4-i5.|=1 & j4=j5 or |.j4-j5.|=1 & i4=i5 by SEQM_3:42;
A26: 1 <= j4 by A22,MATRIX_0:32;
left_cell(f,i1,G) = left_cell(f,i1,G);
then
A27: i4 = i5 & j4+1 = j5 & left_cell(f,i1,G) = cell(G,i4-'1,j4) or i4+1
= i5 & j4 = j5 & left_cell(f,i1,G) = cell(G,i4,j4) or i4 = i5+1 & j4 = j5 &
left_cell(f,i1,G) = cell(G,i5,j5-'1) or i4 = i5 & j4 = j5+1 & left_cell(f,i1,G)
= cell(G,i4,j5) by A5,A8,A9,A22,A23,A15,A16,GOBRD13:def 3;
A28: j4 <= width Gauge(C,j) by A22,MATRIX_0:32;
A29: i4 <= len Gauge(C,j) by A22,MATRIX_0:32;
per cases by A25,SEQM_3:41;
suppose
A30: i4 = i5 & j4+1 = j5;
1 < i4 by A1,A2,A8,A11,A22,A23,Th22,Th28;
then 1+1 <= i4 by NAT_1:13;
then
A31: 1 <= i4-'1 by JORDAN5B:2;
i4-'1+1 = i4 by A24,XREAL_1:235;
hence thesis by A2,A29,A26,A18,A27,A30,A31,JORDAN1H:38;
end;
suppose
A32: i4+1 = i5 & j4 = j5;
j4 < width Gauge(C,j) by A1,A2,A8,A11,A22,A23,Th25,Th28;
then j4+1 <= width Gauge(C,j) by NAT_1:13;
hence thesis by A2,A24,A26,A19,A27,A32,JORDAN1H:38;
end;
suppose
A33: i4 = i5+1 & j4 = j5;
1 < j5 by A1,A2,A9,A13,A15,A16,Th24,Th28;
then 1+1 <= j5 by NAT_1:13;
then
A34: 1 <= j5-'1 by JORDAN5B:2;
j5-'1+1 = j5 by A20,XREAL_1:235;
hence thesis by A2,A29,A17,A18,A27,A33,A34,JORDAN1H:38;
end;
suppose
A35: i4 = i5 & j4 = j5+1;
i4 < len Gauge(C,j) by A1,A2,A8,A11,A22,A23,Th23,Th28;
then i4+1 <= len Gauge(C,j) by NAT_1:13;
hence thesis by A2,A24,A28,A20,A27,A35,JORDAN1H:38;
end;
end;
then consider i2,j2 be Nat such that
1 <= i2 and
A36: i2+1 <= len Gauge(C,i) and
1 <= j2 and
A37: j2+1 <= width Gauge(C,i) and
A38: left_cell(Span(C,j),i1,G) c= cell(Gauge(C,i),i2,j2);
A39: j2 < width Gauge(C,i) by A37,NAT_1:13;
A40: LeftComp Span(C,i) is_a_component_of (L~Span(C,i))` by GOBOARD9:def 1;
A41: Cl RightComp Span(C,i) \/ LeftComp Span(C,i) = L~Span(C,i) \/
RightComp Span(C,i) \/ LeftComp Span(C,i) by GOBRD14:21
.= the carrier of TOP-REAL 2 by GOBRD14:15;
assume not left_cell(Span(C,j),i1,G) c= Cl RightComp Span(C,i);
then not cell(Gauge(C,i),i2,j2) c= Cl RightComp Span(C,i) by A38;
then
A42: cell(Gauge(C,i),i2,j2) meets LeftComp Span(C,i) by A41,XBOOLE_1:73;
A43: i2< len Gauge(C,i) by A36,NAT_1:13;
then cell(Gauge(C,i),i2,j2) = Cl Int cell(Gauge(C,i),i2,j2) by A39,
GOBRD11:35;
then
A44: Int cell(Gauge(C,i),i2,j2) meets LeftComp Span(C,i) by A42,TSEP_1:36;
A45: Int left_cell(Span(C,j),i1,G) c= Int cell(Gauge(C,i),i2,j2) by A38,
TOPS_1:19;
A46: Int cell(Gauge(C,i),i2,j2) is convex
by A43,A39,GOBOARD9:17;
Int cell(Gauge(C,i),i2,j2) c= (L~Span(C,i))` by A12,A43,A39,Th33;
then Int cell(Gauge(C,i),i2,j2) c= LeftComp Span(C,i)
by A44,A40,A46,GOBOARD9:4;
then Int left_cell(Span(C,j),i1,G) c= LeftComp Span(C,i) by A45;
then Cl Int left_cell(Span(C,j),i1,G) c= Cl LeftComp Span(C,i) by
PRE_TOPC:19;
then
A47: left_cell(Span(C,j),i1,G) c= Cl LeftComp Span(C,i) by A5,A8,A9,JORDAN9:11;
LSeg(Span(C,j),i1) c= left_cell(Span(C,j),i1,G) by A5,A8,A9,JORDAN1H:20;
then LSeg(Span(C,j),i1) c= Cl LeftComp Span(C,i) by A47;
hence contradiction by A7,A10;
end;
then
A48: C meets Cl RightComp Span(C,i) by A4,A8,A9,Th7,XBOOLE_1:63;
A49: Cl RightComp Span(C,i) = RightComp Span(C,i) \/ L~Span(C,i) by GOBRD14:21;
C misses L~Span(C,i) by A1,Th8;
then
A50: C meets RightComp Span(C,i) by A48,A49,XBOOLE_1:70;
C meets C;
then
A51: C meets LeftComp Span(C,i) by A1,Th11,XBOOLE_1:63;
reconsider D = (L~Span(C,i))` as Subset of TOP-REAL 2;
D = RightComp Span(C,i) \/ LeftComp Span(C,i) by GOBRD12:10;
then
A52: LeftComp Span(C,i) c= D by XBOOLE_1:7;
C c= LeftComp Span(C,i) by A1,Th11;
then
A53: C c= D by A52;
A54: LeftComp Span(C,i) is_a_component_of D by GOBOARD9:def 1;
RightComp Span(C,i) is_a_component_of D by GOBOARD9:def 2;
hence contradiction by A50,A53,A54,A51,JORDAN9:1,SPRECT_4:6;
end;
theorem Th35:
for C be Simple_closed_curve for n,m be Nat st n
is_sufficiently_large_for C & n <= m holds RightComp(Span(C,n)) c= RightComp(
Span(C,m))
proof
let C be Simple_closed_curve;
let n,m be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m;
A3: L~Span(C,n) misses RightComp(Span(C,n)) by SPRECT_3:25;
A4: RightComp Span(C,n) misses LeftComp Span(C,n) by GOBRD14:14;
Cl LeftComp Span(C,n) = (LeftComp Span(C,n)) \/ L~Span(C,n) by GOBRD14:22;
then Cl LeftComp(Span(C,n)) misses RightComp(Span(C,n)) by A3,A4,XBOOLE_1:70;
then L~Span(C,m) misses RightComp(Span(C,n)) by A1,A2,Th34,XBOOLE_1:63;
then
A5: RightComp(Span(C,n)) c= (L~Span(C,m))` by SUBSET_1:23;
A6: RightComp(Span(C,m)) is_a_component_of (L~Span(C,m))` by GOBOARD9:def 2;
RightComp(Span(C,n)) meets RightComp(Span(C,m)) by A1,A2,Th32;
hence thesis by A6,A5,GOBOARD9:4;
end;
theorem
for C be Simple_closed_curve for n,m be Nat st n
is_sufficiently_large_for C & n <= m holds LeftComp(Span(C,m)) c= LeftComp(Span
(C,n))
proof
let C be Simple_closed_curve;
let n,m be Nat;
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m;
A3: (Cl RightComp(Span(C,n)))` = LeftComp(Span(C,n)) by JORDAN1H:43;
A4: (Cl RightComp(Span(C,m)))` = LeftComp(Span(C,m)) by JORDAN1H:43;
Cl RightComp(Span(C,n)) c= Cl RightComp(Span(C,m)) by A1,A2,Th35,PRE_TOPC:19;
hence thesis by A3,A4,SUBSET_1:12;
end;