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