:: JORDAN12 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for R being Relation st R is trivial holds
dom R is trivial
proof end;

Lm2: for f being FinSequence st dom f is trivial holds
len f is trivial
proof end;

Lm3: for f being FinSequence st f is trivial holds
len f is trivial
proof end;

theorem :: JORDAN12:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat st 1 < i holds
0 < i -' 1
proof end;

theorem :: JORDAN12:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: JORDAN12:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
not 1 is even
proof end;

theorem Th4: :: JORDAN12:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being FinSequence of (TOP-REAL n)
for i being Nat st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
proof end;

registration
cluster s.n.c. -> s.c.c. FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is s.n.c. holds
b1 is s.c.c.
proof end;
end;

theorem Th5: :: JORDAN12:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f ^' g is unfolded & f ^' g is s.c.c. & len g >= 2 holds
( f is unfolded & f is s.n.c. )
proof end;

theorem Th6: :: JORDAN12:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g1, g2 being FinSequence of (TOP-REAL 2) holds L~ g1 c= L~ (g1 ^' g2)
proof end;

definition
let n be Nat;
let f1, f2 be FinSequence of (TOP-REAL n);
pred f1 is_in_general_position_wrt f2 means :Def1: :: JORDAN12:def 1
( L~ f1 misses rng f2 & ( for i being Nat st 1 <= i & i < len f2 holds
(L~ f1) /\ (LSeg f2,i) is trivial ) );
end;

:: deftheorem Def1 defines is_in_general_position_wrt JORDAN12:def 1 :
for n being Nat
for f1, f2 being FinSequence of (TOP-REAL n) holds
( f1 is_in_general_position_wrt f2 iff ( L~ f1 misses rng f2 & ( for i being Nat st 1 <= i & i < len f2 holds
(L~ f1) /\ (LSeg f2,i) is trivial ) ) );

definition
let n be Nat;
let f1, f2 be FinSequence of (TOP-REAL n);
pred f1,f2 are_in_general_position means :Def2: :: JORDAN12:def 2
( f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1 );
symmetry
for f1, f2 being FinSequence of (TOP-REAL n) st f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1 holds
( f2 is_in_general_position_wrt f1 & f1 is_in_general_position_wrt f2 )
;
end;

:: deftheorem Def2 defines are_in_general_position JORDAN12:def 2 :
for n being Nat
for f1, f2 being FinSequence of (TOP-REAL n) holds
( f1,f2 are_in_general_position iff ( f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1 ) );

theorem Th7: :: JORDAN12:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
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 end;

theorem Th8: :: JORDAN12:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2, g1, g2 being FinSequence of (TOP-REAL 2) st f1 ^' f2,g1 ^' g2 are_in_general_position holds
f1 ^' f2,g1 are_in_general_position
proof end;

theorem Th9: :: JORDAN12:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for f, g being FinSequence of (TOP-REAL 2) 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 end;

theorem Th10: :: JORDAN12:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of (TOP-REAL 2) st f1,f2 are_in_general_position holds
for i, j being Nat st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg f1,i) /\ (LSeg f2,j) is trivial
proof end;

theorem Th11: :: JORDAN12:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) 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 end;

theorem Th12: :: JORDAN12:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds
(L~ f) /\ (L~ g) is finite
proof end;

theorem Th13: :: JORDAN12:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds
for k being Nat holds (L~ f) /\ (LSeg g,k) is finite
proof end;

theorem Th14: :: JORDAN12:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for p1, p2 being Point of (TOP-REAL 2) st LSeg p1,p2 misses L~ f holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )
proof end;

theorem Th15: :: JORDAN12:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set
for f being non constant standard special_circular_sequence holds
( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) )
proof end;

theorem Th16: :: JORDAN12:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set
for f being non constant standard special_circular_sequence holds
( ( a in (L~ f) ` & b in (L~ f) ` & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ) ) iff ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) )
proof end;

theorem Th17: :: JORDAN12:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for a, b, c being set st ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & b in C & c in C ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
proof end;

theorem Th18: :: JORDAN12:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for a, b, c being set st a in (L~ f) ` & b in (L~ f) ` & c in (L~ f) ` & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ) & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not b in C or not c in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
proof end;

Lm4: now
let G be Go-board; :: thesis: for i being Nat st i <= len G holds
for w1, w2 being Point of (TOP-REAL 2) st w1 in v_strip G,i & w2 in v_strip G,i & w1 `1 <= w2 `1 holds
LSeg w1,w2 c= v_strip G,i

let i be Nat; :: thesis: ( i <= len G implies for w1, w2 being Point of (TOP-REAL 2) st w1 in v_strip G,i & w2 in v_strip G,i & w1 `1 <= w2 `1 holds
LSeg w1,w2 c= v_strip G,i )

assume A1: i <= len G ; :: thesis: for w1, w2 being Point of (TOP-REAL 2) st w1 in v_strip G,i & w2 in v_strip G,i & w1 `1 <= w2 `1 holds
LSeg w1,w2 c= v_strip G,i

let w1, w2 be Point of (TOP-REAL 2); :: thesis: ( w1 in v_strip G,i & w2 in v_strip G,i & w1 `1 <= w2 `1 implies LSeg w1,w2 c= v_strip G,i )
assume that
A2: ( w1 in v_strip G,i & w2 in v_strip G,i ) and
A3: w1 `1 <= w2 `1 ; :: thesis: LSeg w1,w2 c= v_strip G,i
thus LSeg w1,w2 c= v_strip G,i :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg w1,w2 or x in v_strip G,i )
assume A4: x in LSeg w1,w2 ; :: thesis: x in v_strip G,i
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 ( i = 0 or i = len G or ( 1 <= i & i < len G ) ) by A1, XREAL_1:1, NAT_1:39;
suppose i = 0 ; :: thesis: x in v_strip G,i
then A7: v_strip G,i = { |[r,s]| where r, s is Real : r <= (G * 1,1) `1 } by GOBRD11:18;
then consider r1, s1 being 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, XREAL_1:2;
hence x in v_strip G,i by A5, A7; :: thesis: verum
end;
suppose i = len G ; :: thesis: x in v_strip G,i
then A9: v_strip G,i = { |[r,s]| where r, s is Real : (G * (len G),1) `1 <= r } by GOBRD11:19;
then consider r1, s1 being 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, XREAL_1:2;
hence x in v_strip G,i by A5, A9; :: thesis: verum
end;
suppose ( 1 <= i & i < len G ) ; :: thesis: x in v_strip G,i
then A11: v_strip G,i = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } by GOBRD11:20;
then consider r1, s1 being 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, XREAL_1:2;
consider r2, s2 being 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, XREAL_1:2;
hence x in v_strip G,i by A5, A11, A13; :: thesis: verum
end;
end;
end;
end;

theorem Th19: :: JORDAN12:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Go-board st i <= len G holds
v_strip G,i is convex
proof end;

Lm5: now
let G be Go-board; :: thesis: for j being Nat st j <= width G holds
for w1, w2 being Point of (TOP-REAL 2) st w1 in h_strip G,j & w2 in h_strip G,j & w1 `2 <= w2 `2 holds
LSeg w1,w2 c= h_strip G,j

let j be Nat; :: thesis: ( j <= width G implies for w1, w2 being Point of (TOP-REAL 2) st w1 in h_strip G,j & w2 in h_strip G,j & w1 `2 <= w2 `2 holds
LSeg w1,w2 c= h_strip G,j )

assume A1: j <= width G ; :: thesis: for w1, w2 being Point of (TOP-REAL 2) st w1 in h_strip G,j & w2 in h_strip G,j & w1 `2 <= w2 `2 holds
LSeg w1,w2 c= h_strip G,j

let w1, w2 be Point of (TOP-REAL 2); :: thesis: ( w1 in h_strip G,j & w2 in h_strip G,j & w1 `2 <= w2 `2 implies LSeg w1,w2 c= h_strip G,j )
assume that
A2: ( w1 in h_strip G,j & w2 in h_strip G,j ) and
A3: w1 `2 <= w2 `2 ; :: thesis: LSeg w1,w2 c= h_strip G,j
thus LSeg w1,w2 c= h_strip G,j :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg w1,w2 or x in h_strip G,j )
assume A4: x in LSeg w1,w2 ; :: thesis: x in h_strip G,j
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 ( j = 0 or j = width G or ( 1 <= j & j < width G ) ) by A1, XREAL_1:1, NAT_1:39;
suppose j = 0 ; :: thesis: x in h_strip G,j
then A7: h_strip G,j = { |[r,s]| where r, s is Real : s <= (G * 1,1) `2 } by GOBRD11:21;
then consider r1, s1 being 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, XREAL_1:2;
hence x in h_strip G,j by A5, A7; :: thesis: verum
end;
suppose j = width G ; :: thesis: x in h_strip G,j
then A9: h_strip G,j = { |[r,s]| where r, s is Real : (G * 1,(width G)) `2 <= s } by GOBRD11:22;
then consider r1, s1 being 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, XREAL_1:2;
hence x in h_strip G,j by A5, A9; :: thesis: verum
end;
suppose ( 1 <= j & j < width G ) ; :: thesis: x in h_strip G,j
then A11: h_strip G,j = { |[r,s]| where r, s is Real : ( (G * 1,j) `2 <= s & s <= (G * 1,(j + 1)) `2 ) } by GOBRD11:23;
then consider r1, s1 being 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, XREAL_1:2;
consider r2, s2 being 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, XREAL_1:2;
hence x in h_strip G,j by A5, A11, A13; :: thesis: verum
end;
end;
end;
end;

theorem Th20: :: JORDAN12:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for G being Go-board st j <= width G holds
h_strip G,j is convex
proof end;

theorem Th21: :: JORDAN12:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
cell G,i,j is convex
proof end;

theorem Th22: :: JORDAN12:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for k being Nat st 1 <= k & k + 1 <= len f holds
left_cell f,k is convex
proof end;

theorem Th23: :: JORDAN12:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for k being Nat 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 end;

theorem Th24: :: JORDAN12:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence
for r being Point of (TOP-REAL 2) st r in LSeg p1,p2 & ex x being set st (L~ f) /\ (LSeg p1,p2) = {x} & not r in L~ f & not L~ f misses LSeg p1,r holds
L~ f misses LSeg r,p2
proof end;

Lm6: now
let p1, p2 be Point of (TOP-REAL 2);
let f be non constant standard special_circular_sequence; :: thesis: for r being Point of (TOP-REAL 2) st r in LSeg p1,p2 & ex x being set st (L~ f) /\ (LSeg p1,p2) = {x} & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not b6 is_a_component_of (L~ b4) ` or not b5 in b6 or not C in b6 ) ) holds
ex C being Subset of (TOP-REAL 2) st
( b6 is_a_component_of (L~ b4) ` & b5 in b6 & b3 in b6 )

let r be Point of (TOP-REAL 2); :: thesis: ( r in LSeg p1,p2 & ex x being set st (L~ f) /\ (LSeg p1,p2) = {x} & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not b5 is_a_component_of (L~ b3) ` or not b4 in b5 or not C in b5 ) ) implies ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & b2 in b5 ) )

assume A1: r in LSeg p1,p2 ; :: thesis: ( ex x being set st (L~ f) /\ (LSeg p1,p2) = {x} & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not b5 is_a_component_of (L~ b3) ` or not b4 in b5 or not C in b5 ) ) implies ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & b2 in b5 ) )

assume that
A2: ex x being set st (L~ f) /\ (LSeg p1,p2) = {x} and
A3: not r in L~ f ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & C in b5 ) or ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & b2 in b5 ) )

per cases ( L~ f misses LSeg p1,r or L~ f misses LSeg r,p2 ) by A1, A2, A3, Th24;
suppose L~ f misses LSeg p1,r ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & C in b5 ) or ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & b2 in b5 ) )

hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by Th14; :: thesis: verum
end;
suppose L~ f misses LSeg r,p2 ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & C in b5 ) or ex C being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b3) ` & b4 in b5 & b2 in b5 ) )

hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by Th14; :: thesis: verum
end;
end;
end;

theorem Th25: :: JORDAN12:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th26: :: JORDAN12:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2) st not p in LSeg p1,p2 & p1 `2 = p2 `2 & p2 `2 = p `2 & not p1 in LSeg p,p2 holds
p2 in LSeg p,p1
proof end;

theorem Th27: :: JORDAN12:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2) st not p in LSeg p1,p2 & p1 `1 = p2 `1 & p2 `1 = p `1 & not p1 in LSeg p,p2 holds
p2 in LSeg p,p1
proof end;

theorem Th28: :: JORDAN12:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2) st p <> p1 & p <> p2 & p in LSeg p1,p2 holds
not p1 in LSeg p,p2
proof end;

theorem Th29: :: JORDAN12:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2, q being Point of (TOP-REAL 2) 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 ) ) & not p1 in LSeg q,p holds
p2 in LSeg q,p
proof end;

theorem Th30: :: JORDAN12:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3, p4, p being 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} & not p = p1 & not p = p2 holds
p = p3
proof end;

theorem Th31: :: JORDAN12:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence st (L~ f) /\ (LSeg p1,p2) = {p} holds
for r being 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 being Nat 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 & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
proof end;

theorem Th32: :: JORDAN12:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for p1, p2, p being Point of (TOP-REAL 2) st (L~ f) /\ (LSeg p1,p2) = {p} holds
for rl, rp being 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 being Nat 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
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
proof end;

theorem Th33: :: JORDAN12:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence
for p1, p2 being Point of (TOP-REAL 2) 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
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
proof end;

theorem Th34: :: JORDAN12:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for g being special FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds
for k being Nat st 1 <= k & k + 1 <= len g holds
( Card ((L~ f) /\ (LSeg g,k)) is even Nat iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) )
proof end;

theorem Th35: :: JORDAN12:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & g1 is s.n.c. holds
( Card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Nat iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) )
proof end;

theorem :: JORDAN12:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 holds
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 being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C )
proof end;