:: by Mariusz Giero

::

:: Received May 27, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

Lm1: for f being FinSequence st dom f is trivial holds

len f is trivial

proof end;

Lm2: for f being FinSequence st f is trivial holds

len f is trivial

proof end;

theorem Th3: :: JORDAN12:3

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 )

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
end;

theorem Th4: :: JORDAN12:4

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. )

( f is unfolded & f is s.n.c. )

proof end;

:: deftheorem 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 ) ) );

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);

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;
let f1, f2 be FinSequence of (TOP-REAL n);

pred f1,f2 are_in_general_position means :: JORDAN12:def 2

( f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1 );

symmetry ( f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1 );

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 ) ;

:: deftheorem 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 ) );

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 Th6: :: JORDAN12:6

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

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 Th7: :: JORDAN12:7

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

f1 ^' f2,g1 are_in_general_position

proof end;

theorem Th8: :: JORDAN12:8

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) ` )

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 Th9: :: JORDAN12:9

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

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 Th10: :: JORDAN12:10

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 Th11: :: JORDAN12:11

for f, g being FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds

(L~ f) /\ (L~ g) is finite

(L~ f) /\ (L~ g) is finite

proof end;

theorem Th12: :: JORDAN12:12

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

for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite

proof end;

theorem Th13: :: JORDAN12:13

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 )

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 Th14: :: JORDAN12:14

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 ) ) by JORDAN1H:24, GOBOARD9:def 1, GOBOARD9:def 2;

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 ) ) by JORDAN1H:24, GOBOARD9:def 1, GOBOARD9:def 2;

theorem Th15: :: JORDAN12:15

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 ) ) )

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 Th16: :: JORDAN12:16

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 )

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 Th17: :: JORDAN12:17

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 )

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;

Lm3: now :: thesis: for G being Go-board

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)

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 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) and

A3: w2 in v_strip (G,i) and

A4: w1 `1 <= w2 `1 ; :: thesis: LSeg (w1,w2) c= v_strip (G,i)

thus LSeg (w1,w2) c= v_strip (G,i) :: thesis: verum

end;
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) and

A3: w2 in v_strip (G,i) and

A4: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (w1,w2) or x in v_strip (G,i) )

assume A5: x in LSeg (w1,w2) ; :: thesis: x in v_strip (G,i)

reconsider p = x as Point of (TOP-REAL 2) by A5;

A6: w1 `1 <= p `1 by A4, A5, TOPREAL1:3;

A7: p `1 <= w2 `1 by A4, A5, TOPREAL1:3;

A8: p = |[(p `1),(p `2)]| by EUCLID:53;

end;
assume A5: x in LSeg (w1,w2) ; :: thesis: x in v_strip (G,i)

reconsider p = x as Point of (TOP-REAL 2) by A5;

A6: w1 `1 <= p `1 by A4, A5, TOPREAL1:3;

A7: p `1 <= w2 `1 by A4, A5, TOPREAL1:3;

A8: p = |[(p `1),(p `2)]| by EUCLID:53;

per cases
( i = 0 or i = len G or ( 1 <= i & i < len G ) )
by A1, NAT_1:14, XXREAL_0:1;

end;

suppose
i = 0
; :: thesis: x in v_strip (G,i)

then A9:
v_strip (G,i) = { |[r,s]| where r, s is Real : r <= (G * (1,1)) `1 }
by GOBRD11:18;

then ex r1, s1 being Real st

( w2 = |[r1,s1]| & r1 <= (G * (1,1)) `1 ) by A3;

then w2 `1 <= (G * (1,1)) `1 by EUCLID:52;

then p `1 <= (G * (1,1)) `1 by A7, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A9; :: thesis: verum

end;
then ex r1, s1 being Real st

( w2 = |[r1,s1]| & r1 <= (G * (1,1)) `1 ) by A3;

then w2 `1 <= (G * (1,1)) `1 by EUCLID:52;

then p `1 <= (G * (1,1)) `1 by A7, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A9; :: thesis: verum

suppose
i = len G
; :: thesis: x in v_strip (G,i)

then A10:
v_strip (G,i) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 <= r }
by GOBRD11:19;

then ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * ((len G),1)) `1 <= r1 ) by A2;

then (G * ((len G),1)) `1 <= w1 `1 by EUCLID:52;

then (G * ((len G),1)) `1 <= p `1 by A6, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A10; :: thesis: verum

end;
then ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * ((len G),1)) `1 <= r1 ) by A2;

then (G * ((len G),1)) `1 <= w1 `1 by EUCLID:52;

then (G * ((len G),1)) `1 <= p `1 by A6, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A10; :: thesis: verum

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 ex r2, s2 being Real st

( w2 = |[r2,s2]| & (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 ) by A3;

then w2 `1 <= (G * ((i + 1),1)) `1 by EUCLID:52;

then A12: p `1 <= (G * ((i + 1),1)) `1 by A7, XXREAL_0:2;

ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (i,1)) `1 <= r1 & r1 <= (G * ((i + 1),1)) `1 ) by A2, A11;

then (G * (i,1)) `1 <= w1 `1 by EUCLID:52;

then (G * (i,1)) `1 <= p `1 by A6, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A11, A12; :: thesis: verum

end;
then ex r2, s2 being Real st

( w2 = |[r2,s2]| & (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 ) by A3;

then w2 `1 <= (G * ((i + 1),1)) `1 by EUCLID:52;

then A12: p `1 <= (G * ((i + 1),1)) `1 by A7, XXREAL_0:2;

ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (i,1)) `1 <= r1 & r1 <= (G * ((i + 1),1)) `1 ) by A2, A11;

then (G * (i,1)) `1 <= w1 `1 by EUCLID:52;

then (G * (i,1)) `1 <= p `1 by A6, XXREAL_0:2;

hence x in v_strip (G,i) by A8, A11, A12; :: thesis: verum

Lm4: now :: thesis: for G being Go-board

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)

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 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) and

A3: w2 in h_strip (G,j) and

A4: w1 `2 <= w2 `2 ; :: thesis: LSeg (w1,w2) c= h_strip (G,j)

thus LSeg (w1,w2) c= h_strip (G,j) :: thesis: verum

end;
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) and

A3: w2 in h_strip (G,j) and

A4: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (w1,w2) or x in h_strip (G,j) )

assume A5: x in LSeg (w1,w2) ; :: thesis: x in h_strip (G,j)

then reconsider p = x as Point of (TOP-REAL 2) ;

A6: w1 `2 <= p `2 by A4, A5, TOPREAL1:4;

A7: p `2 <= w2 `2 by A4, A5, TOPREAL1:4;

A8: p = |[(p `1),(p `2)]| by EUCLID:53;

end;
assume A5: x in LSeg (w1,w2) ; :: thesis: x in h_strip (G,j)

then reconsider p = x as Point of (TOP-REAL 2) ;

A6: w1 `2 <= p `2 by A4, A5, TOPREAL1:4;

A7: p `2 <= w2 `2 by A4, A5, TOPREAL1:4;

A8: p = |[(p `1),(p `2)]| by EUCLID:53;

per cases
( j = 0 or j = width G or ( 1 <= j & j < width G ) )
by A1, NAT_1:14, XXREAL_0:1;

end;

suppose
j = 0
; :: thesis: x in h_strip (G,j)

then A9:
h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 }
by GOBRD11:21;

then ex r1, s1 being Real st

( w2 = |[r1,s1]| & s1 <= (G * (1,1)) `2 ) by A3;

then w2 `2 <= (G * (1,1)) `2 by EUCLID:52;

then p `2 <= (G * (1,1)) `2 by A7, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A9; :: thesis: verum

end;
then ex r1, s1 being Real st

( w2 = |[r1,s1]| & s1 <= (G * (1,1)) `2 ) by A3;

then w2 `2 <= (G * (1,1)) `2 by EUCLID:52;

then p `2 <= (G * (1,1)) `2 by A7, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A9; :: thesis: verum

suppose
j = width G
; :: thesis: x in h_strip (G,j)

then A10:
h_strip (G,j) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s }
by GOBRD11:22;

then ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (1,(width G))) `2 <= s1 ) by A2;

then (G * (1,(width G))) `2 <= w1 `2 by EUCLID:52;

then (G * (1,(width G))) `2 <= p `2 by A6, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A10; :: thesis: verum

end;
then ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (1,(width G))) `2 <= s1 ) by A2;

then (G * (1,(width G))) `2 <= w1 `2 by EUCLID:52;

then (G * (1,(width G))) `2 <= p `2 by A6, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A10; :: thesis: verum

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 ex r2, s2 being Real st

( w2 = |[r2,s2]| & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) by A3;

then w2 `2 <= (G * (1,(j + 1))) `2 by EUCLID:52;

then A12: p `2 <= (G * (1,(j + 1))) `2 by A7, XXREAL_0:2;

ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) by A2, A11;

then (G * (1,j)) `2 <= w1 `2 by EUCLID:52;

then (G * (1,j)) `2 <= p `2 by A6, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A11, A12; :: thesis: verum

end;
then ex r2, s2 being Real st

( w2 = |[r2,s2]| & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) by A3;

then w2 `2 <= (G * (1,(j + 1))) `2 by EUCLID:52;

then A12: p `2 <= (G * (1,(j + 1))) `2 by A7, XXREAL_0:2;

ex r1, s1 being Real st

( w1 = |[r1,s1]| & (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) by A2, A11;

then (G * (1,j)) `2 <= w1 `2 by EUCLID:52;

then (G * (1,j)) `2 <= p `2 by A6, XXREAL_0:2;

hence x in h_strip (G,j) by A8, A11, A12; :: thesis: verum

theorem Th21: :: JORDAN12:21

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

for k being Nat st 1 <= k & k + 1 <= len f holds

left_cell (f,k) is convex

proof end;

theorem Th22: :: JORDAN12:22

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 )

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 Th23: :: JORDAN12:23

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)

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;

Lm5: now :: thesis: 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 & ( 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 )

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 & ( 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 )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: 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 & ( for C being Subset of (TOP-REAL 2) holds

( not b_{7} is_a_component_of (L~ b_{5}) ` or not b_{6} in b_{7} or not C in b_{7} ) ) holds

ex C being Subset of (TOP-REAL 2) st

( b_{7} is_a_component_of (L~ b_{5}) ` & b_{6} in b_{7} & b_{4} in b_{7} )

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 b_{6} is_a_component_of (L~ b_{4}) ` or not b_{5} in b_{6} or not C in b_{6} ) ) holds

ex C being Subset of (TOP-REAL 2) st

( b_{6} is_a_component_of (L~ b_{4}) ` & b_{5} in b_{6} & b_{3} in b_{6} )

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 b_{5} is_a_component_of (L~ b_{3}) ` or not b_{4} in b_{5} or not C in b_{5} ) ) implies ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & b_{2} in b_{5} ) )

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 b_{5} is_a_component_of (L~ b_{3}) ` or not b_{4} in b_{5} or not C in b_{5} ) ) implies ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & b_{2} in b_{5} ) )

assume A2: ( ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f ) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & C in b_{5} ) or ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & b_{2} in b_{5} ) )

end;
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 b

ex C being Subset of (TOP-REAL 2) st

( b

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 b

ex C being Subset of (TOP-REAL 2) st

( b

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 b

( b

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 b

( b

assume A2: ( ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f ) ; :: thesis: ( ex C being Subset of (TOP-REAL 2) st

( b

( b

per cases
( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )
by A1, A2, Th23;

end;

suppose
L~ f misses LSeg (p1,r)
; :: thesis: ( ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & C in b_{5} ) or ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & b_{2} in b_{5} ) )

( b

( b

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 Th13; :: thesis: verum

end;
( 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 Th13; :: thesis: verum

suppose
L~ f misses LSeg (r,p2)
; :: thesis: ( ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & C in b_{5} ) or ex C being Subset of (TOP-REAL 2) st

( b_{5} is_a_component_of (L~ b_{3}) ` & b_{4} in b_{5} & b_{2} in b_{5} ) )

( b

( b

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 Th13; :: thesis: verum

end;
( 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 Th13; :: thesis: verum

theorem Th24: :: JORDAN12:24

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

p `1 = r `1

proof end;

theorem Th25: :: JORDAN12:25

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)

p2 in LSeg (p,p1)

proof end;

theorem Th26: :: JORDAN12:26

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)

p2 in LSeg (p,p1)

proof end;

theorem Th27: :: JORDAN12:27

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)

not p1 in LSeg (p,p2)

proof end;

theorem Th28: :: JORDAN12:28

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)

p2 in LSeg (q,p)

proof end;

theorem Th29: :: JORDAN12:29

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

p = p3

proof end;

theorem Th30: :: JORDAN12:30

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 )

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 Th31: :: JORDAN12:31

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 )

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 Th32: :: JORDAN12:32

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 )

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 Th33: :: JORDAN12:33

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 Element of 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 ) )

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 Element of 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 Th34: :: JORDAN12:34

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 Element of 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 ) )

( card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of 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:35

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 )

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;