:: On the General Position of Special Polygons
:: by Mariusz Giero
::
:: Received May 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, SUBSET_1, REAL_1, FINSEQ_1, RELAT_1, ZFMISC_1, XBOOLE_0,
ARYTM_3, CARD_1, ARYTM_1, ABIAN, EUCLID, XXREAL_0, PARTFUN1, FUNCT_1,
TOPREAL1, GOBOARD5, NAT_1, RLTOPSP1, GRAPH_2, TARSKI, STRUCT_0, PRE_TOPC,
SETFAM_1, FINSET_1, CONNSP_1, GOBOARD9, GOBOARD1, MCART_1, CONVEX1,
TREES_1, GOBOARD2, FINSEQ_5, SPPOL_1, MATRIX_1, TOPS_1, INT_1, JORDAN12;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, INT_1, NAT_1, NAT_D, ABIAN, GRAPH_2,
FINSET_1, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, STRUCT_0, PRE_TOPC,
TOPS_1, CONNSP_1, RLTOPSP1, EUCLID, TOPREAL1, SPPOL_1, GOBOARD1,
GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, XXREAL_0, FINSEQ_6;
constructors SETFAM_1, NAT_D, ABIAN, TOPS_1, CONNSP_1, GOBOARD2, SPPOL_1,
GRAPH_2, GOBOARD9, GOBRD13, XXREAL_2, RELSET_1, CONVEX1, FINSEQ_6;
registrations SUBSET_1, XREAL_0, INT_1, MEMBERED, ABIAN, GOBOARD2, SPPOL_2,
GOBOARD5, GOBOARD9, RELAT_1, ZFMISC_1, EUCLID, FINSET_1, FINSEQ_1,
JORDAN1, RLTOPSP1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, JORDAN1;
equalities XBOOLE_0, GOBOARD5, TOPREAL1, SUBSET_1, ORDINAL1;
expansions XBOOLE_0, GOBOARD5, TOPREAL1, JORDAN1;
theorems SPPOL_1, XBOOLE_0, TOPREAL1, JORDAN4, TARSKI, SPPOL_2, FUNCT_1,
FINSEQ_4, FINSEQ_1, NAT_1, SETFAM_1, FINSET_1, CARD_2, RELAT_1, TOPREAL3,
GOBOARD9, CARD_1, SUBSET_1, GOBRD14, JORDAN1H, GOBRD12, JORDAN9,
XBOOLE_1, GOBOARD5, JORDAN8, GOBRD13, GOBOARD6, EUCLID, GOBOARD7, TOPS_1,
NAT_2, JORDAN1G, SPRECT_3, JORDAN1J, FINSEQ_5, GOBRD11, TOPREAL6,
GOBOARD2, TOPREAL8, GRAPH_2, FINSEQ_3, JORDAN5B, XREAL_1, XXREAL_0,
PARTFUN1, ORDINAL1, MATRIX_0, XREAL_0, NAT_D, ZFMISC_1, RLTOPSP1, SEQ_4,
FINSEQ_6;
schemes FRAENKEL, NAT_1;
begin
reserve i,j,k,n for Nat,
X,Y,a,b,c,x for set,
r,s for Real;
Lm1: for f being FinSequence st dom f is trivial holds len f is trivial
proof
let f be FinSequence;
A1: Seg len f = dom f by FINSEQ_1:def 3;
assume
A2: dom f is trivial;
per cases by A2,ZFMISC_1:131;
suppose
dom f is empty;
then f = {};
hence thesis by CARD_1:27;
end;
suppose
ex x being object st dom f = {x};
hence thesis by A1,CARD_1:49,FINSEQ_3:20;
end;
end;
Lm2: for f be FinSequence st f is trivial holds len f is trivial
proof
let f be FinSequence;
assume f is trivial;
then dom f is trivial;
hence thesis by Lm1;
end;
theorem
1 < i implies 0 < i-'1
proof
assume 1 < i;
then 1-1=0 & 1-'1<i-'1 by NAT_D:56;
hence thesis by XREAL_0:def 2;
end;
theorem Th2:
1 is odd
proof
1=2*0+1;
hence thesis;
end;
theorem Th3:
for f be FinSequence of TOP-REAL n for i st 1 <= i & i + 1 <= len
f holds f/.i in rng f & f/.(i+1) in rng f
proof
let f be FinSequence of TOP-REAL n;
let i;
assume
A1: 1 <= i & i + 1 <= len f;
then
A2: i in dom f by SEQ_4:134;
then f.i in rng f by FUNCT_1:3;
hence f/.i in rng f by A2,PARTFUN1:def 6;
A3: i + 1 in dom f by A1,SEQ_4:134;
then f.(i+1) in rng f by FUNCT_1:3;
hence thesis by A3,PARTFUN1:def 6;
end;
registration
cluster s.n.c. -> s.c.c. for FinSequence of TOP-REAL 2;
coherence;
end;
theorem Th4:
for f,g be FinSequence of TOP-REAL 2 st f ^' g is unfolded s.c.c.
& len g >= 2 holds f is unfolded s.n.c.
proof
let f,g be FinSequence of TOP-REAL 2 such that
A1: f ^' g is unfolded s.c.c. and
A2: len g >= 2;
A3: g <> 0 by A2,CARD_1:27;
A4: now
1 = 2-1;
then len g - 1 >= 1 by A2,XREAL_1:9;
then
A5: len g - 1 > 0 by XXREAL_0:2;
assume not f is s.n.c.;
then consider i,j being Nat such that
A6: i+1 < j and
A7: not LSeg(f,i) misses LSeg(f,j);
A8: now
assume not (1<=j & j+1 <= len f);
then LSeg(f,j) = {} by TOPREAL1:def 3;
hence contradiction by A7;
end;
then j < len f by NAT_1:13;
then
A9: LSeg(f^'g,j) = LSeg(f,j) by TOPREAL8:28;
len (f^'g) + 1 = len f + len g by A3,FINSEQ_6:139;
then len (f^'g) + 1 - 1 = len f + (len g - 1);
then len f < len (f^'g) by A5,XREAL_1:29;
then
A10: j+1 < len (f^'g) by A8,XXREAL_0:2;
now
assume not (1<=i & i+1 <= len f);
then LSeg(f,i) = {} by TOPREAL1:def 3;
hence contradiction by A7;
end;
then i<len f by NAT_1:13;
then LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
hence contradiction by A1,A6,A7,A10,A9;
end;
now
assume not f is unfolded;
then consider i be Nat such that
A11: 1 <= i and
A12: i + 2 <= len f and
A13: LSeg(f,i) /\ LSeg(f,i+1) <> {f/.(i+1)};
A14: 1 <= i+1 by A11,NAT_1:13;
i+1 < i+1+1 by NAT_1:13;
then
A15: i+1 < len f by A12,NAT_1:13;
then
A16: LSeg(f^'g,i+1) = LSeg(f,i+1)by TOPREAL8:28;
A17: len f <= len (f^'g) by TOPREAL8:7;
then i+1 <= len (f^'g) by A15,XXREAL_0:2;
then
A18: i+1 in dom (f^'g) by A14,FINSEQ_3:25;
i in NAT & i < len f by A15,NAT_1:13,ORDINAL1:def 12;
then
A19: LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
i+1 in dom f by A14,A15,FINSEQ_3:25;
then
A20: f/.(i+1) = f.(i+1) by PARTFUN1:def 6
.= (f^'g).(i+1) by A14,A15,FINSEQ_6:140
.= (f^'g)/.(i+1) by A18,PARTFUN1:def 6;
i+2 <= len (f^'g) by A12,A17,XXREAL_0:2;
hence contradiction by A1,A11,A13,A20,A19,A16;
end;
hence thesis by A4;
end;
theorem Th5:
for g1,g2 be FinSequence of TOP-REAL 2 holds L~g1 c= L~(g1^'g2)
proof
let g1,g2 be FinSequence of TOP-REAL 2;
let x be object;
assume x in L~g1;
then consider a such that
A1: x in a & a in { LSeg(g1,i) where i is Nat
: 1 <= i & i+1 <= len g1 } by TARSKI:def 4;
consider j being Nat such that
A2: a = LSeg(g1,j) and
A3: 1 <= j and
A4: j+1 <= len g1 by A1;
j < len g1 by A4,NAT_1:13;
then
A5: a = LSeg(g1^'g2,j) by A2,TOPREAL8:28;
len g1 <= len (g1^'g2) by TOPREAL8:7;
then j+1 <= len (g1^'g2) by A4,XXREAL_0:2;
then a in { LSeg(g1^'g2,i)where i is Nat
: 1 <= i & i+1 <= len (g1^'g2) } by A3,A5;
hence thesis by A1,TARSKI:def 4;
end;
begin
definition
let n;
let f1,f2 be FinSequence of TOP-REAL n;
pred f1 is_in_general_position_wrt f2 means
L~f1 misses rng f2 & for
i st 1<=i & i < len f2 holds L~f1 /\ LSeg(f2,i) is trivial;
end;
definition
let n;
let f1,f2 be FinSequence of TOP-REAL n;
pred f1,f2 are_in_general_position means
f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1;
symmetry;
end;
theorem Th6:
for f1,f2 being FinSequence of TOP-REAL 2
st f1,f2 are_in_general_position
for f being FinSequence of TOP-REAL 2
st f = f2|(Seg k) holds f1,f are_in_general_position
proof
let f1,f2 be FinSequence of TOP-REAL 2;
assume
A1: f1,f2 are_in_general_position;
then
A2: f1 is_in_general_position_wrt f2;
let f be FinSequence of TOP-REAL 2 such that
A3: f = f2|(Seg k);
A4: f = f2|k by A3,FINSEQ_1:def 16;
then
A5: len f <= len f2 by FINSEQ_5:16;
A6: now
let i such that
A7: 1<=i and
A8: i < len f;
i in dom(f2|k) by A4,A7,A8,FINSEQ_3:25;
then
A9: f/.i = f2/.i by A4,FINSEQ_4:70;
A10: i+1<=len f by A8,NAT_1:13;
then
A11: i+1<=len f2 by A5,XXREAL_0:2;
then
A12: i < len f2 by NAT_1:13;
1<=i+1 by A7,NAT_1:13;
then i+1 in dom (f2|k) by A4,A10,FINSEQ_3:25;
then
A13: f/.(i+1) = f2/.(i+1) by A4,FINSEQ_4:70;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A7,A10,TOPREAL1:def 3
.= LSeg(f2,i) by A7,A11,A9,A13,TOPREAL1:def 3;
hence L~f1 /\ LSeg(f,i) is trivial by A2,A7,A12;
end;
A14: f2 is_in_general_position_wrt f1 by A1;
A15: now
let i;
assume 1<=i & i < len f1;
then
A16: L~f2 /\ LSeg(f1,i) is trivial by A14;
L~f /\ LSeg(f1,i) c= L~f2 /\ LSeg(f1,i) by A4,TOPREAL3:20,XBOOLE_1:26;
hence L~f /\ LSeg(f1,i) is trivial by A16;
end;
L~f2 misses rng f1 by A14;
then L~f misses rng f1 by A4,TOPREAL3:20,XBOOLE_1:63;
then
A17: f is_in_general_position_wrt f1 by A15;
L~f1 misses rng f2 by A2;
then rng f misses L~f1 by A3,RELAT_1:70,XBOOLE_1:63;
then f1 is_in_general_position_wrt f by A6;
hence thesis by A17;
end;
theorem Th7:
for f1,f2,g1,g2 be FinSequence of TOP-REAL 2 st f1^'f2,g1^'g2
are_in_general_position holds f1^'f2,g1 are_in_general_position
proof
let f1,f2,g1,g2 be FinSequence of TOP-REAL 2 such that
A1: f1^'f2,g1^'g2 are_in_general_position;
A2: g1^'g2 is_in_general_position_wrt f1^'f2 by A1;
A3: now
let i;
assume 1<=i & i < len (f1^'f2);
then
A4: L~(g1^'g2) /\ LSeg(f1^'f2,i) is trivial by A2;
L~g1 /\ LSeg(f1^'f2,i) c= L~(g1^'g2) /\ LSeg(f1^'f2,i) by Th5,XBOOLE_1:26;
hence L~g1 /\ LSeg(f1^'f2,i) is trivial by A4;
end;
A5: f1^'f2 is_in_general_position_wrt g1^'g2 by A1;
A6: now
let i such that
A7: 1<=i and
A8: i < len g1;
len g1 <= len (g1^'g2) by TOPREAL8:7;
then i < len (g1^'g2) by A8,XXREAL_0:2;
then L~(f1^'f2) /\ LSeg(g1^'g2,i) is trivial by A5,A7;
hence L~(f1^'f2) /\ LSeg(g1,i) is trivial by A8,TOPREAL8:28;
end;
L~(g1^'g2) misses rng (f1^'f2) by A2;
then L~g1 misses rng (f1^'f2) by Th5,XBOOLE_1:63;
then
A9: g1 is_in_general_position_wrt f1^' f2 by A3;
L~(f1^'f2) misses rng (g1^'g2) by A5;
then L~(f1^'f2) misses rng g1 by TOPREAL8:10,XBOOLE_1:63;
then f1^'f2 is_in_general_position_wrt g1 by A6;
hence thesis by A9;
end;
reserve f,g for FinSequence of TOP-REAL 2;
theorem Th8:
for k,f,g st 1<=k & k+1<=len g & f,g are_in_general_position
holds g.k in (L~f)` & g.(k+1) in (L~f)`
proof
let k,f,g such that
A1: 1<=k and
A2: k+1<=len g and
A3: f,g are_in_general_position;
f is_in_general_position_wrt g by A3;
then
A4: L~f misses rng g;
A5: rng g c= the carrier of TOP-REAL 2 by FINSEQ_1:def 4;
k < len g by A2,NAT_1:13;
then k in dom g by A1,FINSEQ_3:25;
then
A6: g.k in rng g by FUNCT_1:3;
now
assume not g.k in (L~f)`;
then g.k in (L~f)`` by A6,A5,XBOOLE_0:def 5;
hence contradiction by A4,A6,XBOOLE_0:3;
end;
hence g.k in (L~f)`;
1<=k+1 by A1,NAT_1:13;
then k+1 in dom g by A2,FINSEQ_3:25;
then
A7: g.(k+1) in rng g by FUNCT_1:3;
now
assume not g.(k+1) in (L~f)`;
then g.(k+1) in (L~f)`` by A5,A7,XBOOLE_0:def 5;
hence contradiction by A4,A7,XBOOLE_0:3;
end;
hence thesis;
end;
theorem Th9:
for f1,f2 be FinSequence of TOP-REAL 2 st f1,f2
are_in_general_position for i,j st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <=
len f2 holds LSeg(f1,i) /\ LSeg(f2,j) is trivial
proof
let f1,f2 be FinSequence of TOP-REAL 2 such that
A1: f1,f2 are_in_general_position;
f1 is_in_general_position_wrt f2 by A1;
then
A2: L~f1 misses rng f2;
let i,j such that
A3: 1 <= i & i + 1 <= len f1 and
A4: 1 <= j & j + 1 <= len f2;
f2 is_in_general_position_wrt f1 by A1;
then
A5: L~f2 misses rng f1;
now
set B1 = LSeg(f1/.i,f1/.(i+1)), B2 = LSeg(f2/.j,f2/.(j+1));
set A1 = LSeg(f1,i), A2 = LSeg(f2,j);
set A = LSeg(f1,i) /\ LSeg(f2,j);
assume LSeg(f1,i) /\ LSeg(f2,j) is non trivial;
then consider a1,a2 being object such that
A6: a1 in A and
A7: a2 in A and
A8: a1 <> a2 by ZFMISC_1:def 10;
A9: a1 in A1 & a2 in A1 by A6,A7,XBOOLE_0:def 4;
A10: a2 in A2 by A7,XBOOLE_0:def 4;
A11: a1 in A2 by A6,XBOOLE_0:def 4;
reconsider a1, a2 as Point of TOP-REAL 2 by A6,A7;
A12: a2 in B2 by A4,A10,TOPREAL1:def 3;
A13: A1 = B1 by A3,TOPREAL1:def 3;
then
A14: a2 in B1 by A7,XBOOLE_0:def 4;
a1 in B2 by A4,A11,TOPREAL1:def 3;
then
A15: a1 in LSeg(f2/.j,a2) \/ LSeg(a2,f2/.(j+1)) by A12,TOPREAL1:5;
f1/.i in B1 by RLTOPSP1:68;
then
A16: LSeg(a2, f1/.i) c= B1 by A14,TOPREAL1:6;
A17: a1 in LSeg(f1/.i,a2) \/ LSeg(a2,f1/.(i+1)) by A9,A13,TOPREAL1:5;
f2/.j in B2 by RLTOPSP1:68;
then
A18: LSeg(a2, f2/.j) c= B2 by A12,TOPREAL1:6;
A19: f2/.j in rng f2 by A4,Th3;
A20: f1/.i in rng f1 by A3,Th3;
f2/.(j+1) in B2 by RLTOPSP1:68;
then
A21: LSeg(a2,f2/.(j+1)) c= B2 by A12,TOPREAL1:6;
f1/.(i+1) in B1 by RLTOPSP1:68;
then
A22: LSeg(a2,f1/.(i+1)) c= B1 by A14,TOPREAL1:6;
A23: f2/.(j+1) in rng f2 by A4,Th3;
A24: f1/.(i+1) in rng f1 by A3,Th3;
per cases by A17,XBOOLE_0:def 3;
suppose
A25: a1 in LSeg(f1/.i,a2);
now
per cases by A15,XBOOLE_0:def 3;
suppose
a1 in LSeg(f2/.j,a2);
then f1/.i in LSeg(a2,f2/.j) or f2/.j in LSeg(a2,f1/.i) by A8,A25,
JORDAN4:41;
then
A26: f1/.i in B2 or f2/.j in B1 by A18,A16;
now
per cases by A3,A4,A26,TOPREAL1:def 3;
suppose
f1/.i in A2;
then f1/.i in L~f2 by SPPOL_2:17;
hence contradiction by A5,A20,XBOOLE_0:3;
end;
suppose
f2/.j in A1;
then f2/.j in L~f1 by SPPOL_2:17;
hence contradiction by A2,A19,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
suppose
a1 in LSeg(a2,f2/.(j+1));
then f1/.i in LSeg(a2,f2/.(j+1)) or f2/.(j+1) in LSeg(a2,f1/.i) by A8
,A25,JORDAN4:41;
then
A27: f1/.i in B2 or f2/.(j+1) in B1 by A16,A21;
now
per cases by A3,A4,A27,TOPREAL1:def 3;
suppose
f1/.i in A2;
then f1/.i in L~f2 by SPPOL_2:17;
hence contradiction by A5,A20,XBOOLE_0:3;
end;
suppose
f2/.(j+1) in A1;
then f2/.(j+1) in L~f1 by SPPOL_2:17;
hence contradiction by A2,A23,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
suppose
A28: a1 in LSeg(a2,f1/.(i+1));
now
per cases by A15,XBOOLE_0:def 3;
suppose
a1 in LSeg(f2/.j,a2);
then f1/.(i+1) in LSeg(a2,f2/.j) or f2/.j in LSeg(a2,f1/.(i+1)) by A8
,A28,JORDAN4:41;
then
A29: f1/.(i+1) in B2 or f2/.j in B1 by A18,A22;
now
per cases by A3,A4,A29,TOPREAL1:def 3;
suppose
f1/.(i+1) in A2;
then f1/.(i+1) in L~f2 by SPPOL_2:17;
hence contradiction by A5,A24,XBOOLE_0:3;
end;
suppose
f2/.j in A1;
then f2/.j in L~f1 by SPPOL_2:17;
hence contradiction by A2,A19,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
suppose
a1 in LSeg(a2,f2/.(j+1));
then
f1/.(i+1) in LSeg(a2,f2/.(j+1)) or f2/.(j+1) in LSeg(a2,f1/.(i+
1)) by A8,A28,JORDAN4:41;
then
A30: f1/.(i+1) in B2 or f2/.(j+1) in B1 by A22,A21;
now
per cases by A3,A4,A30,TOPREAL1:def 3;
suppose
f1/.(i+1) in A2;
then f1/.(i+1) in L~f2 by SPPOL_2:17;
hence contradiction by A5,A24,XBOOLE_0:3;
end;
suppose
f2/.(j+1) in A1;
then f2/.(j+1) in L~f1 by SPPOL_2:17;
hence contradiction by A2,A23,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
theorem Th10:
for f,g holds
INTERSECTION({ LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f }
, { LSeg(g,j) where j is Nat : 1 <= j & j+1 <= len g }) is finite
proof
deffunc F(set,set)=$1 /\ $2;
let f,g;
set AL = { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f };
set BL = { LSeg(g,j) where j is Nat: 1 <= j & j+1 <= len g };
set IN = { F(X,Y) where X is Subset of TOP-REAL 2, Y is Subset of TOP-REAL 2
: X in AL & Y in BL };
A1: BL is finite by SPPOL_1:23;
set C = INTERSECTION(AL,BL);
A2: C c= IN
proof
let a be object;
assume a in C;
then consider X,Y such that
A3: X in AL & Y in BL and
A4: a = X /\ Y by SETFAM_1:def 5;
(ex i st X = LSeg(f,i) & 1 <= i & i+1 <= len f )& ex j st Y = LSeg(g,
j) & 1 <= j & j+1 <= len g by A3;
then reconsider X,Y as Subset of TOP-REAL 2;
X /\ Y in IN by A3;
hence thesis by A4;
end;
A5: AL is finite by SPPOL_1:23;
IN is finite from FRAENKEL:sch 22(A5,A1);
hence thesis by A2;
end;
theorem Th11:
for f,g st f,g are_in_general_position holds L~f /\ L~g is finite
proof
let f,g such that
A1: f,g are_in_general_position;
set BL = { LSeg(g,j) : 1 <= j & j+1 <= len g };
set AL = { LSeg(f,i) : 1 <= i & i+1 <= len f };
A2: now
let Z be set;
assume Z in INTERSECTION(AL,BL);
then consider X,Y be set such that
A3: X in AL & Y in BL and
A4: Z = X /\ Y by SETFAM_1:def 5;
( ex i be Nat st X = LSeg(f,i) & 1 <= i & i+1 <= len f)& ex
j be Nat st Y = LSeg(g,j) & 1 <= j & j+1 <= len g by A3;
hence Z is finite by A1,A4,Th9;
end;
L~f /\ L~g = union INTERSECTION(AL,BL) & INTERSECTION(AL,BL) is finite
by Th10,SETFAM_1:28;
hence thesis by A2,FINSET_1:7;
end;
theorem Th12:
for f,g st f,g are_in_general_position for k holds L~f /\ LSeg(g
,k) is finite
proof
let f,g;
assume f,g are_in_general_position;
then
A1: L~f /\ L~g is finite by Th11;
let k;
L~f /\ L~g /\ LSeg(g,k) = L~f /\ (L~g /\ LSeg(g,k)) by XBOOLE_1:16
.= L~f /\ LSeg(g,k) by TOPREAL3:19,XBOOLE_1:28;
hence thesis by A1;
end;
begin
reserve f for non constant standard special_circular_sequence,
p,p1,p2,q for Point of TOP-REAL 2;
theorem Th13:
for f,p1,p2 st LSeg(p1,p2) misses L~f holds ex C be Subset of
TOP-REAL 2 st C is_a_component_of (L~f)` & p1 in C & p2 in C
proof
let f,p1,p2;
assume
A1: LSeg(p1,p2) misses L~f;
A2: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
A3: p1 in LSeg(p1,p2) by RLTOPSP1:68;
then
A4: not p1 in L~f by A1,XBOOLE_0:3;
A5: p2 in LSeg(p1,p2) by RLTOPSP1:68;
then
A6: not p2 in L~f by A1,XBOOLE_0:3;
A7: not (p2 in RightComp f & p1 in LeftComp f) by A1,A3,A5,JORDAN1J:36;
A8: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
now
per cases by A1,A3,A5,JORDAN1J:36;
suppose
not p1 in RightComp f;
then p1 in LeftComp f & p2 in LeftComp f by A7,A4,A6,GOBRD14:17;
hence thesis by A8;
end;
suppose
not p2 in LeftComp f;
then p2 in RightComp f & p1 in RightComp f by A7,A4,A6,GOBRD14:18;
hence thesis by A2;
end;
end;
hence thesis;
end;
theorem Th14:
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a
in C & b in C)) iff ( a in RightComp f & b in RightComp f or a in LeftComp f &
b in LeftComp f )
by JORDAN1H:24,GOBOARD9:def 1,GOBOARD9:def 2;
theorem Th15:
a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
(C is_a_component_of (L~f)` & a in C & b in C)) iff ( a in LeftComp f & b in
RightComp f or a in RightComp f & b in LeftComp f )
proof
A1: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A2: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
thus a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st (C
is_a_component_of (L~f)` & a in C & b in C)) implies ( a in LeftComp f & b in
RightComp f or a in RightComp f & b in LeftComp f )
proof
assume that
A3: a in (L~f)` and
A4: b in (L~f)` and
A5: not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
a in C & b in C);
A6: a in LeftComp f \/ RightComp f by A3,GOBRD12:10;
A7: b in LeftComp f \/ RightComp f by A4,GOBRD12:10;
per cases by A6,XBOOLE_0:def 3;
suppose
A8: a in LeftComp f;
now
per cases by A7,XBOOLE_0:def 3;
suppose
b in LeftComp f;
hence thesis by A1,A5,A8;
end;
suppose
b in RightComp f;
hence thesis by A8;
end;
end;
hence thesis;
end;
suppose
A9: a in RightComp f;
now
per cases by A7,XBOOLE_0:def 3;
suppose
b in RightComp f;
hence thesis by A2,A5,A9;
end;
suppose
b in LeftComp f;
hence thesis by A9;
end;
end;
hence thesis;
end;
end;
thus ( a in LeftComp f & b in RightComp f or a in RightComp f & b in
LeftComp f ) implies a in (L~f)` & b in (L~f)` & not ex C be Subset of TOP-REAL
2 st (C is_a_component_of (L~f)` & a in C & b in C)
proof
assume
A10: a in LeftComp f & b in RightComp f or a in RightComp f & b in LeftComp f;
thus a in (L~f)` & b in (L~f)`
proof
LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
then
A11: LeftComp f c= (L~f)` by GOBRD12:10;
RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
then
A12: RightComp f c= (L~f)` by GOBRD12:10;
per cases by A10;
suppose
a in LeftComp f & b in RightComp f;
hence thesis by A11,A12;
end;
suppose
a in RightComp f & b in LeftComp f;
hence thesis by A11,A12;
end;
end;
now
given C be Subset of TOP-REAL 2 such that
A13: C is_a_component_of (L~f)` and
A14: a in C and
A15: b in C;
now
per cases by A10;
suppose
A16: a in LeftComp f & b in RightComp f;
now
per cases by A1,A13,GOBOARD9:1;
suppose
C = LeftComp f;
then not LeftComp f misses RightComp f by A15,A16,XBOOLE_0:3;
hence contradiction by GOBRD14:14;
end;
suppose
C misses LeftComp f;
hence contradiction by A14,A16,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
suppose
A17: a in RightComp f & b in LeftComp f;
now
per cases by A1,A13,GOBOARD9:1;
suppose
C = LeftComp f;
then not LeftComp f misses RightComp f by A14,A17,XBOOLE_0:3;
hence contradiction by GOBRD14:14;
end;
suppose
C misses LeftComp f;
hence contradiction by A15,A17,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a
in C & b in C);
end;
end;
theorem Th16:
for f,a,b,c st (ex C be Subset of TOP-REAL 2 st (C
is_a_component_of (L~f)` & a in C & b in C)) & (ex C be Subset of TOP-REAL 2 st
(C is_a_component_of (L~f)` & b in C & c in C)) holds ex C be Subset of
TOP-REAL 2 st C is_a_component_of (L~f)` & a in C & c in C
proof
let f be non constant standard special_circular_sequence, a,b,c such that
A1: ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & a in C
& b in C and
A2: ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & b in C
& c in C;
per cases by A1,Th14;
suppose
A3: a in RightComp f & b in RightComp f;
now
per cases by A2,Th14;
suppose
A4: b in RightComp f & c in RightComp f;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
hence thesis by A3,A4;
end;
suppose
b in LeftComp f & c in LeftComp f;
then LeftComp f meets RightComp f by A3,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
suppose
A5: a in LeftComp f & b in LeftComp f;
now
per cases by A2,Th14;
suppose
A6: b in LeftComp f & c in LeftComp f;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
hence thesis by A5,A6;
end;
suppose
b in RightComp f & c in RightComp f;
then LeftComp f meets RightComp f by A5,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
end;
theorem Th17:
for f,a,b,c st a in (L~f)` & b in (L~f)` & c in (L~f)` & (not ex
C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a in C & b in C)) &
(not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & b in C & c
in C)) holds ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & a in
C & c in C
proof
let f,a,b,c such that
A1: a in (L~f)` and
A2: b in (L~f)` and
A3: c in (L~f)` and
A4: not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & a
in C & b in C) and
A5: not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & b
in C & c in C);
A6: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A7: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
per cases by A1,A2,A4,Th15;
suppose
A8: a in LeftComp f & b in RightComp f;
now
per cases by A2,A3,A5,Th15;
suppose
b in LeftComp f & c in RightComp f;
then LeftComp f meets RightComp f by A8,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
b in RightComp f & c in LeftComp f;
hence thesis by A6,A8;
end;
end;
hence thesis;
end;
suppose
A9: a in RightComp f & b in LeftComp f;
now
per cases by A2,A3,A5,Th15;
suppose
b in RightComp f & c in LeftComp f;
then LeftComp f meets RightComp f by A9,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
b in LeftComp f & c in RightComp f;
hence thesis by A7,A9;
end;
end;
hence thesis;
end;
end;
begin
reserve G for Go-board;
Lm3: now
let G,i such that
A1: i <= len G;
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in v_strip(G,i) and
A3: w2 in v_strip(G,i) and
A4: w1`1 <= w2`1;
thus LSeg(w1,w2) c= v_strip(G,i)
proof
let x be object such that
A5: x in LSeg(w1,w2);
reconsider p = x as Point of TOP-REAL 2 by A5;
A6: w1`1 <= p`1 by A4,A5,TOPREAL1:3;
A7: p`1 <= w2`1 by A4,A5,TOPREAL1:3;
A8: p = |[p`1, p`2]| by EUCLID:53;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
i = 0;
then
A9: v_strip(G,i) = { |[r,s]| : r <= G*(1,1)`1 } by GOBRD11:18;
then ex r1,s1 be Real st w2 = |[r1,s1]| & r1 <= G*(1,1)`1 by A3;
then w2`1 <= G*(1,1)`1 by EUCLID:52;
then p`1 <= G*(1,1)`1 by A7,XXREAL_0:2;
hence thesis by A8,A9;
end;
suppose
i = len G;
then
A10: v_strip(G,i) = { |[r,s]| : G*(len G,1)`1 <= r } by GOBRD11:19;
then ex r1,s1 be Real st w1 = |[r1,s1]| & G*(len G,1)`1 <= r1
by A2;
then G*(len G,1)`1 <= w1`1 by EUCLID:52;
then G*(len G,1)`1 <= p`1 by A6,XXREAL_0:2;
hence thesis by A8,A10;
end;
suppose
1 <= i & i < len G;
then
A11: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 } by
GOBRD11:20;
then
ex r2,s2 be Real
st w2 = |[r2,s2]| & G*(i,1)`1 <= r2 & r2 <= G*(i+1,
1)`1 by A3;
then w2`1 <= G*(i+1,1)`1 by EUCLID:52;
then
A12: p`1 <= G*(i+1,1)`1 by A7,XXREAL_0:2;
ex r1,s1 be Real
st w1 = |[r1,s1]| & G*(i,1)`1 <= r1 & r1 <= G*(i+1,
1)`1 by A2,A11;
then G*(i,1)`1 <= w1`1 by EUCLID:52;
then G*(i,1)`1 <= p`1 by A6,XXREAL_0:2;
hence thesis by A8,A11,A12;
end;
end;
end;
theorem Th18:
i <= len G implies v_strip(G,i) is convex
proof
assume
A1: i<= len G;
let w1,w2 be Point of TOP-REAL 2;
set P = v_strip(G,i);
A2: w1`1 <= w2`1 or w2`1 <= w1`1;
assume w1 in P & w2 in P;
hence thesis by A1,A2,Lm3;
end;
Lm4: now
let G,j such that
A1: j <= width G;
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in h_strip(G,j) and
A3: w2 in h_strip(G,j) and
A4: w1`2 <= w2`2;
thus LSeg(w1,w2) c= h_strip(G,j)
proof
let x be object;
assume
A5: x in LSeg(w1,w2);
then reconsider p = x as Point of TOP-REAL 2;
A6: w1`2 <= p`2 by A4,A5,TOPREAL1:4;
A7: p`2 <= w2`2 by A4,A5,TOPREAL1:4;
A8: p = |[p`1, p`2]| by EUCLID:53;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
j = 0;
then
A9: h_strip(G,j) = { |[r,s]| : s <= G*(1,1)`2 } by GOBRD11:21;
then ex r1,s1 be Real st w2 = |[r1,s1]| & s1 <= G*(1,1)`2 by A3;
then w2`2 <= G*(1,1)`2 by EUCLID:52;
then p`2 <= G*(1,1)`2 by A7,XXREAL_0:2;
hence thesis by A8,A9;
end;
suppose
j = width G;
then
A10: h_strip(G,j) = { |[r,s]| : G*(1,width G)`2 <= s } by GOBRD11:22;
then ex r1,s1 be Real st w1 = |[r1,s1]| & G*(1,width G)`2 <= s1
by A2;
then G*(1,width G)`2 <= w1`2 by EUCLID:52;
then G*(1,width G)`2 <= p`2 by A6,XXREAL_0:2;
hence thesis by A8,A10;
end;
suppose
1 <= j & j < width G;
then
A11: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by
GOBRD11:23;
then
ex r2,s2 be Real
st w2 = |[r2,s2]| & G*(1,j)`2 <= s2 & s2 <= G*(1,j+
1)`2 by A3;
then w2`2 <= G*(1,j+1)`2 by EUCLID:52;
then
A12: p`2 <= G*(1,j+1)`2 by A7,XXREAL_0:2;
ex r1,s1 be Real
st w1 = |[r1,s1]| & G*(1,j)`2 <= s1 & s1 <= G*(1,j+
1)`2 by A2,A11;
then G*(1,j)`2 <= w1`2 by EUCLID:52;
then G*(1,j)`2 <= p`2 by A6,XXREAL_0:2;
hence thesis by A8,A11,A12;
end;
end;
end;
theorem Th19:
j <= width G implies h_strip(G,j) is convex
proof
assume
A1: j<= width G;
set P = h_strip(G,j);
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in P & w2 in P;
w1`2 <= w2`2 or w2`2 <= w1`2;
hence thesis by A1,A2,Lm4;
end;
theorem Th20:
i <= len G & j <= width G implies cell(G,i,j) is convex
proof
assume i <= len G & j <= width G;
then v_strip(G,i) is convex & h_strip(G,j) is convex by Th18,Th19;
hence thesis by GOBOARD9:6;
end;
theorem Th21:
for f,k st 1<=k & k+1<=len f holds left_cell(f,k) is convex
proof
let f,k;
assume 1<=k & k+1<=len f;
then ex i,j st i <= len GoB f & j <= width GoB f & cell(GoB f,i,j) =
left_cell(f,k) by GOBOARD9:11;
hence thesis by Th20;
end;
theorem Th22:
for f,k st 1<=k & k+1<=len f holds left_cell(f,k,GoB f) is
convex & right_cell(f,k,GoB f) is convex
proof
let f,k such that
A1: 1<=k and
A2: k+1<=len f;
left_cell(f,k) = left_cell(f,k,GoB f) by A1,A2,JORDAN1H:21;
hence left_cell(f,k,GoB f) is convex by A1,A2,Th21;
k <= len f by A2,NAT_1:13;
then
A3: len f-'k+k = len f by XREAL_1:235;
then
A4: len f-'k >= 1 by A2,XREAL_1:6;
then
A5: right_cell(f,k) = left_cell(Rev f,len f-'k) by A1,A3,GOBOARD9:10;
len f = len Rev f & len f-'k+1 <= len f by A1,A3,FINSEQ_5:def 3,XREAL_1:6;
then left_cell(Rev f,len f-'k) is convex by A4,Th21;
hence thesis by A1,A2,A5,JORDAN1H:23;
end;
begin
theorem Th23:
for p1,p2,f for r be Point of TOP-REAL 2 st r in LSeg(p1,p2) & (
ex x st (L~f) /\ LSeg(p1,p2) = {x}) & not r in L~f holds L~f misses LSeg(p1,r)
or L~f misses LSeg(r,p2)
proof
let p1,p2,f;
let r be Point of TOP-REAL 2 such that
A1: r in LSeg(p1,p2) and
A2: ex x st (L~f) /\ LSeg(p1,p2) = {x} and
A3: not r in L~f;
consider p be set such that
A4: (L~f) /\ LSeg(p1,p2) = {p} by A2;
A5: p in {p} by TARSKI:def 1;
then
A6: p in LSeg(p1,p2) by A4,XBOOLE_0:def 4;
reconsider p as Point of TOP-REAL 2 by A4,A5;
A7: now
A8: LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2) by A6,TOPREAL1:5;
per cases by A1,A8,XBOOLE_0:def 3;
suppose
r in LSeg(p1,p);
hence LSeg(p1,r) /\ LSeg(r,p) = {r} or LSeg(p,r) /\ LSeg(r,p2) = {r} by
TOPREAL1:8;
end;
suppose
r in LSeg(p,p2);
hence LSeg(p1,r) /\ LSeg(r,p) = {r} or LSeg(p,r) /\ LSeg(r,p2) = {r} by
TOPREAL1:8;
end;
end;
p2 in LSeg(p1,p2) by RLTOPSP1:68;
then
A9: LSeg(p2,r) c= LSeg(p1,p2) by A1,TOPREAL1:6;
p1 in LSeg(p1,p2) by RLTOPSP1:68;
then
A10: LSeg(p1,r) c= LSeg(p1,p2) by A1,TOPREAL1:6;
now
assume that
A11: L~f meets LSeg(p1,r) and
A12: L~f meets LSeg(r,p2);
per cases by A7;
suppose
A13: LSeg(p1,r) /\ LSeg(r,p) = {r};
consider x being object such that
A14: x in L~f and
A15: x in LSeg(p1,r) by A11,XBOOLE_0:3;
x in L~f /\ LSeg(p1,p2) by A10,A14,A15,XBOOLE_0:def 4;
then x = p by A4,TARSKI:def 1;
then x in LSeg(r,p) by RLTOPSP1:68;
then x in LSeg(p1,r) /\ LSeg(r,p) by A15,XBOOLE_0:def 4;
hence contradiction by A3,A13,A14,TARSKI:def 1;
end;
suppose
A16: LSeg(p,r) /\ LSeg(r,p2) = {r};
consider x being object such that
A17: x in L~f and
A18: x in LSeg(r,p2) by A12,XBOOLE_0:3;
x in L~f /\ LSeg(p1,p2) by A9,A17,A18,XBOOLE_0:def 4;
then x = p by A4,TARSKI:def 1;
then x in LSeg(p,r) by RLTOPSP1:68;
then x in LSeg(p,r) /\ LSeg(r,p2) by A18,XBOOLE_0:def 4;
hence contradiction by A3,A16,A17,TARSKI:def 1;
end;
end;
hence thesis;
end;
Lm5: now
let p1,p2,f;
let r be Point of TOP-REAL 2 such that
A1: r in LSeg(p1,p2);
assume
A2: ( ex x st (L~f) /\ LSeg(p1,p2) = {x})& not r in L~f;
per cases by A1,A2,Th23;
suppose
L~f misses LSeg(p1,r);
hence
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & r in C
& p1 in C)) or ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r
in C & p2 in C by Th13;
end;
suppose
L~f misses LSeg(r,p2);
hence
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & r in C
& p1 in C)) or ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r
in C & p2 in C by Th13;
end;
end;
theorem Th24:
for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is vertical &
LSeg(r,s) is vertical & LSeg(p,q) meets LSeg(r,s) holds p`1 = r`1
proof
let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is vertical and
A2: LSeg(r,s) is vertical;
assume LSeg(p,q) meets LSeg(r,s);
then LSeg(p,q) /\ LSeg(r,s) <> {};
then consider x being Point of TOP-REAL 2 such that
A3: x in LSeg(p,q) /\ LSeg(r,s) by SUBSET_1:4;
A4: x in LSeg(r,s) by A3,XBOOLE_0:def 4;
x in LSeg(p,q) by A3,XBOOLE_0:def 4;
hence p`1 = x`1 by A1,SPPOL_1:41
.= r`1 by A2,A4,SPPOL_1:41;
end;
theorem Th25:
for p,p1,p2 st not p in LSeg(p1,p2) & p1`2 = p2`2 & p2`2 = p`2
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1)
proof
let p,p1,p2 such that
A1: not p in LSeg(p1,p2) and
A2: p1`2 = p2`2 & p2`2 = p`2;
per cases;
suppose
A3: p1`1 <= p2`1;
now
per cases by A1,A2,GOBOARD7:8;
suppose
p`1<p1`1;
hence thesis by A2,A3,GOBOARD7:8;
end;
suppose
p2`1<p`1;
hence thesis by A2,A3,GOBOARD7:8;
end;
end;
hence thesis;
end;
suppose
A4: p2`1 <= p1`1;
now
per cases by A1,A2,GOBOARD7:8;
suppose
p`1<p2`1;
hence thesis by A2,A4,GOBOARD7:8;
end;
suppose
p1`1<p`1;
hence thesis by A2,A4,GOBOARD7:8;
end;
end;
hence thesis;
end;
end;
theorem Th26:
for p,p1,p2 st not p in LSeg(p1,p2) & p1`1 = p2`1 & p2`1 = p`1
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1)
proof
let p,p1,p2 such that
A1: not p in LSeg(p1,p2) and
A2: p1`1 = p2`1 & p2`1 = p`1;
per cases;
suppose
A3: p1`2 <= p2`2;
now
per cases by A1,A2,GOBOARD7:7;
suppose
p`2<p1`2;
hence thesis by A2,A3,GOBOARD7:7;
end;
suppose
p2`2<p`2;
hence thesis by A2,A3,GOBOARD7:7;
end;
end;
hence thesis;
end;
suppose
A4: p2`2 <= p1`2;
now
per cases by A1,A2,GOBOARD7:7;
suppose
p`2<p2`2;
hence thesis by A2,A4,GOBOARD7:7;
end;
suppose
p1`2<p`2;
hence thesis by A2,A4,GOBOARD7:7;
end;
end;
hence thesis;
end;
end;
theorem Th27:
p <> p1 & p <> p2 & p in LSeg(p1,p2) implies not p1 in LSeg(p,p2 )
proof
assume that
A1: p <> p1 & p <> p2 and
A2: p in LSeg(p1,p2);
A3: LSeg(p1,p) \/ LSeg(p,p2) = LSeg(p1,p2) by A2,TOPREAL1:5;
now
assume p1 in LSeg(p,p2);
then
A4: LSeg(p,p1) \/ LSeg(p1,p2) = LSeg(p,p2) by TOPREAL1:5;
LSeg(p,p1) \/ LSeg(p1,p2) = LSeg(p1,p2) by A3,XBOOLE_1:7,12;
hence contradiction by A1,A4,SPPOL_1:8;
end;
hence thesis;
end;
theorem Th28:
for p,p1,p2,q st not q in LSeg(p1,p2) & p in LSeg(p1,p2) & p <>
p1 & p <> p2 & (p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2) holds p1
in LSeg(q,p) or p2 in LSeg(q,p)
proof
let p,p1,p2,q such that
A1: not q in LSeg(p1,p2) and
A2: p in LSeg(p1,p2) and
A3: p <> p1 & p <> p2 and
A4: p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2;
A5: not p1 in LSeg(p,p2) by A2,A3,Th27;
A6: not p2 in LSeg(p,p1) by A2,A3,Th27;
per cases by A1,A4,Th25,Th26;
suppose
A7: p1 in LSeg(q,p2);
A8: p in LSeg(q,p1) \/ LSeg(p1,p2) by A2,XBOOLE_0:def 3;
LSeg(q,p1) \/ LSeg(p1,p2) = LSeg(q,p2) by A7,TOPREAL1:5;
then LSeg(q,p) \/ LSeg(p,p2) = LSeg(q,p2) by A8,TOPREAL1:5;
hence thesis by A5,A7,XBOOLE_0:def 3;
end;
suppose
A9: p2 in LSeg(q,p1);
A10: p in LSeg(q,p2) \/ LSeg(p1,p2) by A2,XBOOLE_0:def 3;
LSeg(q,p2) \/ LSeg(p1,p2) = LSeg(q,p1) by A9,TOPREAL1:5;
then LSeg(q,p) \/ LSeg(p,p1) = LSeg(q,p1) by A10,TOPREAL1:5;
hence thesis by A6,A9,XBOOLE_0:def 3;
end;
end;
theorem Th29:
for p1,p2,p3,p4,p be Point of TOP-REAL 2 st (p1`1 = p2`1 & p3`1
= p4`1 or p1`2 = p2`2 & p3`2 = p4`2) & LSeg(p1,p2) /\ LSeg(p3,p4) = {p} holds p
=p1 or p=p2 or p=p3
proof
let p1,p2,p3,p4,p be Point of TOP-REAL 2 such that
A1: p1`1 = p2`1 & p3`1 = p4`1 or p1`2 = p2`2 & p3`2 = p4`2 and
A2: LSeg(p1,p2) /\ LSeg(p3,p4) = {p};
A3: p in LSeg(p1,p2) /\ LSeg(p3,p4) by A2,TARSKI:def 1;
then p in LSeg(p3,p4) by XBOOLE_0:def 4;
then LSeg(p3,p) \/ LSeg(p,p4) = LSeg(p3,p4) by TOPREAL1:5;
then
A4: LSeg(p3,p) c= LSeg(p3,p4) by XBOOLE_1:7;
A5: LSeg(p1,p2) meets LSeg(p3,p4) by A3;
A6: now
assume p1`2 = p2`2 & p3`2 = p4`2;
then LSeg(p1,p2) is horizontal & LSeg(p3,p4) is horizontal by SPPOL_1:15;
hence p2`2 = p3`2 by A5,SPRECT_3:9;
end;
A7: now
assume p1`1 = p2`1 & p3`1 = p4`1;
then LSeg(p1,p2) is vertical & LSeg(p3,p4) is vertical by SPPOL_1:16;
hence p2`1 = p3`1 by A5,Th24;
end;
A8: p3 in LSeg(p3,p4) by RLTOPSP1:68;
A9: p2 in LSeg(p1,p2) by RLTOPSP1:68;
A10: p1 in LSeg(p1,p2) by RLTOPSP1:68;
now
A11: p in LSeg(p1,p2) by A3,XBOOLE_0:def 4;
assume that
A12: p<>p1 and
A13: p<>p2 and
A14: p<>p3;
A15: now
assume p3 in LSeg(p1,p2);
then p3 in LSeg(p1,p2) /\ LSeg(p3,p4) by A8,XBOOLE_0:def 4;
hence contradiction by A2,A14,TARSKI:def 1;
end;
now
per cases by A1,A7,A6,A12,A13,A11,A15,Th28;
suppose
p1 in LSeg(p3,p);
then p1 in LSeg(p1,p2) /\ LSeg(p3,p4) by A4,A10,XBOOLE_0:def 4;
hence contradiction by A2,A12,TARSKI:def 1;
end;
suppose
p2 in LSeg(p3,p);
then p2 in LSeg(p1,p2) /\ LSeg(p3,p4) by A4,A9,XBOOLE_0:def 4;
hence contradiction by A2,A13,TARSKI:def 1;
end;
end;
hence contradiction;
end;
hence thesis;
end;
begin
theorem Th30:
for p,p1,p2,f st (L~f) /\ LSeg(p1,p2) = {p} for r be Point of
TOP-REAL 2 st not r in LSeg(p1,p2) & not p1 in L~f & not p2 in L~f & ( p1`1 =
p2`1 & p1`1 = r`1 or p1`2 = p2`2 & p1`2 = r`2 ) & (ex i st (1<=i & i+1<= len f
& (r in right_cell(f,i,GoB f) or r in left_cell(f,i,GoB f)) & p in LSeg(f,i)))
& not r in L~f holds (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f
)` & r in C & p1 in C)) or ex C be Subset of TOP-REAL 2 st C is_a_component_of
(L~f)` & r in C & p2 in C
proof
let p,p1,p2,f;
assume (L~f) /\ LSeg(p1,p2) = {p};
then
A1: p in L~f /\ LSeg(p1,p2) by TARSKI:def 1;
then
A2: p in LSeg(p1,p2) by XBOOLE_0:def 4;
let r be Point of TOP-REAL 2 such that
A3: not r in LSeg(p1,p2) and
A4: not p1 in L~f and
A5: not p2 in L~f and
A6: p1`1 = p2`1 & p1`1 = r`1 or p1`2 = p2`2 & p1`2 = r`2 and
A7: ex i st 1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or r in
left_cell(f,i,GoB f)) & p in LSeg(f,i) and
A8: not r in L~f;
consider i such that
A9: 1<=i & i+1<= len f and
A10: r in right_cell(f,i,GoB f) or r in left_cell(f,i,GoB f) and
A11: p in LSeg(f,i) by A7;
A12: right_cell(f,i,GoB f) is convex by A9,Th22;
A13: f is_sequence_on GoB f by GOBOARD5:def 5;
then
A14: right_cell(f,i,GoB f)\L~f c= RightComp f by A9,JORDAN9:27;
A15: now
assume r in right_cell(f,i,GoB f);
then r in right_cell(f,i,GoB f)\L~f by A8,XBOOLE_0:def 5;
hence r in RightComp f by A14;
end;
A16: LSeg(f,i) c= right_cell(f,i,GoB f) by A13,A9,JORDAN1H:22;
A17: now
assume that
A18: p1 in LSeg(r,p) and
A19: r in right_cell(f,i,GoB f);
LSeg(r,p) c= right_cell(f,i,GoB f) by A11,A16,A12,A19;
then p1 in right_cell(f,i,GoB f)\L~f by A4,A18,XBOOLE_0:def 5;
hence
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r in C &
p1 in C by A14,A15,A19,Th14;
end;
A20: left_cell(f,i,GoB f) is convex by A9,Th22;
A21: left_cell(f,i,GoB f)\L~f c= LeftComp f by A13,A9,JORDAN9:27;
A22: now
assume r in left_cell(f,i,GoB f);
then r in left_cell(f,i,GoB f)\L~f by A8,XBOOLE_0:def 5;
hence r in LeftComp f by A21;
end;
A23: LSeg(f,i) c= left_cell(f,i,GoB f) by A13,A9,JORDAN1H:20;
A24: now
assume that
A25: p1 in LSeg(r,p) and
A26: r in left_cell(f,i,GoB f);
LSeg(r,p) c= left_cell(f,i,GoB f) by A11,A23,A20,A26;
then p1 in left_cell(f,i,GoB f)\L~f by A4,A25,XBOOLE_0:def 5;
hence
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r in C &
p1 in C by A21,A22,A26,Th14;
end;
A27: now
assume that
A28: p2 in LSeg(r,p) and
A29: r in left_cell(f,i,GoB f);
LSeg(r,p) c= left_cell(f,i,GoB f) by A11,A23,A20,A29;
then p2 in left_cell(f,i,GoB f)\L~f by A5,A28,XBOOLE_0:def 5;
hence
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r in C &
p2 in C by A21,A22,A29,Th14;
end;
A30: now
assume that
A31: p2 in LSeg(r,p) and
A32: r in right_cell(f,i,GoB f);
LSeg(r,p) c= right_cell(f,i,GoB f) by A11,A16,A12,A32;
then p2 in right_cell(f,i,GoB f)\L~f by A5,A31,XBOOLE_0:def 5;
hence
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & r in C &
p2 in C by A14,A15,A32,Th14;
end;
A33: p <> p2 & p <> p1 by A4,A5,A1,XBOOLE_0:def 4;
per cases by A3,A6,A33,A2,Th28;
suppose
A34: p1 in LSeg(r,p);
now
per cases by A10;
suppose
r in right_cell(f,i,GoB f);
hence thesis by A17,A34;
end;
suppose
r in left_cell(f,i,GoB f);
hence thesis by A24,A34;
end;
end;
hence thesis;
end;
suppose
A35: p2 in LSeg(r,p);
now
per cases by A10;
suppose
r in right_cell(f,i,GoB f);
hence thesis by A30,A35;
end;
suppose
r in left_cell(f,i,GoB f);
hence thesis by A27,A35;
end;
end;
hence thesis;
end;
end;
theorem Th31:
for f,p1,p2,p st (L~f) /\ LSeg(p1,p2) = {p} for rl,rp be Point
of TOP-REAL 2 st not p1 in L~f & not p2 in L~f & ( p1`1 = p2`1 & p1`1 = rl`1 &
rl`1 = rp`1 or p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2 ) & (ex i st (1<=i & i+1
<= len f & rl in left_cell(f,i,GoB f) & rp in right_cell(f,i,GoB f) & p in LSeg
(f,i))) & not rl in L~f & not rp in L~f holds not ex C be Subset of TOP-REAL 2
st (C is_a_component_of (L~f)` & p1 in C & p2 in C)
proof
let f,p1,p2,p such that
A1: (L~f) /\ LSeg(p1,p2) = {p};
let rl,rp be Point of TOP-REAL 2;
assume that
A2: ( not p1 in L~f)& not p2 in L~f &( p1`1 = p2`1 & p1`1 = rl`1 & rl`1
= rp`1 or p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2) and
A3: ex i st 1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) & rp in
right_cell(f,i,GoB f) & p in LSeg(f,i) and
A4: not rl in L~f and
A5: not rp in L~f;
consider i such that
A6: 1<=i & i+1<= len f and
A7: rl in left_cell(f,i,GoB f) and
A8: rp in right_cell(f,i,GoB f) by A3;
A9: f is_sequence_on GoB f by GOBOARD5:def 5;
then
A10: left_cell(f,i,GoB f)\L~f c= LeftComp f by A6,JORDAN9:27;
A11: right_cell(f,i,GoB f)\L~f c= RightComp f by A9,A6,JORDAN9:27;
rp in right_cell(f,i,GoB f)\L~f by A5,A8,XBOOLE_0:def 5;
then
A12: not rp in LeftComp f by A11,GOBRD14:18;
A13: now
assume
A14: not rp in LSeg(p1,p2);
per cases by A1,A2,A3,A5,A14,Th30;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rp
in C & p1 in C;
hence p1 in RightComp f or p2 in RightComp f by A12,Th14;
end;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rp
in C & p2 in C;
hence p1 in RightComp f or p2 in RightComp f by A12,Th14;
end;
end;
rl in left_cell(f,i,GoB f)\L~f by A4,A7,XBOOLE_0:def 5;
then
A15: not rl in RightComp f by A10,GOBRD14:17;
A16: now
assume
A17: not rl in LSeg(p1,p2);
per cases by A1,A2,A3,A4,A17,Th30;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rl
in C & p1 in C;
hence p1 in LeftComp f or p2 in LeftComp f by A15,Th14;
end;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rl
in C & p2 in C;
hence p1 in LeftComp f or p2 in LeftComp f by A15,Th14;
end;
end;
A18: now
assume that
A19: not rl in LSeg(p1,p2) and
A20: not rp in LSeg(p1,p2);
per cases by A16,A19;
suppose
A21: p1 in LeftComp f;
now
per cases by A13,A20;
suppose
p1 in RightComp f;
then LeftComp f meets RightComp f by A21,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
p2 in RightComp f;
hence thesis by A21,Th15;
end;
end;
hence thesis;
end;
suppose
A22: p2 in LeftComp f;
now
per cases by A13,A20;
suppose
p1 in RightComp f;
hence thesis by A22,Th15;
end;
suppose
p2 in RightComp f;
then LeftComp f meets RightComp f by A22,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
end;
A23: now
assume
A24: rp in LSeg(p1,p2);
per cases by A1,A5,A24,Lm5;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rp
in C & p1 in C;
hence p1 in RightComp f or p2 in RightComp f by A12,Th14;
end;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rp
in C & p2 in C;
hence p1 in RightComp f or p2 in RightComp f by A12,Th14;
end;
end;
A25: now
assume that
A26: not rl in LSeg(p1,p2) and
A27: rp in LSeg(p1,p2);
per cases by A16,A26;
suppose
A28: p1 in LeftComp f;
now
per cases by A23,A27;
suppose
p1 in RightComp f;
then LeftComp f meets RightComp f by A28,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
p2 in RightComp f;
hence thesis by A28,Th15;
end;
end;
hence thesis;
end;
suppose
A29: p2 in LeftComp f;
now
per cases by A23,A27;
suppose
p1 in RightComp f;
hence thesis by A29,Th15;
end;
suppose
p2 in RightComp f;
then LeftComp f meets RightComp f by A29,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
end;
A30: now
assume
A31: rl in LSeg(p1,p2);
per cases by A1,A4,A31,Lm5;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rl
in C & p1 in C;
hence p1 in LeftComp f or p2 in LeftComp f by A15,Th14;
end;
suppose
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & rl
in C & p2 in C;
hence p1 in LeftComp f or p2 in LeftComp f by A15,Th14;
end;
end;
A32: now
assume that
A33: rl in LSeg(p1,p2) and
A34: rp in LSeg(p1,p2);
per cases by A30,A33;
suppose
A35: p1 in LeftComp f;
now
per cases by A23,A34;
suppose
p1 in RightComp f;
then LeftComp f meets RightComp f by A35,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
p2 in RightComp f;
hence thesis by A35,Th15;
end;
end;
hence thesis;
end;
suppose
A36: p2 in LeftComp f;
now
per cases by A23,A34;
suppose
p1 in RightComp f;
hence thesis by A36,Th15;
end;
suppose
p2 in RightComp f;
then LeftComp f meets RightComp f by A36,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
end;
A37: now
assume that
A38: rl in LSeg(p1,p2) and
A39: not rp in LSeg(p1,p2);
per cases by A30,A38;
suppose
A40: p1 in LeftComp f;
now
per cases by A13,A39;
suppose
p1 in RightComp f;
then LeftComp f meets RightComp f by A40,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
suppose
p2 in RightComp f;
hence thesis by A40,Th15;
end;
end;
hence thesis;
end;
suppose
A41: p2 in LeftComp f;
now
per cases by A13,A39;
suppose
p1 in RightComp f;
hence thesis by A41,Th15;
end;
suppose
p2 in RightComp f;
then LeftComp f meets RightComp f by A41,XBOOLE_0:3;
hence thesis by GOBRD14:14;
end;
end;
hence thesis;
end;
end;
per cases;
suppose
A42: rl in LSeg(p1,p2);
now
per cases;
suppose
rp in LSeg(p1,p2);
hence thesis by A32,A42;
end;
suppose
not rp in LSeg(p1,p2);
hence thesis by A37,A42;
end;
end;
hence thesis;
end;
suppose
A43: not rl in LSeg(p1,p2);
now
per cases;
suppose
rp in LSeg(p1,p2);
hence thesis by A25,A43;
end;
suppose
not rp in LSeg(p1,p2);
hence thesis by A18,A43;
end;
end;
hence thesis;
end;
end;
theorem Th32:
for p,f,p1,p2 st L~f /\ LSeg(p1,p2) = {p} & (p1`1=p2`1 or p1`2=
p2`2) & not p1 in L~f & not p2 in L~f & rng f misses LSeg(p1,p2) holds not ex C
be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` & p1 in C & p2 in C)
proof
let p,f,p1,p2 such that
A1: L~f /\ LSeg(p1,p2) = {p} and
A2: p1`1=p2`1 or p1`2=p2`2;
A3: p in {p} by TARSKI:def 1;
then
A4: p in LSeg(p1,p2) by A1,XBOOLE_0:def 4;
A5: p in LSeg(p2,p1) by A1,A3,XBOOLE_0:def 4;
p in L~f by A1,A3,XBOOLE_0:def 4;
then consider LS be set such that
A6: p in LS & LS in { LSeg(f,i) : 1 <= i & i+1 <= len f } by TARSKI:def 4;
set G = GoB f;
assume that
A7: ( not p1 in L~f)& not p2 in L~f and
A8: rng f misses LSeg(p1,p2);
consider k such that
A9: LS = LSeg(f,k) and
A10: 1 <= k and
A11: k+1 <= len f by A6;
A12: f is_sequence_on GoB(f) by GOBOARD5:def 5;
then consider i1,j1,i2,j2 being Nat such that
A13: [i1,j1] in Indices G and
A14: f/.k = G*(i1,j1) and
A15: [i2,j2] in Indices G and
A16: f/.(k+1) = G*(i2,j2) and
A17: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A10,A11,JORDAN8:3;
A18: 1 <= i1 by A13,MATRIX_0:32;
1<=k+1 by A10,NAT_1:13;
then
A19: k+1 in dom f by A11,FINSEQ_3:25;
then f.(k+1) in rng f by FUNCT_1:3;
then f/.(k+1) in rng f by A19,PARTFUN1:def 6;
then
A20: p <> f/.(k+1) by A8,A4,XBOOLE_0:3;
A21: i2 <= len G by A15,MATRIX_0:32;
then
A22: i2=i1+1 implies i1 < len G by NAT_1:13;
then
A23: j1 = width G & i2 = i1+1 implies Int cell(G,i1,j1) = { |[r,s]| : G*(i1,
1)`1 < r & r < G*(i1+1,1)`1 & G*(1,width G)`2 < s } by A18,GOBOARD6:25;
A24: 1<=j1 by A13,MATRIX_0:32;
then
A25: j1 < width G & i2 = i1+1 implies Int cell(G,i1,j1) = { |[r,s]| : G*(i1,
1)`1 < r & r < G*(i1+1,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A18,A22,
GOBOARD6:26;
A26: j2 <= width G by A15,MATRIX_0:32;
then
A27: j2=j1+1 implies j1 < width G by NAT_1:13;
then
A28: i1 = len G & j2 = j1+1 implies Int cell(G,i1,j1) = { |[r,s]| : G*(len
G,1)`1 < r & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A24,GOBOARD6:23;
A29: 1 <= j2 by A15,MATRIX_0:32;
A30: j1 <= width G by A13,MATRIX_0:32;
then
A31: j1=j2+1 implies j2 < width G by NAT_1:13;
then
A32: i2 = len G & j1 = j2+1 implies Int cell(G,i2,j2) = { |[r,s]| : G*(len
G,1)`1 < r & G*(1,j2)`2 < s & s < G*(1,j2+1)`2 } by A29,GOBOARD6:23;
A33: 1 <= i2 by A15,MATRIX_0:32;
then
A34: i2 < len G & j1 = j2+1 implies Int cell(G,i2,j2) = { |[r,s]| : G*(i2,1
)`1 < r & r < G*(i2+1,1)`1 & G*(1,j2)`2 < s & s < G*(1,j2+1)`2 } by A29,A31,
GOBOARD6:26;
A35: i1 <= len G by A13,MATRIX_0:32;
then
A36: i1=i2+1 implies i2 < len G by NAT_1:13;
then
A37: j1 = width G & i1 = i2+1 implies Int cell(G,i2,j1) = { |[r,s]| : G*(i2
,1)`1 < r & r < G*(i2+1,1)`1 & G*(1,width G)`2 < s } by A33,GOBOARD6:25;
k < len f by A11,NAT_1:13;
then
A38: k in dom f by A10,FINSEQ_3:25;
then f.k in rng f by FUNCT_1:3;
then f/.k in rng f by A38,PARTFUN1:def 6;
then
A39: p <> f/.k by A8,A4,XBOOLE_0:3;
A40: j1 -'1 < j1 by A24,JORDAN5B:1;
A41: now
assume 1 < j1 & i2 = i1+1;
then
A42: i1 < len G & 1 <= j1-'1 by A21,NAT_1:13,NAT_D:49;
1 <= i1 & j1-'1 < width G by A13,A30,A40,MATRIX_0:32,XXREAL_0:2;
hence Int cell(G,i1,j1-'1) = { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1
& G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 } by A42,GOBOARD6:26;
end;
A43: j1 < width G & i1 = i2+1 implies Int cell(G,i2,j1) = { |[r,s]| : G*(i2
,1)`1 < r & r < G*(i2+1,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A33,A24
,A36,GOBOARD6:26;
A44: now
assume 1 < j1 & i1 = i2+1;
then
A45: i2 < len G & 1 <= j1-'1 by A35,NAT_1:13,NAT_D:49;
1 <= i2 & j1-'1 < width G by A15,A30,A40,MATRIX_0:32,XXREAL_0:2;
hence Int cell(G,i2,j1-'1) = { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1
& G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 } by A45,GOBOARD6:26;
end;
A46: now
assume that
A47: 1 = j1 and
A48: i1 = i2+1;
Int cell(G,i2,0) = Int cell(G,i2,j1-'1) by A47,NAT_2:8;
hence Int cell(G,i2,j1-'1) = { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1
& s < G*(1,1)`2 } by A33,A36,A48,GOBOARD6:24;
end;
A49: j1 = j2 & i2 = i1+1 implies Int left_cell(f,k,G)= Int cell(G,i1,j1) &
Int right_cell(f,k,G)= Int cell(G,i1,j1-'1) by A12,A10,A11,A13,A14,A15,A16,
GOBRD13:23,24;
A50: p in LSeg(f/.(k+1),f/.k) by A6,A9,A10,A11,TOPREAL1:def 3;
A51: now
assume that
A52: i1 = i2 and
A53: j1 = j2+1;
j2 < j1 by A53,NAT_1:13;
then (f/.(k+1))`2 < (f/.k)`2 by A14,A16,A35,A18,A30,A29,A52,GOBOARD5:4;
then
A54: (f/.(k+1))`2 < p`2 & p`2 < (f/.k)`2 by A39,A50,A20,TOPREAL6:30;
1 <= j2+1 & j2+1<=width G by A13,A53,MATRIX_0:32;
hence
G*(1,j2)`2 < p`2 & p`2 < G*(1,j2+1)`2 by A14,A16,A35,A18,A26,A29,A52,A53
,A54,GOBOARD5:1;
end;
A55: now
assume that
A56: i1 = i2 and
A57: j2 = j1+1;
j1 < j2 by A57,NAT_1:13;
then (f/.k)`2 < (f/.(k+1))`2 by A14,A16,A35,A18,A24,A26,A56,GOBOARD5:4;
then (f/.k)`2 < p`2 & p`2 < (f/.(k+1))`2 by A39,A50,A20,TOPREAL6:30;
hence
G*(1,j1)`2 < p`2 & p`2 < G*(1,j1+1)`2 by A14,A16,A33,A35,A24,A30,A26,A29
,A56,A57,GOBOARD5:1;
end;
A58: now
assume that
A59: 1 = i2 and
A60: j1 = j2+1;
Int cell(G,i2-'1,j2) = Int cell(G,0,j2) by A59,NAT_2:8;
hence
Int cell(G,i2-'1,j2) = { |[r,s]| : r < G*(1,1)`1 & G*(1,j2)`2 < s & s
< G*(1,j2+1)`2 } by A29,A31,A60,GOBOARD6:20;
end;
LSeg(p1,p2) /\ LSeg(f,k) = {p} by A1,A6,A9,TOPREAL3:19,ZFMISC_1:124;
then
A61: LSeg(p1,p2) /\ LSeg(f/.k,f/.(k+1)) = {p} by A10,A11,TOPREAL1:def 3;
A62: i1 < len G & j2 = j1+1 implies Int cell(G,i1,j1) = { |[r,s]| : G*(i1,1
)`1 < r & r < G*(i1+1,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A18,A24
,A27,GOBOARD6:26;
A63: now
assume that
A64: 1 = i1 and
A65: j2 = j1+1;
Int cell(G,i1-'1,j1) = Int cell(G,0,j1) by A64,NAT_2:8;
hence
Int cell(G,i1-'1,j1) = { |[r,s]| : r < G*(1,1)`1 & G*(1,j1)`2 < s & s
< G*(1,j1+1)`2 } by A24,A27,A65,GOBOARD6:20;
end;
A66: i1 = i2 & j1 = j2+1 implies Int right_cell(f,k,G)= Int cell(G,i2-'1,j2
) & Int left_cell(f,k,G)= Int cell(G,i2,j2) by A12,A10,A11,A13,A14,A15,A16,
GOBRD13:27,28;
A67: now
let r be Point of TOP-REAL 2;
assume
A68: r in Int left_cell(f,k,G);
Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:16;
hence r in left_cell(f,k,G) by A68;
Int left_cell(f,k,G) misses L~f by A12,A10,A11,JORDAN9:15;
hence not r in L~f by A68,XBOOLE_0:3;
end;
A69: now
let r be Point of TOP-REAL 2;
assume
A70: r in Int right_cell(f,k,G);
Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:16;
hence r in right_cell(f,k,G) by A70;
Int right_cell(f,k,G) misses L~f by A12,A10,A11,JORDAN9:15;
hence not r in L~f by A70,XBOOLE_0:3;
end;
A71: now
assume that
A72: 1 = j1 and
A73: i2 = i1+1;
Int cell(G,i1,0) = Int cell(G,i1,j1-'1) by A72,NAT_2:8;
hence Int cell(G,i1,j1-'1) = { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1
& s < G*(1,1)`2 } by A18,A22,A73,GOBOARD6:24;
end;
LSeg(f,k) is vertical or LSeg(f,k) is horizontal by SPPOL_1:19;
then
LSeg(f/.k,f/.(k+1)) is vertical or LSeg(f/.k,f/.(k+1)) is horizontal by A10
,A11,TOPREAL1:def 3;
then
A74: (f/.k)`1 =(f/.(k+1))`1 or (f/.k)`2 = (f/.(k+1))`2 by SPPOL_1:15,16;
A75: now
assume that
A76: j1 = j2 and
A77: i2 = i1+1;
i1 < i2 by A77,NAT_1:13;
then (f/.k)`1 < (f/.(k+1))`1 by A14,A16,A21,A18,A26,A29,A76,GOBOARD5:3;
then (f/.k)`1 < p`1 & p`1 < (f/.(k+1))`1 by A39,A50,A20,TOPREAL6:29;
hence
G*(i1,1)`1 < p`1 & p`1 < G*(i1+1,1)`1 by A14,A16,A21,A33,A35,A18,A30,A29
,A76,A77,GOBOARD5:2;
end;
A78: i2 -'1 < i2 by A33,JORDAN5B:1;
A79: now
assume 1 < i2 & j1 = j2+1;
then
A80: 1 <= i2-'1 & j2 < width G by A30,NAT_1:13,NAT_D:49;
i2-'1 < len G & 1 <= j2 by A15,A21,A78,MATRIX_0:32,XXREAL_0:2;
hence
Int cell(G,i2-'1,j2) = { |[r,s]| : G*(i2-'1,1)`1 < r & r < G*(i2-'1+1
,1)`1 & G*(1,j2)`2 < s & s < G*(1,j2+1)`2 } by A80,GOBOARD6:26;
end;
A81: j1 = j2 & i1 = i2+1 implies Int left_cell(f,k,G)= Int cell(G,i2,j1-'1)
& Int right_cell(f,k,G)= Int cell(G,i2,j1) by A12,A10,A11,A13,A14,A15,A16,
GOBRD13:25,26;
A82: now
assume that
A83: j1 = j2 and
A84: i1 = i2+1;
i2 < i1 by A84,NAT_1:13;
then G*(i2,j1)`1 < G*(i1,j1)`1 by A33,A35,A24,A30,GOBOARD5:3;
then (f/.(k+1))`1 < p`1 & p`1 < (f/.k)`1 by A14,A16,A39,A50,A20,A83,
TOPREAL6:29;
hence
G*(i2,1)`1 < p`1 & p`1 < G*(i2+1,1)`1 by A14,A16,A21,A33,A35,A18,A26,A29
,A83,A84,GOBOARD5:2;
end;
A85: i1 -'1 < i1 by A18,JORDAN5B:1;
A86: now
assume 1 < i1 & j2 = j1+1;
then
A87: 1 <= i1-'1 & j1 < width G by A26,NAT_1:13,NAT_D:49;
i1-'1 < len G & 1 <= j1 by A13,A35,A85,MATRIX_0:32,XXREAL_0:2;
hence
Int cell(G,i1-'1,j1) = { |[r,s]| : G*(i1-'1,1)`1 < r & r < G*(i1-'1+1
,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A87,GOBOARD6:26;
end;
A88: i1 = i2 & j2 = j1+1 implies Int left_cell(f,k,G)= Int cell(G,i1-'1,j1)
& Int right_cell(f,k,G)= Int cell(G,i1,j1) by A12,A10,A11,A13,A14,A15,A16,
GOBRD13:21,22;
A89: p <> p1 & p <> p2 by A1,A7,A3,XBOOLE_0:def 4;
then
A90: p1`2 = p2`2 implies i1 = i2 by A13,A14,A15,A16,A74,A61,A39,Th29,JORDAN1G:7
;
A91: p1`1 = p2`1 implies j1 = j2 by A13,A14,A15,A16,A74,A61,A89,A39,Th29,
JORDAN1G:6;
per cases by A2;
suppose
A92: p1`2=p2`2;
Int right_cell(f,k,G) <> {} by A12,A10,A11,JORDAN9:9;
then consider rp9 be object such that
A93: rp9 in Int right_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rp9 as Point of TOP-REAL 2 by A93;
reconsider rp = |[rp9`1,p`2]| as Point of TOP-REAL 2;
A94: p`2 = p1`2 by A5,A92,GOBOARD7:6;
A95: now
assume
A96: j1=j2+1 & 1 < i2;
then ex r,s st rp9 = |[r,s]| & G*(i2-'1,1)`1 < r & r < G*(i2-'1+1,1)`1
& G*(1,j2)`2 < s & s < G*(1,j2+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A66,A79
,A92,A93,Th29,JORDAN1G:7;
then G*(i2-'1,1)`1 < rp9`1 & rp9`1 < G*(i2-'1+1,1)`1 by EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A51,A66
,A79,A92,A96,Th29,JORDAN1G:7;
end;
A97: now
assume
A98: j1=j2+1 & 1 = i2;
then ex r,s st rp9 = |[r,s]| & r < G*(1,1)`1 & G*(1,j2)`2 < s & s < G*(
1,j2+ 1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A66,A58,A92,A93,Th29,
JORDAN1G:7;
then rp9`1 < G*(1,1)`1 by EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A51,A66
,A58,A92,A98,Th29,JORDAN1G:7;
end;
Int left_cell(f,k,G) <> {} by A12,A10,A11,JORDAN9:9;
then consider rl9 be object such that
A99: rl9 in Int left_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rl9 as Point of TOP-REAL 2 by A99;
reconsider rl = |[rl9`1,p`2]| as Point of TOP-REAL 2;
A100: rl`2=p`2 & rp`2=p`2 by EUCLID:52;
A101: now
assume
A102: j2=j1+1 & 1 < i1;
then ex r,s st rl9 = |[r,s]| & G*(i1-'1,1)`1 < r & r < G*(i1-'1+1,1)`1
& G*(1,j1)`2 < s & s < G*(1,j1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A88,A86
,A92,A99,Th29,JORDAN1G:7;
then G*(i1-'1,1)`1 < rl9`1 & rl9`1 < G*(i1-'1+1,1)`1 by EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A55
,A88,A86,A92,A102,Th29,JORDAN1G:7;
end;
A103: now
assume
A104: j2=j1+1 & 1 = i1;
then ex r,s st rl9 = |[r,s]| & r < G*(1,1)`1 & G*(1,j1)`2 < s & s < G*(
1,j1+ 1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A88,A63,A92,A99,Th29,
JORDAN1G:7;
then rl9`1 < G*(1,1)`1 by EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A55
,A88,A63,A92,A104,Th29,JORDAN1G:7;
end;
A105: rl`1=rl9`1 by EUCLID:52;
A106: now
assume
A107: j1=j2+1 & i2 = len G;
then ex r,s st rl9 = |[r,s]| & G*(len G,1)`1 < r & G*(1,j2)`2 < s & s <
G*(1,j2+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A66,A32,A92,A99,Th29,
JORDAN1G:7;
then G*(len G,1)`1 < rl`1 by A105,EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A51
,A66,A32,A92,A105,A107,Th29,JORDAN1G:7;
end;
A108: now
assume
A109: j2=j1+1 & i1 = len G;
then ex r,s st rp9 = |[r,s]| & G*(len G,1)`1 < r & G*(1,j1)`2 < s & s <
G*(1,j1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A88,A28,A92,A93,Th29,
JORDAN1G:7;
then G*(len G,1)`1 < rp9`1 by EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A55,A88
,A28,A92,A109,Th29,JORDAN1G:7;
end;
A110: now
assume
A111: j2=j1+1 & i1 < len G;
then ex r,s st rp9 = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & G*(1
,j1)`2 < s & s < G*(1,j1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A88,A62
,A92,A93,Th29,JORDAN1G:7;
then G*(i1,1)`1 < rp9`1 & rp9`1 < G*(i1+1,1)`1 by EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A55,A88
,A62,A92,A111,Th29,JORDAN1G:7;
end;
A112: now
assume
A113: j1=j2+1 & i2 < len G;
then ex r,s st rl9 = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & G*(1
,j2)`2 < s & s < G*(1,j2+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A66,A34
,A92,A99,Th29,JORDAN1G:7;
then G*(i2,1)`1 < rl`1 & rl`1 < G*(i2+1,1)`1 by A105,EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A51
,A66,A34,A92,A105,A113,Th29,JORDAN1G:7;
end;
now
per cases by A17,A90,A92;
suppose
A114: j1=j2+1;
rp in Int right_cell(f,k,GoB f)
proof
per cases by A33,XXREAL_0:1;
suppose
1 < i2;
hence thesis by A95,A114;
end;
suppose
1 = i2;
hence thesis by A97,A114;
end;
end;
then
A115: rp in right_cell(f,k,GoB f) & not rp in L~f by A69;
rl in Int left_cell(f,k,G)
proof
per cases by A21,XXREAL_0:1;
suppose
i2 < len G;
hence thesis by A112,A114;
end;
suppose
i2 = len G;
hence thesis by A106,A114;
end;
end;
then rl in left_cell(f,k,GoB f) & not rl in L~f by A67;
hence thesis by A1,A7,A6,A9,A10,A11,A92,A94,A100,A115,Th31;
end;
suppose
A116: j2=j1+1;
rp in Int right_cell(f,k,GoB f)
proof
per cases by A35,XXREAL_0:1;
suppose
i1 < len G;
hence thesis by A110,A116;
end;
suppose
i1 = len G;
hence thesis by A108,A116;
end;
end;
then
A117: rp in right_cell(f,k,GoB f) & not rp in L~f by A69;
rl in Int left_cell(f,k,G)
proof
per cases by A18,XXREAL_0:1;
suppose
1 < i1;
hence thesis by A101,A116;
end;
suppose
1 = i1;
hence thesis by A103,A116;
end;
end;
then rl in left_cell(f,k,GoB f) & not rl in L~f by A67;
hence thesis by A1,A7,A6,A9,A10,A11,A92,A94,A100,A117,Th31;
end;
end;
hence thesis;
end;
suppose
A118: p1`1=p2`1;
Int left_cell(f,k,G) <> {} by A12,A10,A11,JORDAN9:9;
then consider rl9 be object such that
A119: rl9 in Int left_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rl9 as Point of TOP-REAL 2 by A119;
reconsider rl = |[p`1,rl9`2]| as Point of TOP-REAL 2;
A120: p`1 = p1`1 by A5,A118,GOBOARD7:5;
A121: rl`2=rl9`2 by EUCLID:52;
A122: now
assume
A123: i1=i2+1 & 1 = j1;
then ex r,s st rl9 = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & s <
G*(1, 1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A81,A46,A118,A119,Th29,
JORDAN1G:6;
then rl`2 < G*(1,1)`2 by A121,EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A82
,A81,A46,A118,A121,A123,Th29,JORDAN1G:6;
end;
A124: now
assume
A125: i2=i1+1 & j1 < width G;
then ex r,s st rl9 = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & G*(1
,j1)`2 < s & s < G*(1,j1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A49,A25,A118
,A119,Th29,JORDAN1G:6;
then G*(1,j1)`2 < rl`2 & rl`2 < G*(1,j1+1)`2 by A121,EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A75
,A49,A25,A118,A121,A125,Th29,JORDAN1G:6;
end;
Int right_cell(f,k,G) <> {} by A12,A10,A11,JORDAN9:9;
then consider rp9 be object such that
A126: rp9 in Int right_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rp9 as Point of TOP-REAL 2 by A126;
reconsider rp = |[p`1,rp9`2]| as Point of TOP-REAL 2;
A127: rl`1=p`1 & rp`1=p`1 by EUCLID:52;
A128: now
assume
A129: i2=i1+1 & 1 < j1;
then ex r,s st rp9 = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & G*(1
,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A49,A41
,A118,A126,Th29,JORDAN1G:6;
then G*(1,j1-'1)`2 < rp9`2 & rp9`2 < G*(1,j1-'1+1)`2 by EUCLID:52;
hence rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A75
,A49,A41,A118,A129,Th29,JORDAN1G:6;
end;
A130: now
assume
A131: i2=i1+1 & 1 = j1;
then ex r,s st rp9 = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & s <
G*(1, 1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A49,A71,A118,A126,Th29,
JORDAN1G:6;
then rp9`2 < G*(1,1)`2 by EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A75,A49
,A71,A118,A131,Th29,JORDAN1G:6;
end;
A132: rp`2=rp9`2 by EUCLID:52;
A133: now
assume
A134: i1=i2+1 & j1 = width G;
then ex r,s st rp9 = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & G*(1
,width G)`2 < s by A13,A14,A15,A16,A74,A61,A89,A39,A81,A37,A118,A126,Th29
,JORDAN1G:6;
then G*(1,width G)`2 < rp`2 by A132,EUCLID:52;
hence
rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A82,A81
,A37,A118,A132,A134,Th29,JORDAN1G:6;
end;
A135: now
assume
A136: i2=i1+1 & j1 = width G;
then ex r,s st rl9 = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & G*(1
,width G)`2 < s by A13,A14,A15,A16,A74,A61,A89,A39,A49,A23,A118,A119,Th29
,JORDAN1G:6;
then G*(1,width G)`2 < rl9`2 by EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A75
,A49,A23,A118,A136,Th29,JORDAN1G:6;
end;
A137: now
assume
A138: i1=i2+1 & 1 < j1;
then ex r,s st rl9 = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & G*(1
,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A81,A44
,A118,A119,Th29,JORDAN1G:6;
then G*(1,j1-'1)`2 < rl9`2 & rl9`2 < G*(1,j1-'1+1)`2 by EUCLID:52;
hence rl in Int left_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A82
,A81,A44,A118,A138,Th29,JORDAN1G:6;
end;
A139: now
assume
A140: i1=i2+1 & j1 < width G;
then ex r,s st rp9 = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & G*(1
,j1)`2 < s & s < G*(1,j1+1)`2 by A13,A14,A15,A16,A74,A61,A89,A39,A81,A43,A118
,A126,Th29,JORDAN1G:6;
then G*(1,j1)`2 < rp`2 & rp`2 < G*(1,j1+1)`2 by A132,EUCLID:52;
hence rp in Int right_cell(f,k,G) by A13,A14,A15,A16,A74,A61,A89,A39,A82
,A81,A43,A118,A132,A140,Th29,JORDAN1G:6;
end;
now
per cases by A17,A91,A118;
suppose
A141: i1=i2+1;
rp in Int right_cell(f,k,GoB f)
proof
per cases by A30,XXREAL_0:1;
suppose
j1 < width G;
hence thesis by A139,A141;
end;
suppose
j1 = width G;
hence thesis by A133,A141;
end;
end;
then
A142: rp in right_cell(f,k,GoB f) & not rp in L~f by A69;
rl in Int left_cell(f,k,G)
proof
per cases by A24,XXREAL_0:1;
suppose
1 < j1;
hence thesis by A137,A141;
end;
suppose
1 = j1;
hence thesis by A122,A141;
end;
end;
then rl in left_cell(f,k,GoB f) & not rl in L~f by A67;
hence thesis by A1,A7,A6,A9,A10,A11,A118,A120,A127,A142,Th31;
end;
suppose
A143: i2=i1+1;
rl in Int left_cell(f,k,GoB f)
proof
per cases by A30,XXREAL_0:1;
suppose
j1 < width G;
hence thesis by A124,A143;
end;
suppose
j1 = width G;
hence thesis by A135,A143;
end;
end;
then
A144: rl in left_cell(f,k,GoB f) & not rl in L~f by A67;
rp in Int right_cell(f,k,G)
proof
per cases by A24,XXREAL_0:1;
suppose
1 < j1;
hence thesis by A128,A143;
end;
suppose
1 = j1;
hence thesis by A130,A143;
end;
end;
then rp in right_cell(f,k,GoB f) & not rp in L~f by A69;
hence thesis by A1,A7,A6,A9,A10,A11,A118,A120,A127,A144,Th31;
end;
end;
hence thesis;
end;
end;
theorem Th33:
for f being non constant standard special_circular_sequence, g
being special FinSequence of TOP-REAL 2 st f,g are_in_general_position for k st
1<=k & k+1<= len g holds card (L~f /\ LSeg(g,k)) is even Element of NAT iff ex
C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & g.k in C & g.(k+1) in
C
proof
let f be non constant standard special_circular_sequence, g being special
FinSequence of TOP-REAL 2 such that
A1: f,g are_in_general_position;
A2: g is_in_general_position_wrt f by A1;
let k such that
A3: 1<=k and
A4: k+1<= len g;
A5: g.k in (L~f)` by A1,A3,A4,Th8;
then
A6: not g.k in (L~f) by XBOOLE_0:def 5;
A7: g.(k+1) in (L~f)` by A1,A3,A4,Th8;
then
A8: not g.(k+1) in (L~f) by XBOOLE_0:def 5;
A9: k < len g by A4,NAT_1:13;
then
A10: k in dom g by A3,FINSEQ_3:25;
then
A11: g/.k = g.k by PARTFUN1:def 6;
then
A12: g.k in LSeg(g,k) by A3,A4,TOPREAL1:21;
set m = L~f /\ LSeg(g,k);
set p1 = g/.k, p2 = g/.(k+1);
A13: LSeg(g,k) = LSeg(p1,p2) by A3,A4,TOPREAL1:def 3;
LSeg(g,k) is vertical or LSeg(g,k) is horizontal by SPPOL_1:19;
then
A14: p1`1=p2`1 or p1`2=p2`2 by A13,SPPOL_1:15,16;
A15: rng g c= the carrier of TOP-REAL 2 by FINSEQ_1:def 4;
1<=k+1 by A3,NAT_1:13;
then
A16: k+1 in dom g by A4,FINSEQ_3:25;
then
A17: g/.(k+1) = g.(k+1) by PARTFUN1:def 6;
then
A18: g.(k+1) in LSeg(g,k) by A3,A4,TOPREAL1:21;
g.(k+1) in rng g by A16,FUNCT_1:3;
then reconsider gk1 = g.(k+1) as Point of TOP-REAL 2 by A15;
g.k in rng g by A10,FUNCT_1:3;
then reconsider gk = g.k as Point of TOP-REAL 2 by A15;
LSeg(gk,gk1) = LSeg(g,k) by A3,A4,A11,A17,TOPREAL1:def 3;
then
A19: LSeg(g,k) is convex;
A20: f is_in_general_position_wrt g by A1;
then
A21: L~f misses rng g;
per cases;
suppose
A22: not m = {};
m is trivial by A3,A9,A20;
then consider x being object such that
A23: m = {x} by A22,ZFMISC_1:131;
x in m by A23,TARSKI:def 1;
then reconsider p = x as Point of TOP-REAL 2;
A24: p2 = g.(k+1) by A16,PARTFUN1:def 6;
then
A25: p2 in rng g by A16,FUNCT_1:3;
A26: p1 = g.k by A10,PARTFUN1:def 6;
then
A27: p1 in rng g by A10,FUNCT_1:3;
A28: now
assume
A29: not (not p1 in L~f & not p2 in L~f);
per cases by A29;
suppose
p1 in L~f;
hence contradiction by A21,A27,XBOOLE_0:3;
end;
suppose
p2 in L~f;
hence contradiction by A21,A25,XBOOLE_0:3;
end;
end;
rng f misses L~g by A2;
then
A30: rng f misses LSeg(p1,p2) by A13,TOPREAL3:19,XBOOLE_1:63;
L~f /\ LSeg(p1,p2) = {p} by A3,A4,A23,TOPREAL1:def 3;
hence thesis by A14,A23,A26,A24,A28,A30,Th2,Th32,CARD_1:30;
end;
suppose
A31: m = {};
then
A32: LSeg(g,k) misses L~f;
then
A33: not (g.(k+1) in RightComp f & g.k in LeftComp f) by A19,A12,A18,
JORDAN1J:36;
A34: now
per cases by A19,A12,A18,A32,JORDAN1J:36;
suppose
A35: not gk in RightComp f;
A36: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
gk in LeftComp f & g.(k+1) in LeftComp f by A6,A7,A8,A33,A35,GOBRD14:17
;
hence ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & g.k
in C & g.(k+1) in C by A36;
end;
suppose
A37: not g.(k+1) in LeftComp f;
A38: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
g.(k+1) in RightComp f & g.k in RightComp f by A5,A6,A7,A8,A33,A37,
GOBRD14:18;
hence ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~f)` & g.k
in C & g.(k+1) in C by A38;
end;
end;
card m = 2*0 by A31,CARD_1:27;
hence thesis by A34;
end;
end;
theorem Th34:
for f1,f2,g1 being special FinSequence of TOP-REAL 2 st f1 ^' f2
is non constant standard special_circular_sequence & f1 ^' f2, g1
are_in_general_position & len g1 >= 2 & g1 is unfolded s.n.c. holds card (L~(f1
^' f2) /\ L~g1) is even Element of NAT iff ex C be Subset of TOP-REAL 2 st C
is_a_component_of (L~(f1 ^' f2))` & g1.1 in C & g1.len g1 in C
proof
let f1,f2,g1 being special FinSequence of TOP-REAL 2 such that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: f1 ^' f2, g1 are_in_general_position and
A3: len g1 >= 2 and
A4: g1 is unfolded s.n.c.;
reconsider g1 as special unfolded s.n.c. FinSequence of TOP-REAL 2 by A4;
set Lf = L~(f1 ^' f2);
(f1 ^' f2) is_in_general_position_wrt g1 by A2;
then
A5: Lf misses rng g1;
defpred P[Nat] means $1 <= len g1 implies for a being FinSequence of
TOP-REAL 2 st a = g1|(Seg $1) holds ( (card (Lf /\ L~a) is even Element of NAT
iff (ex C be Subset of TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(
len a) in C)) );
A6: dom g1 = Seg len g1 by FINSEQ_1:def 3;
A7: 1+1<=len g1 by A3;
A8: now
let k be Nat such that
A9: k>=2 and
A10: P[k];
A11: 1<=k by A9,XXREAL_0:2;
then
A12: 1<=k+1 by NAT_1:13;
now
reconsider b = g1|Seg k as FinSequence of TOP-REAL 2 by FINSEQ_1:18;
1 in Seg k by A11,FINSEQ_1:1;
then
A13: b.1 = g1.1 by FUNCT_1:49;
reconsider s1 = Lf /\ L~b as finite set by A2,Th6,Th11;
set c = LSeg(g1,k);
A14: k in Seg k by A11,FINSEQ_1:1;
reconsider s2 = Lf /\ c as finite set by A2,Th12;
A15: k <=k+1 by NAT_1:13;
then
A16: Seg k c= Seg (k+1) by FINSEQ_1:5;
k>=1+1 by A9;
then
A17: 1<k by NAT_1:13;
A18: g1.1 in Lf` by A2,A7,Th8;
assume
A19: k+1 <= len g1;
then
A20: g1.(k+1) in Lf` & g1.k in Lf` by A2,A11,Th8;
let a being FinSequence of TOP-REAL 2 such that
A21: a = g1|(Seg (k+1));
A22: dom a = dom g1 /\ Seg(k+1) by A21,RELAT_1:61;
A23: k+1 in Seg (k+1) by A12,FINSEQ_1:1;
then
A24: g1.(k+1) = a.(k+1) by A21,FUNCT_1:49
.= a.(len a) by A19,A21,FINSEQ_1:17;
A25: k+1 in Seg len g1 by A12,A19,FINSEQ_1:1;
then
A26: k+1 in dom a by A6,A23,A22,XBOOLE_0:def 4;
then
A27: a/.(k+1) = a.(k+1) by PARTFUN1:def 6
.= g1.(k+1) by A21,A26,FUNCT_1:47
.= g1/.(k+1) by A6,A25,PARTFUN1:def 6;
A28: len a = k+1 by A19,A21,FINSEQ_1:17;
g1|(k+1) = a by A21,FINSEQ_1:def 16;
then L~(a|k) /\ LSeg(a,k) = {a/.k} by A28,A17,GOBOARD2:4;
then
A29: L~(a|k) /\ LSeg(a/.k,a/.(k+1)) = {a/.k} by A11,A28,TOPREAL1:def 3;
1 in Seg (k+1) by A12,FINSEQ_1:1;
then
A30: g1.1 = a.1 by A21,FUNCT_1:49;
reconsider s = Lf /\ L~a as finite set by A2,A21,Th6,Th11;
A31: a = g1|(k+1) by A21,FINSEQ_1:def 16;
A32: k < len g1 by A19,NAT_1:13;
then
A33: k in dom g1 by A6,A11,FINSEQ_1:1;
A34: a|k = (g1|(Seg (k+1)))|(Seg k) by A21,FINSEQ_1:def 16
.= g1|(Seg k) by A16,FUNCT_1:51
.= g1|k by FINSEQ_1:def 16;
A35: b.(len b) = b.k by A32,FINSEQ_1:17
.= g1.k by A14,FUNCT_1:49;
k in Seg (k+1) by A11,A15,FINSEQ_1:1;
then
A36: k in dom a by A33,A22,XBOOLE_0:def 4;
then a/.k = a.k by PARTFUN1:def 6
.= g1.k by A21,A36,FUNCT_1:47
.= g1/.k by A33,PARTFUN1:def 6;
then L~b /\ LSeg(g1/.k,g1/.(k+1)) = {g1/.k} by A34,A27,A29,
FINSEQ_1:def 16;
then L~b /\ LSeg(g1,k) = {g1/.k} by A11,A19,TOPREAL1:def 3;
then
A37: L~b /\ c = {g1.k} by A33,PARTFUN1:def 6;
A38: s1 misses s2
proof
assume s1 meets s2;
then consider x being object such that
A39: x in s1 and
A40: x in s2 by XBOOLE_0:3;
x in L~b & x in c by A39,A40,XBOOLE_0:def 4;
then x in (L~b /\ c) by XBOOLE_0:def 4;
then x = g1.k by A37,TARSKI:def 1;
then
A41: x in rng g1 by A33,FUNCT_1:3;
x in Lf by A39,XBOOLE_0:def 4;
hence contradiction by A5,A41,XBOOLE_0:3;
end;
k+1 in dom g1 by A6,A12,A19,FINSEQ_1:1;
then L~a = L~(g1|k) \/ LSeg(g1/.k,g1/.(k+1)) by A33,A31,TOPREAL3:38
.= L~b \/ LSeg(g1/.k,g1/.(k+1)) by FINSEQ_1:def 16
.= L~b \/ c by A11,A19,TOPREAL1:def 3;
then
A42: s = s1 \/ s2 by XBOOLE_1:23;
per cases;
suppose
A43: card s1 is even Element of NAT;
then reconsider c1 = card (Lf /\ L~b) as even Integer;
now
per cases;
suppose
A44: card s2 is even Element of NAT;
then reconsider c2 = card (Lf /\ c) as even Integer;
reconsider c = card s as Integer;
A45: c = c1 + c2 & ex C be Subset of TOP-REAL 2 st C
is_a_component_of (Lf)` & b. 1 in C & b.(len b) in C by A10,A19,A42,A38,A43,
CARD_2:40,NAT_1:13;
ex C be Subset of TOP-REAL 2 st C is_a_component_of (Lf)` &
g1.k in C & g1.(k+1) in C by A1,A2,A11,A19,A44,Th33;
hence
card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C by A1,A30
,A24,A13,A35,A45,Th16;
end;
suppose
A46: not card s2 is even Element of NAT;
then reconsider c2 = card (Lf /\ c) as odd Integer;
reconsider c = card s as Integer;
A47: c = c1 + c2 & ex C be Subset of TOP-REAL 2 st C
is_a_component_of (Lf)` & b. 1 in C & b.(len b) in C by A10,A19,A42,A38,A43,
CARD_2:40,NAT_1:13;
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)
` & g1.k in C & g1.(k+1) in C) by A1,A2,A11,A19,A46,Th33;
hence
card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C by A1,A30
,A24,A13,A35,A47,Th16;
end;
end;
hence card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C;
end;
suppose
A48: not card s1 is even Element of NAT;
then reconsider c1 = card (Lf /\ L~b) as odd Integer;
now
per cases;
suppose
A49: card s2 is even Element of NAT;
then reconsider c2 = card (Lf /\ c) as even Integer;
reconsider c = card s as Integer;
A50: c = c1 + c2 & not ex C be Subset of TOP-REAL 2 st (C
is_a_component_of (Lf)` & b.1 in C & b.(len b) in C) by A10,A19,A42,A38,A48,
CARD_2:40,NAT_1:13;
ex C be Subset of TOP-REAL 2 st C is_a_component_of (Lf)` &
g1.k in C & g1.(k+1) in C by A1,A2,A11,A19,A49,Th33;
hence
card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C by A1,A30
,A24,A13,A35,A50,Th16;
end;
suppose
A51: not card s2 is even Element of NAT;
then reconsider c2 = card (Lf /\ c) as odd Integer;
reconsider c = card s as Integer;
A52: c = c1 + c2 & not ex C be Subset of TOP-REAL 2 st (C
is_a_component_of (Lf)` & b.1 in C & b.(len b) in C) by A10,A19,A42,A38,A48,
CARD_2:40,NAT_1:13;
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)
` & g1.k in C & g1.(k+1) in C) by A1,A2,A11,A19,A51,Th33;
hence
card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C by A1,A30
,A18,A20,A24,A13,A35,A52,Th17;
end;
end;
hence card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C;
end;
end;
hence P[k+1];
end;
dom g1 = Seg len g1 by FINSEQ_1:def 3;
then
A53: g1|(Seg len g1) = g1;
A54: 2 in dom g1 by A3,FINSEQ_3:25;
A55: 1 <= len g1 by A3,XXREAL_0:2;
then
A56: 1 in dom g1 by FINSEQ_3:25;
now
g1|1 = g1|(Seg 1) by FINSEQ_1:def 16;
then
A57: len (g1|1) = 1 by A55,FINSEQ_1:17;
A58: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
let a being FinSequence of TOP-REAL 2 such that
A59: a = g1|(Seg 2);
A60: a.(len a) = a.2 by A3,A59,FINSEQ_1:17
.= g1.(1+1) by A59,A58,FUNCT_1:49;
1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A61: a.1 = g1.1 by A59,FUNCT_1:49;
L~a = L~(g1|2) by A59,FINSEQ_1:def 16
.= L~(g1|1) \/ LSeg(g1/.1,g1/.(1+1)) by A56,A54,TOPREAL3:38
.= L~(g1|1) \/ LSeg(g1,1) by A3,TOPREAL1:def 3
.= {} \/ LSeg(g1,1) by A57,TOPREAL1:22
.= LSeg(g1,1);
hence card (Lf /\ L~a) is even Element of NAT iff ex C be Subset of
TOP-REAL 2 st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C by A1,A2,A3
,A61,A60,Th33;
end;
then
A62: P[2];
for k be Nat st k>=2 holds P[k] from NAT_1:sch 8(A62,A8);
hence thesis by A3,A53;
end;
theorem
for f1,f2,g1,g2 being special FinSequence of TOP-REAL 2 st f1 ^' f2 is
non constant standard special_circular_sequence & g1 ^' g2 is non constant
standard special_circular_sequence & L~f1 misses L~g2 & L~f2 misses L~g1 & f1
^' f2, g1 ^' g2 are_in_general_position for p1,p2,q1,q2 being Point of TOP-REAL
2 st f1.1 = p1 & f1.len f1 = p2 & g1.1 = q1 & g1.len g1 = q2 & f1/.len f1 = f2
/.1 & g1/.len g1 = g2/.1 & p1 in L~f1 /\ L~f2 & q1 in L~g1 /\ L~g2 & ex C be
Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))` & q1 in C & q2 in C
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(g1 ^' g2))` & p1 in C &
p2 in C
proof
let f1,f2,g1,g2 be special FinSequence of TOP-REAL 2 such that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: g1 ^' g2 is non constant standard special_circular_sequence and
A3: L~f1 misses L~g2 and
A4: L~f2 misses L~g1 and
A5: f1 ^' f2, g1 ^' g2 are_in_general_position;
let p1,p2,q1,q2 be Point of TOP-REAL 2 such that
A6: f1.1 = p1 & f1.len f1 = p2 and
A7: g1.1 = q1 & g1.len g1 = q2 and
A8: f1/.len f1 = f2/.1 and
A9: g1/.len g1 = g2/.1 and
A10: p1 in L~f1 /\ L~f2 and
A11: q1 in L~g1 /\ L~g2 and
A12: ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
& q1 in C & q2 in C;
A13: f1 ^' f2, g1 are_in_general_position by A5,Th7;
A14: now
assume
A15: len f1 = 0 or len f1 =1 or len f2 = 0 or len f2 = 1;
per cases by A15;
suppose
len f1 = 0 or len f1 = 1;
then L~f1 = {} by TOPREAL1:22;
hence contradiction by A10;
end;
suppose
len f2 = 0 or len f2 = 1;
then L~f2 = {} by TOPREAL1:22;
hence contradiction by A10;
end;
end;
then
A16: len f2 is non trivial by NAT_2:def 1;
then
A17: f2 is non trivial by Lm2;
A18: now
assume
A19: len g1 = 0 or len g1 =1 or len g2 = 0 or len g2 =1;
per cases by A19;
suppose
len g1 = 0 or len g1 = 1;
then L~g1 = {} by TOPREAL1:22;
hence contradiction by A11;
end;
suppose
len g2 = 0 or len g2 = 1;
then L~g2 = {} by TOPREAL1:22;
hence contradiction by A11;
end;
end;
then
A20: len g2 is non trivial by NAT_2:def 1;
then
A21: g2 is non trivial by Lm2;
A22: len g1 is non trivial by A18,NAT_2:def 1;
then
A23: g1 is non empty by Lm2;
len g2 >= 1+1 by A20,NAT_2:29;
then
A24: g1 is unfolded s.n.c. by A2,Th4;
len g1 >= 2 by A22,NAT_2:29;
then
A25: card (L~(f1 ^' f2) /\ L~g1) is even Element of NAT by A1,A7,A12,A13,A24
,Th34;
len f2 >= 1+1 by A16,NAT_2:29;
then
A26: f1 is unfolded s.n.c. by A1,Th4;
A27: g1 ^' g2, f1 are_in_general_position by A5,Th7;
A28: len f1 is non trivial by A14,NAT_2:def 1;
then f1 is non empty by Lm2;
then
A29: L~(f1 ^' f2) /\ L~g1 = (L~f1 \/ L~f2) /\ L~g1 by A8,A17,TOPREAL8:35
.= L~f1 /\ L~g1 \/ L~f2 /\ L~g1 by XBOOLE_1:23
.= L~f1 /\ L~g1 \/ {} by A4
.= L~f1 /\ L~g1 \/ L~f1 /\ L~g2 by A3
.= (L~g1 \/ L~g2) /\ L~f1 by XBOOLE_1:23
.= L~f1 /\ L~(g1 ^' g2) by A9,A23,A21,TOPREAL8:35;
len f1 >= 2 by A28,NAT_2:29;
hence thesis by A2,A6,A29,A27,A26,A25,Th34;
end;