:: JORDAN12 semantic presentation

begin

            Lm1:  for f being FinSequence st dom f is trivial holds
len f is trivial
proof
let f be FinSequence; ::_thesis: ( dom f is trivial implies len f is trivial )
A1: Seg (len f) = dom f by FINSEQ_1:def_3;
assume A2: dom f is trivial ; ::_thesis: len f is trivial
percases ( dom f is empty or ex x being set st dom f = {x} ) by A2, ZFMISC_1:131;
suppose dom f is empty ; ::_thesis: len f is trivial
then  f = {} ;
hence  len f is trivial by CARD_1:27; ::_thesis: verum
end;
suppose ex x being set st dom f = {x} ; ::_thesis: len f is trivial
hence  len f is trivial by A1, CARD_1:49, FINSEQ_3:20; ::_thesis: verum
end;
end;
end;

Lm2:  for f being FinSequence st f is trivial holds
len f is trivial
proof
let f be FinSequence; ::_thesis: ( f is trivial implies len f is trivial )
assume  f is trivial ; ::_thesis: len f is trivial
then  dom f is trivial ;
hence  len f is trivial by Lm1; ::_thesis: verum
end;

theorem :: JORDAN12:1
for i being Element of NAT st 1 < i holds
0 < i -' 1
proof
let i be Element of NAT ; ::_thesis: ( 1 < i implies 0 < i -' 1 )
assume  1 < i ; ::_thesis: 0 < i -' 1
then  ( 1 - 1 = 0 & 1 -' 1 < i -' 1 ) by NAT_D:56;
hence  0 < i -' 1 by XREAL_0:def_2; ::_thesis: verum
end;

theorem Th2: :: JORDAN12:2
1 is odd
proof
 1 = (2 * 0) + 1 ;
hence  1 is odd ; ::_thesis: verum
end;

theorem Th3: :: JORDAN12:3
for n being Element of NAT
for f being FinSequence of (TOP-REAL n)
for i being Element of NAT st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
proof
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL n)
for i being Element of NAT st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
let f be FinSequence of (TOP-REAL n); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f implies ( f /. i in rng f & f /. (i + 1) in rng f ) )
assume A1: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: ( f /. i in rng f & f /. (i + 1) in rng f )
then A2: i in dom f by SEQ_4:134;
then  f . i in rng f by FUNCT_1:3;
hence  f /. i in rng f by A2, PARTFUN1:def_6; ::_thesis: f /. (i + 1) in rng f
A3: i + 1 in dom f by A1, SEQ_4:134;
then  f . (i + 1) in rng f by FUNCT_1:3;
hence  f /. (i + 1) in rng f by A3, PARTFUN1:def_6; ::_thesis: verum
end;

registration
cluster s.n.c.  ->  s.c.c. for 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
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is s.n.c. implies f is s.c.c. )
assume A1: for i, j being Nat st i + 1 < j holds
LSeg (f,i) misses LSeg (f,j) ; :: according to TOPREAL1:def_7 ::_thesis: f is s.c.c.
let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds
( b1 <= i + 1 or ( ( i <= 1 or len f <= b1 ) & len f <= b1 + 1 ) or LSeg (f,i) misses LSeg (f,b1) )
let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len f <= j ) & len f <= j + 1 ) or LSeg (f,i) misses LSeg (f,j) )
thus  ( j <= i + 1 or ( ( i <= 1 or len f <= j ) & len f <= j + 1 ) or LSeg (f,i) misses LSeg (f,j) ) by A1; ::_thesis: verum
end;
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. )
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f ^' g is unfolded & f ^' g is s.c.c. & len g >= 2 implies ( f is unfolded & f is s.n.c. ) )
assume that
A1: ( f ^' g is unfolded & f ^' g is s.c.c. ) and
A2: len g >= 2 ; ::_thesis: ( f is unfolded & f is s.n.c. )
A3: g <> {} by A2, CARD_1:27;
A4: now__::_thesis:_f_is_s.n.c.
 1 = 2 - 1 ;
then  (len g) - 1 >= 1 by A2, XREAL_1:9;
then A5: (len g) - 1 > 0 by XXREAL_0:2;
assume  not f is s.n.c. ; ::_thesis: contradiction
then consider i, j being Nat such that
A6: i + 1 < j and
A7: not LSeg (f,i) misses LSeg (f,j) by TOPREAL1:def_7;
A8: j in NAT by ORDINAL1:def_12;
A9: now__::_thesis:_(_1_<=_j_&_j_+_1_<=_len_f_)
assume  ( not 1 <= j or not j + 1 <= len f ) ; ::_thesis: contradiction
then  LSeg (f,j) = {} by TOPREAL1:def_3;
hence  contradiction by A7, XBOOLE_1:65; ::_thesis: verum
end;
then  j < len f by NAT_1:13;
then A10: LSeg ((f ^' g),j) = LSeg (f,j) by A8, TOPREAL8:28;
 (len (f ^' g)) + 1 = (len f) + (len g) by A3, GRAPH_2:13;
then  ((len (f ^' g)) + 1) - 1 = (len f) + ((len g) - 1) ;
then  len f < len (f ^' g) by A5, XREAL_1:29;
then A11: j + 1 < len (f ^' g) by A9, XXREAL_0:2;
A12: i in NAT by ORDINAL1:def_12;
now__::_thesis:_(_1_<=_i_&_i_+_1_<=_len_f_)
assume  ( not 1 <= i or not i + 1 <= len f ) ; ::_thesis: contradiction
then  LSeg (f,i) = {} by TOPREAL1:def_3;
hence  contradiction by A7, XBOOLE_1:65; ::_thesis: verum
end;
then  i < len f by NAT_1:13;
then  LSeg ((f ^' g),i) = LSeg (f,i) by A12, TOPREAL8:28;
hence  contradiction by A1, A6, A7, A11, A12, A8, A10, GOBOARD5:def_4; ::_thesis: verum
end;
now__::_thesis:_f_is_unfolded
assume  not f is unfolded ; ::_thesis: contradiction
then consider i being Nat such that
A13: 1 <= i and
A14: i + 2 <= len f and
A15: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) <> {(f /. (i + 1))} by TOPREAL1:def_6;
A16: 1 <= i + 1 by A13, NAT_1:13;
 i + 1 < (i + 1) + 1 by NAT_1:13;
then A17: i + 1 < len f by A14, NAT_1:13;
then A18: LSeg ((f ^' g),(i + 1)) = LSeg (f,(i + 1)) by TOPREAL8:28;
A19: len f <= len (f ^' g) by TOPREAL8:7;
then  i + 1 <= len (f ^' g) by A17, XXREAL_0:2;
then A20: i + 1 in dom (f ^' g) by A16, FINSEQ_3:25;
 ( i in NAT & i < len f ) by A17, NAT_1:13, ORDINAL1:def_12;
then A21: LSeg ((f ^' g),i) = LSeg (f,i) by TOPREAL8:28;
 i + 1 in dom f by A16, A17, FINSEQ_3:25;
then A22: f /. (i + 1) = f . (i + 1) by PARTFUN1:def_6
.= (f ^' g) . (i + 1) by A16, A17, GRAPH_2:14
.= (f ^' g) /. (i + 1) by A20, PARTFUN1:def_6 ;
 i + 2 <= len (f ^' g) by A14, A19, XXREAL_0:2;
hence  contradiction by A1, A13, A15, A22, A21, A18, TOPREAL1:def_6; ::_thesis: verum
end;
hence  ( f is unfolded & f is s.n.c. ) by A4; ::_thesis: verum
end;

theorem Th5: :: JORDAN12:5
for g1, g2 being FinSequence of (TOP-REAL 2) holds L~ g1 c= L~ (g1 ^' g2)
proof
let g1, g2 be FinSequence of (TOP-REAL 2); ::_thesis: L~ g1 c= L~ (g1 ^' g2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g1 or x in L~ (g1 ^' g2) )
assume  x in L~ g1 ; ::_thesis: x in L~ (g1 ^' g2)
then consider a being set  such that
A1: ( x in a & a in  {  (LSeg (g1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g1 )  }  ) by TARSKI:def_4;
consider j being Element of NAT  such that
A2: a = LSeg (g1,j) and
A3: 1 <= j and
A4: j + 1 <= len g1 by A1;
 j < len g1 by A4, NAT_1:13;
then A5: a = LSeg ((g1 ^' g2),j) by A2, TOPREAL8:28;
 len g1 <= len (g1 ^' g2) by TOPREAL8:7;
then  j + 1 <= len (g1 ^' g2) by A4, XXREAL_0:2;
then  a in  {  (LSeg ((g1 ^' g2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (g1 ^' g2) )  }  by A3, A5;
hence  x in L~ (g1 ^' g2) by A1, TARSKI:def_4; ::_thesis: verum
end;

begin

definition
let n be Element of NAT ;
let f1, f2 be FinSequence of (TOP-REAL n);
predf1 is_in_general_position_wrt f2 means :Def1: :: JORDAN12:def 1
( L~ f1 misses rng f2 & ( for i being Element of 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 Element of 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 Element of NAT st 1 <= i & i < len f2 holds
(L~ f1) /\ (LSeg (f2,i)) is trivial ) ) );

definition
let n be Element of NAT ;
let f1, f2 be FinSequence of (TOP-REAL n);
predf1,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 Element of 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 Element of 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
let k be Element of NAT ; ::_thesis: 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
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( f1,f2 are_in_general_position implies for f being FinSequence of (TOP-REAL 2) st f = f2 | (Seg k) holds
f1,f are_in_general_position )
assume A1: f1,f2 are_in_general_position ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f = f2 | (Seg k) holds
f1,f are_in_general_position
then A2: f1 is_in_general_position_wrt f2 by Def2;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f = f2 | (Seg k) implies f1,f are_in_general_position )
assume A3: f = f2 | (Seg k) ; ::_thesis: f1,f are_in_general_position
A4: f = f2 | k by A3, FINSEQ_1:def_15;
then A5: len f <= len f2 by FINSEQ_5:16;
A6: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f_holds_
(L~_f1)_/\_(LSeg_(f,i))_is_trivial
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies (L~ f1) /\ (LSeg (f,i)) is trivial )
assume that
A7: 1 <= i and
A8: i < len f ; ::_thesis: (L~ f1) /\ (LSeg (f,i)) is trivial
 i in dom (f2 | k) by A4, A7, A8, FINSEQ_3:25;
then A9: f /. i = f2 /. i by A4, FINSEQ_4:70;
A10: i + 1 <= len f by A8, NAT_1:13;
then A11: i + 1 <= len f2 by A5, XXREAL_0:2;
then A12: i < len f2 by NAT_1:13;
 1 <= i + 1 by A7, NAT_1:13;
then  i + 1 in dom (f2 | k) by A4, A10, FINSEQ_3:25;
then A13: f /. (i + 1) = f2 /. (i + 1) by A4, FINSEQ_4:70;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A7, A10, TOPREAL1:def_3
.= LSeg (f2,i) by A7, A11, A9, A13, TOPREAL1:def_3 ;
hence  (L~ f1) /\ (LSeg (f,i)) is trivial by A2, A7, A12, Def1; ::_thesis: verum
end;
A14: f2 is_in_general_position_wrt f1 by A1, Def2;
A15: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_f1_holds_
(L~_f)_/\_(LSeg_(f1,i))_is_trivial
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f1 implies (L~ f) /\ (LSeg (f1,i)) is trivial )
assume  ( 1 <= i & i < len f1 ) ; ::_thesis: (L~ f) /\ (LSeg (f1,i)) is trivial
then A16: (L~ f2) /\ (LSeg (f1,i)) is trivial by A14, Def1;
 (L~ f) /\ (LSeg (f1,i)) c= (L~ f2) /\ (LSeg (f1,i)) by A4, TOPREAL3:20, XBOOLE_1:26;
hence  (L~ f) /\ (LSeg (f1,i)) is trivial by A16; ::_thesis: verum
end;
 L~ f2 misses rng f1 by A14, Def1;
then  L~ f misses rng f1 by A4, TOPREAL3:20, XBOOLE_1:63;
then A17: f is_in_general_position_wrt f1 by A15, Def1;
 L~ f1 misses rng f2 by A2, Def1;
then  rng f misses L~ f1 by A3, RELAT_1:70, XBOOLE_1:63;
then  f1 is_in_general_position_wrt f by A6, Def1;
hence  f1,f are_in_general_position by A17, Def2; ::_thesis: verum
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
proof
let f1, f2, g1, g2 be FinSequence of (TOP-REAL 2); ::_thesis: ( f1 ^' f2,g1 ^' g2 are_in_general_position implies f1 ^' f2,g1 are_in_general_position )
assume A1: f1 ^' f2,g1 ^' g2 are_in_general_position ; ::_thesis: f1 ^' f2,g1 are_in_general_position
A2: g1 ^' g2 is_in_general_position_wrt f1 ^' f2 by A1, Def2;
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_(f1_^'_f2)_holds_
(L~_g1)_/\_(LSeg_((f1_^'_f2),i))_is_trivial
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (f1 ^' f2) implies (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial )
assume  ( 1 <= i & i < len (f1 ^' f2) ) ; ::_thesis: (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial
then A4: (L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),i)) is trivial by A2, Def1;
 (L~ g1) /\ (LSeg ((f1 ^' f2),i)) c= (L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),i)) by Th5, XBOOLE_1:26;
hence  (L~ g1) /\ (LSeg ((f1 ^' f2),i)) is trivial by A4; ::_thesis: verum
end;
A5: f1 ^' f2 is_in_general_position_wrt g1 ^' g2 by A1, Def2;
A6: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_g1_holds_
(L~_(f1_^'_f2))_/\_(LSeg_(g1,i))_is_trivial
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len g1 implies (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial )
assume that
A7: 1 <= i and
A8: i < len g1 ; ::_thesis: (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial
 len g1 <= len (g1 ^' g2) by TOPREAL8:7;
then  i < len (g1 ^' g2) by A8, XXREAL_0:2;
then  (L~ (f1 ^' f2)) /\ (LSeg ((g1 ^' g2),i)) is trivial by A5, A7, Def1;
hence  (L~ (f1 ^' f2)) /\ (LSeg (g1,i)) is trivial by A8, TOPREAL8:28; ::_thesis: verum
end;
 L~ (g1 ^' g2) misses rng (f1 ^' f2) by A2, Def1;
then  L~ g1 misses rng (f1 ^' f2) by Th5, XBOOLE_1:63;
then A9: g1 is_in_general_position_wrt f1 ^' f2 by A3, Def1;
 L~ (f1 ^' f2) misses rng (g1 ^' g2) by A5, Def1;
then  L~ (f1 ^' f2) misses rng g1 by TOPREAL8:10, XBOOLE_1:63;
then  f1 ^' f2 is_in_general_position_wrt g1 by A6, Def1;
hence  f1 ^' f2,g1 are_in_general_position by A9, Def2; ::_thesis: verum
end;


theorem Th8: :: JORDAN12:8
for k being Element of 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
let k be Element of NAT ; ::_thesis: 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) ` )
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= k & k + 1 <= len g & f,g are_in_general_position implies ( g . k in (L~ f) ` & g . (k + 1) in (L~ f) ` ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len g and
A3: f,g are_in_general_position ; ::_thesis: ( g . k in (L~ f) ` & g . (k + 1) in (L~ f) ` )
 f is_in_general_position_wrt g by A3, Def2;
then A4: L~ f misses rng g by Def1;
A5: rng g c= the carrier of (TOP-REAL 2) by FINSEQ_1:def_4;
 k < len g by A2, NAT_1:13;
then  k in dom g by A1, FINSEQ_3:25;
then A6: g . k in rng g by FUNCT_1:3;
now__::_thesis:_g_._k_in_(L~_f)_`
assume  not g . k in (L~ f) ` ; ::_thesis: contradiction
then  g . k in ((L~ f) `) ` by A6, A5, XBOOLE_0:def_5;
hence  contradiction by A4, A6, XBOOLE_0:3; ::_thesis: verum
end;
hence  g . k in (L~ f) ` ; ::_thesis: g . (k + 1) in (L~ f) `
 1 <= k + 1 by A1, NAT_1:13;
then  k + 1 in dom g by A2, FINSEQ_3:25;
then A7: g . (k + 1) in rng g by FUNCT_1:3;
now__::_thesis:_g_._(k_+_1)_in_(L~_f)_`
assume  not g . (k + 1) in (L~ f) ` ; ::_thesis: contradiction
then  g . (k + 1) in ((L~ f) `) ` by A5, A7, XBOOLE_0:def_5;
hence  contradiction by A4, A7, XBOOLE_0:3; ::_thesis: verum
end;
hence  g . (k + 1) in (L~ f) ` ; ::_thesis: verum
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 Element of NAT 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); ::_thesis: ( f1,f2 are_in_general_position implies for i, j being Element of NAT st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial )
assume A1: f1,f2 are_in_general_position ; ::_thesis: for i, j being Element of NAT st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial
 f1 is_in_general_position_wrt f2 by A1, Def2;
then A2: L~ f1 misses rng f2 by Def1;
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 implies (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial )
assume that
A3: ( 1 <= i & i + 1 <= len f1 ) and
A4: ( 1 <= j & j + 1 <= len f2 ) ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial
 f2 is_in_general_position_wrt f1 by A1, Def2;
then A5: L~ f2 misses rng f1 by Def1;
now__::_thesis:_(LSeg_(f1,i))_/\_(LSeg_(f2,j))_is_trivial
set B1 = LSeg ((f1 /. i),(f1 /. (i + 1)));
set B2 = LSeg ((f2 /. j),(f2 /. (j + 1)));
set A1 = LSeg (f1,i);
set A2 = LSeg (f2,j);
set A = (LSeg (f1,i)) /\ (LSeg (f2,j));
assume  not (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial ; ::_thesis: contradiction
then consider a1, a2 being set  such that
A6: a1 in (LSeg (f1,i)) /\ (LSeg (f2,j)) and
A7: a2 in (LSeg (f1,i)) /\ (LSeg (f2,j)) and
A8: a1 <> a2 by ZFMISC_1:def_10;
A9: ( a1 in LSeg (f1,i) & a2 in LSeg (f1,i) ) by A6, A7, XBOOLE_0:def_4;
A10: a2 in LSeg (f2,j) by A7, XBOOLE_0:def_4;
A11: a1 in LSeg (f2,j) by A6, XBOOLE_0:def_4;
reconsider a1 = a1, a2 = a2 as Point of (TOP-REAL 2) by A6, A7;
A12: a2 in LSeg ((f2 /. j),(f2 /. (j + 1))) by A4, A10, TOPREAL1:def_3;
A13: LSeg (f1,i) = LSeg ((f1 /. i),(f1 /. (i + 1))) by A3, TOPREAL1:def_3;
then A14: a2 in LSeg ((f1 /. i),(f1 /. (i + 1))) by A7, XBOOLE_0:def_4;
 a1 in LSeg ((f2 /. j),(f2 /. (j + 1))) by A4, A11, TOPREAL1:def_3;
then A15: a1 in (LSeg ((f2 /. j),a2)) \/ (LSeg (a2,(f2 /. (j + 1)))) by A12, TOPREAL1:5;
 f1 /. i in LSeg ((f1 /. i),(f1 /. (i + 1))) by RLTOPSP1:68;
then A16: LSeg (a2,(f1 /. i)) c= LSeg ((f1 /. i),(f1 /. (i + 1))) by A14, TOPREAL1:6;
A17: a1 in (LSeg ((f1 /. i),a2)) \/ (LSeg (a2,(f1 /. (i + 1)))) by A9, A13, TOPREAL1:5;
 f2 /. j in LSeg ((f2 /. j),(f2 /. (j + 1))) by RLTOPSP1:68;
then A18: LSeg (a2,(f2 /. j)) c= LSeg ((f2 /. j),(f2 /. (j + 1))) by A12, TOPREAL1:6;
A19: f2 /. j in rng f2 by A4, Th3;
A20: f1 /. i in rng f1 by A3, Th3;
 f2 /. (j + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) by RLTOPSP1:68;
then A21: LSeg (a2,(f2 /. (j + 1))) c= LSeg ((f2 /. j),(f2 /. (j + 1))) by A12, TOPREAL1:6;
 f1 /. (i + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) by RLTOPSP1:68;
then A22: LSeg (a2,(f1 /. (i + 1))) c= LSeg ((f1 /. i),(f1 /. (i + 1))) by A14, TOPREAL1:6;
A23: f2 /. (j + 1) in rng f2 by A4, Th3;
A24: f1 /. (i + 1) in rng f1 by A3, Th3;
percases ( a1 in LSeg ((f1 /. i),a2) or a1 in LSeg (a2,(f1 /. (i + 1))) ) by A17, XBOOLE_0:def_3;
supposeA25: a1 in LSeg ((f1 /. i),a2) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a1 in LSeg ((f2 /. j),a2) or a1 in LSeg (a2,(f2 /. (j + 1))) ) by A15, XBOOLE_0:def_3;
suppose a1 in LSeg ((f2 /. j),a2) ; ::_thesis: contradiction
then  ( f1 /. i in LSeg (a2,(f2 /. j)) or f2 /. j in LSeg (a2,(f1 /. i)) ) by A8, A25, JORDAN4:41;
then A26: ( f1 /. i in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. j in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A18, A16;
now__::_thesis:_contradiction
percases ( f1 /. i in LSeg (f2,j) or f2 /. j in LSeg (f1,i) ) by A3, A4, A26, TOPREAL1:def_3;
suppose f1 /. i in LSeg (f2,j) ; ::_thesis: contradiction
then  f1 /. i in L~ f2 by SPPOL_2:17;
hence  contradiction by A5, A20, XBOOLE_0:3; ::_thesis: verum
end;
suppose f2 /. j in LSeg (f1,i) ; ::_thesis: contradiction
then  f2 /. j in L~ f1 by SPPOL_2:17;
hence  contradiction by A2, A19, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose a1 in LSeg (a2,(f2 /. (j + 1))) ; ::_thesis: contradiction
then  ( f1 /. i in LSeg (a2,(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg (a2,(f1 /. i)) ) by A8, A25, JORDAN4:41;
then A27: ( f1 /. i in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A16, A21;
now__::_thesis:_contradiction
percases ( f1 /. i in LSeg (f2,j) or f2 /. (j + 1) in LSeg (f1,i) ) by A3, A4, A27, TOPREAL1:def_3;
suppose f1 /. i in LSeg (f2,j) ; ::_thesis: contradiction
then  f1 /. i in L~ f2 by SPPOL_2:17;
hence  contradiction by A5, A20, XBOOLE_0:3; ::_thesis: verum
end;
suppose f2 /. (j + 1) in LSeg (f1,i) ; ::_thesis: contradiction
then  f2 /. (j + 1) in L~ f1 by SPPOL_2:17;
hence  contradiction by A2, A23, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA28: a1 in LSeg (a2,(f1 /. (i + 1))) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a1 in LSeg ((f2 /. j),a2) or a1 in LSeg (a2,(f2 /. (j + 1))) ) by A15, XBOOLE_0:def_3;
suppose a1 in LSeg ((f2 /. j),a2) ; ::_thesis: contradiction
then  ( f1 /. (i + 1) in LSeg (a2,(f2 /. j)) or f2 /. j in LSeg (a2,(f1 /. (i + 1))) ) by A8, A28, JORDAN4:41;
then A29: ( f1 /. (i + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. j in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A18, A22;
now__::_thesis:_contradiction
percases ( f1 /. (i + 1) in LSeg (f2,j) or f2 /. j in LSeg (f1,i) ) by A3, A4, A29, TOPREAL1:def_3;
suppose f1 /. (i + 1) in LSeg (f2,j) ; ::_thesis: contradiction
then  f1 /. (i + 1) in L~ f2 by SPPOL_2:17;
hence  contradiction by A5, A24, XBOOLE_0:3; ::_thesis: verum
end;
suppose f2 /. j in LSeg (f1,i) ; ::_thesis: contradiction
then  f2 /. j in L~ f1 by SPPOL_2:17;
hence  contradiction by A2, A19, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose a1 in LSeg (a2,(f2 /. (j + 1))) ; ::_thesis: contradiction
then  ( f1 /. (i + 1) in LSeg (a2,(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg (a2,(f1 /. (i + 1))) ) by A8, A28, JORDAN4:41;
then A30: ( f1 /. (i + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A22, A21;
now__::_thesis:_contradiction
percases ( f1 /. (i + 1) in LSeg (f2,j) or f2 /. (j + 1) in LSeg (f1,i) ) by A3, A4, A30, TOPREAL1:def_3;
suppose f1 /. (i + 1) in LSeg (f2,j) ; ::_thesis: contradiction
then  f1 /. (i + 1) in L~ f2 by SPPOL_2:17;
hence  contradiction by A5, A24, XBOOLE_0:3; ::_thesis: verum
end;
suppose f2 /. (j + 1) in LSeg (f1,i) ; ::_thesis: contradiction
then  f2 /. (j + 1) in L~ f1 by SPPOL_2:17;
hence  contradiction by A2, A23, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial ; ::_thesis: verum
end;

theorem Th10: :: JORDAN12:10
for f, g being FinSequence of (TOP-REAL 2) holds INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) is finite
proof
deffunc H1( set , set ) ->  set = $1 /\ $2;
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) is finite
set AL =  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  ;
set BL =  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ;
set IN =  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }  ;
A1:  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  is finite by SPPOL_1:23;
set C = INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  );
A2: INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) c=  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) or a in  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }  )
assume  a in INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) ; ::_thesis: a in  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }
then consider X, Y being set  such that
A3: ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) and
A4: a = X /\ Y by SETFAM_1:def_5;
 ( ex i being Element of NAT st
( X = LSeg (f,i) & 1 <= i & i + 1 <= len f ) & ex j being Element of NAT st
( Y = LSeg (g,j) & 1 <= j & j + 1 <= len g ) ) by A3;
then reconsider X = X, Y = Y as Subset of (TOP-REAL 2) ;
 X /\ Y in  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }  by A3;
hence  a in  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }  by A4; ::_thesis: verum
end;
A5:  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  is finite by SPPOL_1:23;
  {  H1(X,Y) where X, Y is Subset of (TOP-REAL 2) : ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )  }  is finite from FRAENKEL:sch_22(A5, A1);
hence  INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) is finite by A2; ::_thesis: verum
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
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f,g are_in_general_position implies (L~ f) /\ (L~ g) is finite )
assume A1: f,g are_in_general_position ; ::_thesis: (L~ f) /\ (L~ g) is finite
set BL =  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ;
set AL =  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  ;
A2: now__::_thesis:_for_Z_being_set_st_Z_in_INTERSECTION_(_{__(LSeg_(f,i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_f_)__}__,_{__(LSeg_(g,j))_where_j_is_Element_of_NAT_:_(_1_<=_j_&_j_+_1_<=_len_g_)__}__)_holds_
Z_is_finite
let Z be set ; ::_thesis: ( Z in INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) implies Z is finite )
assume  Z in INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) ; ::_thesis: Z is finite
then consider X, Y being set  such that
A3: ( X in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  & Y in  {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) and
A4: Z = X /\ Y by SETFAM_1:def_5;
 ( ex i being Element of NAT st
( X = LSeg (f,i) & 1 <= i & i + 1 <= len f ) & ex j being Element of NAT st
( Y = LSeg (g,j) & 1 <= j & j + 1 <= len g ) ) by A3;
hence  Z is finite by A1, A4, Th9; ::_thesis: verum
end;
 ( (L~ f) /\ (L~ g) = union (INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  )) & INTERSECTION ( {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  , {  (LSeg (g,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g )  }  ) is finite ) by Th10, SETFAM_1:28;
hence  (L~ f) /\ (L~ g) is finite by A2, FINSET_1:7; ::_thesis: verum
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 Element of NAT holds (L~ f) /\ (LSeg (g,k)) is finite
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f,g are_in_general_position implies for k being Element of NAT holds (L~ f) /\ (LSeg (g,k)) is finite )
assume  f,g are_in_general_position ; ::_thesis: for k being Element of NAT holds (L~ f) /\ (LSeg (g,k)) is finite
then A1: (L~ f) /\ (L~ g) is finite by Th11;
let k be Element of NAT ; ::_thesis: (L~ f) /\ (LSeg (g,k)) is finite
((L~ f) /\ (L~ g)) /\ (LSeg (g,k)) = (L~ f) /\ ((L~ g) /\ (LSeg (g,k))) by XBOOLE_1:16
.= (L~ f) /\ (LSeg (g,k)) by TOPREAL3:19, XBOOLE_1:28 ;
hence  (L~ f) /\ (LSeg (g,k)) is finite by A1; ::_thesis: verum
end;

begin


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 )
proof
let f be non constant standard special_circular_sequence; ::_thesis: 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 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p1,p2) misses L~ f implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) )
assume A1: LSeg (p1,p2) misses L~ f ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )
A2: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
A3: p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A4: not p1 in L~ f by A1, XBOOLE_0:3;
A5: p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A6: not p2 in L~ f by A1, XBOOLE_0:3;
A7: ( not p2 in RightComp f or not p1 in LeftComp f ) by A1, A3, A5, JORDAN1J:36;
A8: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
now__::_thesis:_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_p1_in_C_&_p2_in_C_)
percases ( not p1 in RightComp f or not p2 in LeftComp f ) by A1, A3, A5, JORDAN1J:36;
suppose not p1 in RightComp f ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )
then  ( p1 in LeftComp f & p2 in LeftComp f ) by A7, A4, A6, GOBRD14:17;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A8; ::_thesis: verum
end;
suppose not p2 in LeftComp f ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C )
then  ( p2 in RightComp f & p1 in RightComp f ) by A7, A4, A6, GOBRD14:18;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) by A2; ::_thesis: verum
end;
end;
end;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & p1 in C & p2 in C ) ; ::_thesis: verum
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 ) )
proof
let a, b be set ; ::_thesis: 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 ) )
let f be non constant standard special_circular_sequence; ::_thesis: ( ( ( 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 ) )
thus  ( 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 ) or ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) by JORDAN1H:24; ::_thesis: ( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) )
 ( LeftComp f is_a_component_of (L~ f) ` & RightComp f is_a_component_of (L~ f) ` ) by GOBOARD9:def_1, GOBOARD9:def_2;
hence  ( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) ) ; ::_thesis: verum
end;

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 ) ) )
proof
let a, b be set ; ::_thesis: 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 ) ) )
let f be non constant standard special_circular_sequence; ::_thesis: ( ( 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 ) ) )
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) ` & ( 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 ) ) & not ( a in LeftComp f & b in RightComp f ) implies ( a in RightComp f & b in LeftComp f ) ) ::_thesis: ( ( ( 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) ` & ( 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 ) ) ) )
proof
assume that
A3: a in (L~ f) ` and
A4: b in (L~ f) ` and
A5: 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 ) ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
A6: a in (LeftComp f) \/ (RightComp f) by A3, GOBRD12:10;
A7: b in (LeftComp f) \/ (RightComp f) by A4, GOBRD12:10;
percases ( a in LeftComp f or a in RightComp f ) by A6, XBOOLE_0:def_3;
supposeA8: a in LeftComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
now__::_thesis:_(_(_a_in_LeftComp_f_&_b_in_RightComp_f_)_or_(_a_in_RightComp_f_&_b_in_LeftComp_f_)_)
percases ( b in LeftComp f or b in RightComp f ) by A7, XBOOLE_0:def_3;
suppose b in LeftComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A1, A5, A8; ::_thesis: verum
end;
suppose b in RightComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A8; ::_thesis: verum
end;
end;
end;
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; ::_thesis: verum
end;
supposeA9: a in RightComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
now__::_thesis:_(_(_a_in_LeftComp_f_&_b_in_RightComp_f_)_or_(_a_in_RightComp_f_&_b_in_LeftComp_f_)_)
percases ( b in RightComp f or b in LeftComp f ) by A7, XBOOLE_0:def_3;
suppose b in RightComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A2, A5, A9; ::_thesis: verum
end;
suppose b in LeftComp f ; ::_thesis: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A9; ::_thesis: verum
end;
end;
end;
hence  ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; ::_thesis: verum
end;
end;
end;
thus  ( ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) implies ( a in (L~ f) ` & b in (L~ f) ` & ( 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 ) ) ) ) ::_thesis: verum
proof
assume A10: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; ::_thesis: ( 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 ) ) )
thus  ( a in (L~ f) ` & b in (L~ f) ` ) ::_thesis: 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 )
proof
 LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
then A11: LeftComp f c= (L~ f) ` by GOBRD12:10;
 RightComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
then A12: RightComp f c= (L~ f) ` by GOBRD12:10;
percases ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A10;
suppose ( a in LeftComp f & b in RightComp f ) ; ::_thesis: ( a in (L~ f) ` & b in (L~ f) ` )
hence  ( a in (L~ f) ` & b in (L~ f) ` ) by A11, A12; ::_thesis: verum
end;
suppose ( a in RightComp f & b in LeftComp f ) ; ::_thesis: ( a in (L~ f) ` & b in (L~ f) ` )
hence  ( a in (L~ f) ` & b in (L~ f) ` ) by A11, A12; ::_thesis: verum
end;
end;
end;
now__::_thesis:_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_)
given C being Subset of (TOP-REAL 2) such that A13: C is_a_component_of (L~ f) ` and
A14: a in C and
A15: b in C ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A10;
supposeA16: ( a in LeftComp f & b in RightComp f ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( C = LeftComp f or C misses LeftComp f ) by A1, A13, GOBOARD9:1;
suppose C = LeftComp f ; ::_thesis: contradiction
then  not LeftComp f misses RightComp f by A15, A16, XBOOLE_0:3;
hence  contradiction by GOBRD14:14; ::_thesis: verum
end;
suppose C misses LeftComp f ; ::_thesis: contradiction
hence  contradiction by A14, A16, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA17: ( a in RightComp f & b in LeftComp f ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( C = LeftComp f or C misses LeftComp f ) by A1, A13, GOBOARD9:1;
suppose C = LeftComp f ; ::_thesis: contradiction
then  not LeftComp f misses RightComp f by A14, A17, XBOOLE_0:3;
hence  contradiction by GOBRD14:14; ::_thesis: verum
end;
suppose C misses LeftComp f ; ::_thesis: contradiction
hence  contradiction by A15, A17, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  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 ) ; ::_thesis: verum
end;
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 )
proof
let f be non constant standard special_circular_sequence; ::_thesis: 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 )
let a, b, c be set ; ::_thesis: ( 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 ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) )
assume that
A1: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) and
A2: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & b in C & c in C ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
percases ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) by A1, Th14;
supposeA3: ( a in RightComp f & b in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
now__::_thesis:_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_a_in_C_&_c_in_C_)
percases ( ( b in RightComp f & c in RightComp f ) or ( b in LeftComp f & c in LeftComp f ) ) by A2, Th14;
supposeA4: ( b in RightComp f & c in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
 RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A3, A4; ::_thesis: verum
end;
suppose ( b in LeftComp f & c in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
then  LeftComp f meets RightComp f by A3, XBOOLE_0:3;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; ::_thesis: verum
end;
supposeA5: ( a in LeftComp f & b in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
now__::_thesis:_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_a_in_C_&_c_in_C_)
percases ( ( b in LeftComp f & c in LeftComp f ) or ( b in RightComp f & c in RightComp f ) ) by A2, Th14;
supposeA6: ( b in LeftComp f & c in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
 LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A5, A6; ::_thesis: verum
end;
suppose ( b in RightComp f & c in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
then  LeftComp f meets RightComp f by A5, XBOOLE_0:3;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; ::_thesis: verum
end;
end;
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 )
proof
let f be non constant standard special_circular_sequence; ::_thesis: 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 )
let a, b, c be set ; ::_thesis: ( 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 ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) )
assume that
A1: a in (L~ f) ` and
A2: b in (L~ f) ` and
A3: c in (L~ f) ` and
A4: 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 ) and
A5: 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 ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
A6: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
A7: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
percases ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A1, A2, A4, Th15;
supposeA8: ( a in LeftComp f & b in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
now__::_thesis:_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_a_in_C_&_c_in_C_)
percases ( ( b in LeftComp f & c in RightComp f ) or ( b in RightComp f & c in LeftComp f ) ) by A2, A3, A5, Th15;
suppose ( b in LeftComp f & c in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
then  LeftComp f meets RightComp f by A8, XBOOLE_0:3;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:14; ::_thesis: verum
end;
suppose ( b in RightComp f & c in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A6, A8; ::_thesis: verum
end;
end;
end;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; ::_thesis: verum
end;
supposeA9: ( a in RightComp f & b in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
now__::_thesis:_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_a_in_C_&_c_in_C_)
percases ( ( b in RightComp f & c in LeftComp f ) or ( b in LeftComp f & c in RightComp f ) ) by A2, A3, A5, Th15;
suppose ( b in RightComp f & c in LeftComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
then  LeftComp f meets RightComp f by A9, XBOOLE_0:3;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:14; ::_thesis: verum
end;
suppose ( b in LeftComp f & c in RightComp f ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A7, A9; ::_thesis: verum
end;
end;
end;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; ::_thesis: verum
end;
end;
end;

begin

Lm3: now__::_thesis:_for_G_being_Go-board
for_i_being_Element_of_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 Element of 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 Element of 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 set ; :: 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;
percases ( i = 0 or i = len G or ( 1 <= i & i < len G ) ) by A1, NAT_1:14, XXREAL_0:1;
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;
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;
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;
end;
end;
end;

theorem Th18: :: JORDAN12:18
for i being Element of NAT
for G being Go-board st i <= len G holds
v_strip (G,i) is convex
proof
let i be Element of NAT ; ::_thesis: for G being Go-board st i <= len G holds
v_strip (G,i) is convex
let G be Go-board; ::_thesis: ( i <= len G implies v_strip (G,i) is convex )
assume A1: i <= len G ; ::_thesis: v_strip (G,i) is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in v_strip (G,i) or not w2 in v_strip (G,i) or LSeg (w1,w2) c= v_strip (G,i) )
set P = v_strip (G,i);
A2: ( w1 `1 <= w2 `1 or w2 `1 <= w1 `1 ) ;
assume  ( w1 in v_strip (G,i) & w2 in v_strip (G,i) ) ; ::_thesis: LSeg (w1,w2) c= v_strip (G,i)
hence  LSeg (w1,w2) c= v_strip (G,i) by A1, A2, Lm3; ::_thesis: verum
end;

Lm4: now__::_thesis:_for_G_being_Go-board
for_j_being_Element_of_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 Element of 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 Element of 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 set ; :: 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;
percases ( j = 0 or j = width G or ( 1 <= j & j < width G ) ) by A1, NAT_1:14, XXREAL_0:1;
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;
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;
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;
end;
end;
end;

theorem Th19: :: JORDAN12:19
for j being Element of NAT
for G being Go-board st j <= width G holds
h_strip (G,j) is convex
proof
let j be Element of NAT ; ::_thesis: for G being Go-board st j <= width G holds
h_strip (G,j) is convex
let G be Go-board; ::_thesis: ( j <= width G implies h_strip (G,j) is convex )
assume A1: j <= width G ; ::_thesis: h_strip (G,j) is convex
set P = h_strip (G,j);
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in h_strip (G,j) or not w2 in h_strip (G,j) or LSeg (w1,w2) c= h_strip (G,j) )
assume A2: ( w1 in h_strip (G,j) & w2 in h_strip (G,j) ) ; ::_thesis: LSeg (w1,w2) c= h_strip (G,j)
 ( w1 `2 <= w2 `2 or w2 `2 <= w1 `2 ) ;
hence  LSeg (w1,w2) c= h_strip (G,j) by A1, A2, Lm4; ::_thesis: verum
end;

theorem Th20: :: JORDAN12:20
for i, j being Element of NAT
for G being Go-board st i <= len G & j <= width G holds
cell (G,i,j) is convex
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds
cell (G,i,j) is convex
let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies cell (G,i,j) is convex )
assume  ( i <= len G & j <= width G ) ; ::_thesis: cell (G,i,j) is convex
then  ( v_strip (G,i) is convex & h_strip (G,j) is convex ) by Th18, Th19;
hence  cell (G,i,j) is convex by GOBOARD9:6; ::_thesis: verum
end;

theorem Th21: :: JORDAN12:21
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
left_cell (f,k) is convex
proof
let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
left_cell (f,k) is convex
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k) is convex )
assume  ( 1 <= k & k + 1 <= len f ) ; ::_thesis: left_cell (f,k) is convex
then  ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by GOBOARD9:11;
hence  left_cell (f,k) is convex by Th20; ::_thesis: verum
end;

theorem Th22: :: JORDAN12:22
for f being non constant standard special_circular_sequence
for k being Element of 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
let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of 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 )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex )
 left_cell (f,k) = left_cell (f,k,(GoB f)) by A1, A2, JORDAN1H:21;
hence  left_cell (f,k,(GoB f)) is convex by A1, A2, Th21; ::_thesis: right_cell (f,k,(GoB f)) is convex
 k <= len f by A2, NAT_1:13;
then A3: ((len f) -' k) + k = len f by XREAL_1:235;
then A4: (len f) -' k >= 1 by A2, XREAL_1:6;
then A5: right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A3, GOBOARD9:10;
 ( len f = len (Rev f) & ((len f) -' k) + 1 <= len f ) by A1, A3, FINSEQ_5:def_3, XREAL_1:6;
then  left_cell ((Rev f),((len f) -' k)) is convex by A4, Th21;
hence  right_cell (f,k,(GoB f)) is convex by A1, A2, A5, JORDAN1H:23; ::_thesis: verum
end;

begin

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)
proof
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 & not L~ f misses LSeg (p1,r) holds
L~ f misses LSeg (r,p2)
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 & not L~ f misses LSeg (p1,r) holds
L~ f misses LSeg (r,p2)
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 & not L~ f misses LSeg (p1,r) implies L~ f misses LSeg (r,p2) )
assume that
A1: r in LSeg (p1,p2) and
A2: ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} and
A3: not r in L~ f ; ::_thesis: ( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )
consider p being set  such that
A4: (L~ f) /\ (LSeg (p1,p2)) = {p} by A2;
A5: p in {p} by TARSKI:def_1;
then A6: p in LSeg (p1,p2) by A4, XBOOLE_0:def_4;
reconsider p = p as Point of (TOP-REAL 2) by A4, A5;
A7: now__::_thesis:_(_(LSeg_(p1,r))_/\_(LSeg_(r,p))_=_{r}_or_(LSeg_(p,r))_/\_(LSeg_(r,p2))_=_{r}_)
A8: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A6, TOPREAL1:5;
percases ( r in LSeg (p1,p) or r in LSeg (p,p2) ) by A1, A8, XBOOLE_0:def_3;
suppose r in LSeg (p1,p) ; ::_thesis: ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} )
hence  ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} ) by TOPREAL1:8; ::_thesis: verum
end;
suppose r in LSeg (p,p2) ; ::_thesis: ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} )
hence  ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} ) by TOPREAL1:8; ::_thesis: verum
end;
end;
end;
 p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A9: LSeg (p2,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;
 p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A10: LSeg (p1,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;
now__::_thesis:_(_L~_f_meets_LSeg_(p1,r)_implies_not_L~_f_meets_LSeg_(r,p2)_)
assume that
A11: L~ f meets LSeg (p1,r) and
A12: L~ f meets LSeg (r,p2) ; ::_thesis: contradiction
percases ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} ) by A7;
supposeA13: (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} ; ::_thesis: contradiction
consider x being set  such that
A14: x in L~ f and
A15: x in LSeg (p1,r) by A11, XBOOLE_0:3;
 x in (L~ f) /\ (LSeg (p1,p2)) by A10, A14, A15, XBOOLE_0:def_4;
then  x = p by A4, TARSKI:def_1;
then  x in LSeg (r,p) by RLTOPSP1:68;
then  x in (LSeg (p1,r)) /\ (LSeg (r,p)) by A15, XBOOLE_0:def_4;
hence  contradiction by A3, A13, A14, TARSKI:def_1; ::_thesis: verum
end;
supposeA16: (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} ; ::_thesis: contradiction
consider x being set  such that
A17: x in L~ f and
A18: x in LSeg (r,p2) by A12, XBOOLE_0:3;
 x in (L~ f) /\ (LSeg (p1,p2)) by A9, A17, A18, XBOOLE_0:def_4;
then  x = p by A4, TARSKI:def_1;
then  x in LSeg (p,r) by RLTOPSP1:68;
then  x in (LSeg (p,r)) /\ (LSeg (r,p2)) by A18, XBOOLE_0:def_4;
hence  contradiction by A3, A16, A17, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  ( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) ) ; ::_thesis: verum
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_)
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 b7 is_a_component_of (L~ b5) ` or not b6 in b7 or not C in b7 ) ) holds
ex C being Subset of (TOP-REAL 2) st
( b7 is_a_component_of (L~ b5) ` & b6 in b7 & b4 in b7 )
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 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
( 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 ) )
percases ( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) ) by A1, A2, Th23;
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 Th13; ::_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 Th13; ::_thesis: verum
end;
end;
end;

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
proof
let p, q, r, s be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is vertical & LSeg (r,s) is vertical & LSeg (p,q) meets LSeg (r,s) implies p `1 = r `1 )
assume that
A1: LSeg (p,q) is vertical and
A2: LSeg (r,s) is vertical ; ::_thesis: ( not LSeg (p,q) meets LSeg (r,s) or p `1 = r `1 )
assume  LSeg (p,q) meets LSeg (r,s) ; ::_thesis: p `1 = r `1
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:4;
A4: x in LSeg (r,s) by A3, XBOOLE_0:def_4;
 x in LSeg (p,q) by A3, XBOOLE_0:def_4;
hence p `1 = x `1 by A1, SPPOL_1:41
.= r `1 by A2, A4, SPPOL_1:41 ;
::_thesis: verum
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)
proof
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( not p in LSeg (p1,p2) & p1 `2 = p2 `2 & p2 `2 = p `2 & not p1 in LSeg (p,p2) implies p2 in LSeg (p,p1) )
assume that
A1: not p in LSeg (p1,p2) and
A2: ( p1 `2 = p2 `2 & p2 `2 = p `2 ) ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
percases ( p1 `1 <= p2 `1 or p2 `1 <= p1 `1 ) ;
supposeA3: p1 `1 <= p2 `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now__::_thesis:_(_p1_in_LSeg_(p,p2)_or_p2_in_LSeg_(p,p1)_)
percases ( p `1 < p1 `1 or p2 `1 < p `1 ) by A1, A2, GOBOARD7:8;
suppose p `1 < p1 `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:8; ::_thesis: verum
end;
suppose p2 `1 < p `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:8; ::_thesis: verum
end;
end;
end;
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; ::_thesis: verum
end;
supposeA4: p2 `1 <= p1 `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now__::_thesis:_(_p1_in_LSeg_(p,p2)_or_p2_in_LSeg_(p,p1)_)
percases ( p `1 < p2 `1 or p1 `1 < p `1 ) by A1, A2, GOBOARD7:8;
suppose p `1 < p2 `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:8; ::_thesis: verum
end;
suppose p1 `1 < p `1 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:8; ::_thesis: verum
end;
end;
end;
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; ::_thesis: verum
end;
end;
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)
proof
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( not p in LSeg (p1,p2) & p1 `1 = p2 `1 & p2 `1 = p `1 & not p1 in LSeg (p,p2) implies p2 in LSeg (p,p1) )
assume that
A1: not p in LSeg (p1,p2) and
A2: ( p1 `1 = p2 `1 & p2 `1 = p `1 ) ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
percases ( p1 `2 <= p2 `2 or p2 `2 <= p1 `2 ) ;
supposeA3: p1 `2 <= p2 `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now__::_thesis:_(_p1_in_LSeg_(p,p2)_or_p2_in_LSeg_(p,p1)_)
percases ( p `2 < p1 `2 or p2 `2 < p `2 ) by A1, A2, GOBOARD7:7;
suppose p `2 < p1 `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:7; ::_thesis: verum
end;
suppose p2 `2 < p `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:7; ::_thesis: verum
end;
end;
end;
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; ::_thesis: verum
end;
supposeA4: p2 `2 <= p1 `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now__::_thesis:_(_p1_in_LSeg_(p,p2)_or_p2_in_LSeg_(p,p1)_)
percases ( p `2 < p2 `2 or p1 `2 < p `2 ) by A1, A2, GOBOARD7:7;
suppose p `2 < p2 `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:7; ::_thesis: verum
end;
suppose p1 `2 < p `2 ; ::_thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:7; ::_thesis: verum
end;
end;
end;
hence  ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; ::_thesis: verum
end;
end;
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)
proof
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p <> p1 & p <> p2 & p in LSeg (p1,p2) implies not p1 in LSeg (p,p2) )
assume that
A1: ( p <> p1 & p <> p2 ) and
A2: p in LSeg (p1,p2) ; ::_thesis: not p1 in LSeg (p,p2)
A3: (LSeg (p1,p)) \/ (LSeg (p,p2)) = LSeg (p1,p2) by A2, TOPREAL1:5;
now__::_thesis:_not_p1_in_LSeg_(p,p2)
assume  p1 in LSeg (p,p2) ; ::_thesis: contradiction
then A4: (LSeg (p,p1)) \/ (LSeg (p1,p2)) = LSeg (p,p2) by TOPREAL1:5;
 (LSeg (p,p1)) \/ (LSeg (p1,p2)) = LSeg (p1,p2) by A3, XBOOLE_1:7, XBOOLE_1:12;
hence  contradiction by A1, A4, SPPOL_1:8; ::_thesis: verum
end;
hence  not p1 in LSeg (p,p2) ; ::_thesis: verum
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)
proof
let p, p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( 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) implies p2 in LSeg (q,p) )
assume 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 ) ) ; ::_thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )
A5: not p1 in LSeg (p,p2) by A2, A3, Th27;
A6: not p2 in LSeg (p,p1) by A2, A3, Th27;
percases ( p1 in LSeg (q,p2) or p2 in LSeg (q,p1) ) by A1, A4, Th25, Th26;
supposeA7: p1 in LSeg (q,p2) ; ::_thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )
A8: p in (LSeg (q,p1)) \/ (LSeg (p1,p2)) by A2, XBOOLE_0:def_3;
 (LSeg (q,p1)) \/ (LSeg (p1,p2)) = LSeg (q,p2) by A7, TOPREAL1:5;
then  (LSeg (q,p)) \/ (LSeg (p,p2)) = LSeg (q,p2) by A8, TOPREAL1:5;
hence  ( p1 in LSeg (q,p) or p2 in LSeg (q,p) ) by A5, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA9: p2 in LSeg (q,p1) ; ::_thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )
A10: p in (LSeg (q,p2)) \/ (LSeg (p1,p2)) by A2, XBOOLE_0:def_3;
 (LSeg (q,p2)) \/ (LSeg (p1,p2)) = LSeg (q,p1) by A9, TOPREAL1:5;
then  (LSeg (q,p)) \/ (LSeg (p,p1)) = LSeg (q,p1) by A10, TOPREAL1:5;
hence  ( p1 in LSeg (q,p) or p2 in LSeg (q,p) ) by A6, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
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
proof
let p1, p2, p3, p4, p be Point of (TOP-REAL 2); ::_thesis: ( ( ( 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 implies p = p3 )
assume 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} ; ::_thesis: ( p = p1 or p = p2 or p = p3 )
A3: p in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A2, TARSKI:def_1;
then  p in LSeg (p3,p4) by XBOOLE_0:def_4;
then  (LSeg (p3,p)) \/ (LSeg (p,p4)) = LSeg (p3,p4) by TOPREAL1:5;
then A4: LSeg (p3,p) c= LSeg (p3,p4) by XBOOLE_1:7;
A5: LSeg (p1,p2) meets LSeg (p3,p4) by A3, XBOOLE_0:4;
A6: now__::_thesis:_(_p1_`2_=_p2_`2_&_p3_`2_=_p4_`2_implies_p2_`2_=_p3_`2_)
assume  ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ; ::_thesis: p2 `2 = p3 `2
then  ( LSeg (p1,p2) is horizontal & LSeg (p3,p4) is horizontal ) by SPPOL_1:15;
hence  p2 `2 = p3 `2 by A5, SPRECT_3:9; ::_thesis: verum
end;
A7: now__::_thesis:_(_p1_`1_=_p2_`1_&_p3_`1_=_p4_`1_implies_p2_`1_=_p3_`1_)
assume  ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) ; ::_thesis: p2 `1 = p3 `1
then  ( LSeg (p1,p2) is vertical & LSeg (p3,p4) is vertical ) by SPPOL_1:16;
hence  p2 `1 = p3 `1 by A5, Th24; ::_thesis: verum
end;
A8: p3 in LSeg (p3,p4) by RLTOPSP1:68;
A9: p2 in LSeg (p1,p2) by RLTOPSP1:68;
A10: p1 in LSeg (p1,p2) by RLTOPSP1:68;
now__::_thesis:_(_p_<>_p1_&_p_<>_p2_implies_not_p_<>_p3_)
A11: p in LSeg (p1,p2) by A3, XBOOLE_0:def_4;
assume that
A12: p <> p1 and
A13: p <> p2 and
A14: p <> p3 ; ::_thesis: contradiction
A15: now__::_thesis:_not_p3_in_LSeg_(p1,p2)
assume  p3 in LSeg (p1,p2) ; ::_thesis: contradiction
then  p3 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A8, XBOOLE_0:def_4;
hence  contradiction by A2, A14, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_contradiction
percases ( p1 in LSeg (p3,p) or p2 in LSeg (p3,p) ) by A1, A7, A6, A12, A13, A11, A15, Th28;
suppose p1 in LSeg (p3,p) ; ::_thesis: contradiction
then  p1 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A4, A10, XBOOLE_0:def_4;
hence  contradiction by A2, A12, TARSKI:def_1; ::_thesis: verum
end;
suppose p2 in LSeg (p3,p) ; ::_thesis: contradiction
then  p2 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A4, A9, XBOOLE_0:def_4;
hence  contradiction by A2, A13, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( p = p1 or p = p2 or p = p3 ) ; ::_thesis: verum
end;

begin

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 Element of 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
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: 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 Element of 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 )
let f be non constant standard special_circular_sequence; ::_thesis: ( (L~ f) /\ (LSeg (p1,p2)) = {p} implies 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 Element of 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 ) )
assume  (L~ f) /\ (LSeg (p1,p2)) = {p} ; ::_thesis: 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 Element of 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 )
then A1: p in (L~ f) /\ (LSeg (p1,p2)) by TARSKI:def_1;
then A2: p in LSeg (p1,p2) by XBOOLE_0:def_4;
let r be Point of (TOP-REAL 2); ::_thesis: ( 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 Element of 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 ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume that
A3: not r in LSeg (p1,p2) and
A4: not p1 in L~ f and
A5: not p2 in L~ f and
A6: ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) and
A7: ex i being Element of 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) ) and
A8: not r in L~ f ; ::_thesis: ( 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 ) )
consider i being Element of NAT  such that
A9: ( 1 <= i & i + 1 <= len f ) and
A10: ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) and
A11: p in LSeg (f,i) by A7;
A12: right_cell (f,i,(GoB f)) is convex by A9, Th22;
A13: f is_sequence_on GoB f by GOBOARD5:def_5;
then A14: (right_cell (f,i,(GoB f))) \ (L~ f) c= RightComp f by A9, JORDAN9:27;
A15: now__::_thesis:_(_r_in_right_cell_(f,i,(GoB_f))_implies_r_in_RightComp_f_)
assume  r in right_cell (f,i,(GoB f)) ; ::_thesis: r in RightComp f
then  r in (right_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def_5;
hence  r in RightComp f by A14; ::_thesis: verum
end;
A16: LSeg (f,i) c= right_cell (f,i,(GoB f)) by A13, A9, JORDAN1H:22;
A17: now__::_thesis:_(_p1_in_LSeg_(r,p)_&_r_in_right_cell_(f,i,(GoB_f))_implies_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_r_in_C_&_p1_in_C_)_)
assume that
A18: p1 in LSeg (r,p) and
A19: r in right_cell (f,i,(GoB f)) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
 LSeg (r,p) c= right_cell (f,i,(GoB f)) by A11, A16, A12, A19, JORDAN1:def_1;
then  p1 in (right_cell (f,i,(GoB f))) \ (L~ f) by A4, A18, XBOOLE_0:def_5;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A14, A15, A19, Th14; ::_thesis: verum
end;
A20: left_cell (f,i,(GoB f)) is convex by A9, Th22;
A21: (left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f by A13, A9, JORDAN9:27;
A22: now__::_thesis:_(_r_in_left_cell_(f,i,(GoB_f))_implies_r_in_LeftComp_f_)
assume  r in left_cell (f,i,(GoB f)) ; ::_thesis: r in LeftComp f
then  r in (left_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def_5;
hence  r in LeftComp f by A21; ::_thesis: verum
end;
A23: LSeg (f,i) c= left_cell (f,i,(GoB f)) by A13, A9, JORDAN1H:20;
A24: now__::_thesis:_(_p1_in_LSeg_(r,p)_&_r_in_left_cell_(f,i,(GoB_f))_implies_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_r_in_C_&_p1_in_C_)_)
assume that
A25: p1 in LSeg (r,p) and
A26: r in left_cell (f,i,(GoB f)) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
 LSeg (r,p) c= left_cell (f,i,(GoB f)) by A11, A23, A20, A26, JORDAN1:def_1;
then  p1 in (left_cell (f,i,(GoB f))) \ (L~ f) by A4, A25, XBOOLE_0:def_5;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A21, A22, A26, Th14; ::_thesis: verum
end;
A27: now__::_thesis:_(_p2_in_LSeg_(r,p)_&_r_in_left_cell_(f,i,(GoB_f))_implies_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_r_in_C_&_p2_in_C_)_)
assume that
A28: p2 in LSeg (r,p) and
A29: r in left_cell (f,i,(GoB f)) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
 LSeg (r,p) c= left_cell (f,i,(GoB f)) by A11, A23, A20, A29, JORDAN1:def_1;
then  p2 in (left_cell (f,i,(GoB f))) \ (L~ f) by A5, A28, XBOOLE_0:def_5;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A21, A22, A29, Th14; ::_thesis: verum
end;
A30: now__::_thesis:_(_p2_in_LSeg_(r,p)_&_r_in_right_cell_(f,i,(GoB_f))_implies_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_f)_`_&_r_in_C_&_p2_in_C_)_)
assume that
A31: p2 in LSeg (r,p) and
A32: r in right_cell (f,i,(GoB f)) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
 LSeg (r,p) c= right_cell (f,i,(GoB f)) by A11, A16, A12, A32, JORDAN1:def_1;
then  p2 in (right_cell (f,i,(GoB f))) \ (L~ f) by A5, A31, XBOOLE_0:def_5;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A14, A15, A32, Th14; ::_thesis: verum
end;
A33: ( p <> p2 & p <> p1 ) by A4, A5, A1, XBOOLE_0:def_4;
percases ( p1 in LSeg (r,p) or p2 in LSeg (r,p) ) by A3, A6, A33, A2, Th28;
supposeA34: p1 in LSeg (r,p) ; ::_thesis: ( 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 ) )
now__::_thesis:_(_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_)_)
percases ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) by A10;
suppose r in right_cell (f,i,(GoB f)) ; ::_thesis: ( 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 ) )
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 A17, A34; ::_thesis: verum
end;
suppose r in left_cell (f,i,(GoB f)) ; ::_thesis: ( 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 ) )
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 A24, A34; ::_thesis: verum
end;
end;
end;
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 ) ) ; ::_thesis: verum
end;
supposeA35: p2 in LSeg (r,p) ; ::_thesis: ( 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 ) )
now__::_thesis:_(_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_)_)
percases ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) by A10;
suppose r in right_cell (f,i,(GoB f)) ; ::_thesis: ( 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 ) )
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 A30, A35; ::_thesis: verum
end;
suppose r in left_cell (f,i,(GoB f)) ; ::_thesis: ( 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 ) )
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 A27, A35; ::_thesis: verum
end;
end;
end;
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 ) ) ; ::_thesis: verum
end;
end;
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 Element of 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
let f be non constant standard special_circular_sequence; ::_thesis: 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 Element of 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 )
let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( (L~ f) /\ (LSeg (p1,p2)) = {p} implies 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 Element of 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 ) )
assume A1: (L~ f) /\ (LSeg (p1,p2)) = {p} ; ::_thesis: 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 Element of 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 )
let rl, rp be Point of (TOP-REAL 2); ::_thesis: ( 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 Element of 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 implies 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 ) )
assume that
A2: ( not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) ) and
A3: ex i being Element of 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) ) and
A4: not rl in L~ f and
A5: not rp in L~ f ; ::_thesis: 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 )
consider i being Element of NAT  such that
A6: ( 1 <= i & i + 1 <= len f ) and
A7: rl in left_cell (f,i,(GoB f)) and
A8: rp in right_cell (f,i,(GoB f)) by A3;
A9: f is_sequence_on GoB f by GOBOARD5:def_5;
then A10: (left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f by A6, JORDAN9:27;
A11: (right_cell (f,i,(GoB f))) \ (L~ f) c= RightComp f by A9, A6, JORDAN9:27;
 rp in (right_cell (f,i,(GoB f))) \ (L~ f) by A5, A8, XBOOLE_0:def_5;
then A12: not rp in LeftComp f by A11, GOBRD14:18;
A13: now__::_thesis:_(_rp_in_LSeg_(p1,p2)_or_p1_in_RightComp_f_or_p2_in_RightComp_f_)
assume A14: not rp in LSeg (p1,p2) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
percases ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A2, A3, A5, A14, Th30;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
hence  ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; ::_thesis: verum
end;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
hence  ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; ::_thesis: verum
end;
end;
end;
 rl in (left_cell (f,i,(GoB f))) \ (L~ f) by A4, A7, XBOOLE_0:def_5;
then A15: not rl in RightComp f by A10, GOBRD14:17;
A16: now__::_thesis:_(_rl_in_LSeg_(p1,p2)_or_p1_in_LeftComp_f_or_p2_in_LeftComp_f_)
assume A17: not rl in LSeg (p1,p2) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
percases ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A2, A3, A4, A17, Th30;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence  ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; ::_thesis: verum
end;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence  ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; ::_thesis: verum
end;
end;
end;
A18: now__::_thesis:_(_not_rl_in_LSeg_(p1,p2)_&_not_rp_in_LSeg_(p1,p2)_implies_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_)_)
assume that
A19: not rl in LSeg (p1,p2) and
A20: not rp in LSeg (p1,p2) ; ::_thesis: 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 )
percases ( p1 in LeftComp f or p2 in LeftComp f ) by A16, A19;
supposeA21: p1 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A13, A20;
suppose p1 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A21, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A21, Th15; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA22: p2 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A13, A20;
suppose p1 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A22, Th15; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A22, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
end;
A23: now__::_thesis:_(_not_rp_in_LSeg_(p1,p2)_or_p1_in_RightComp_f_or_p2_in_RightComp_f_)
assume A24: rp in LSeg (p1,p2) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
percases ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A5, A24, Lm5;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
hence  ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; ::_thesis: verum
end;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; ::_thesis: ( p1 in RightComp f or p2 in RightComp f )
hence  ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; ::_thesis: verum
end;
end;
end;
A25: now__::_thesis:_(_not_rl_in_LSeg_(p1,p2)_&_rp_in_LSeg_(p1,p2)_implies_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_)_)
assume that
A26: not rl in LSeg (p1,p2) and
A27: rp in LSeg (p1,p2) ; ::_thesis: 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 )
percases ( p1 in LeftComp f or p2 in LeftComp f ) by A16, A26;
supposeA28: p1 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A23, A27;
suppose p1 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A28, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A28, Th15; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA29: p2 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A23, A27;
suppose p1 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A29, Th15; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A29, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
end;
A30: now__::_thesis:_(_not_rl_in_LSeg_(p1,p2)_or_p1_in_LeftComp_f_or_p2_in_LeftComp_f_)
assume A31: rl in LSeg (p1,p2) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
percases ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A4, A31, Lm5;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence  ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; ::_thesis: verum
end;
suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; ::_thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence  ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; ::_thesis: verum
end;
end;
end;
A32: now__::_thesis:_(_rl_in_LSeg_(p1,p2)_&_rp_in_LSeg_(p1,p2)_implies_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_)_)
assume that
A33: rl in LSeg (p1,p2) and
A34: rp in LSeg (p1,p2) ; ::_thesis: 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 )
percases ( p1 in LeftComp f or p2 in LeftComp f ) by A30, A33;
supposeA35: p1 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A23, A34;
suppose p1 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A35, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A35, Th15; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA36: p2 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A23, A34;
suppose p1 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A36, Th15; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A36, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
end;
A37: now__::_thesis:_(_rl_in_LSeg_(p1,p2)_&_not_rp_in_LSeg_(p1,p2)_implies_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_)_)
assume that
A38: rl in LSeg (p1,p2) and
A39: not rp in LSeg (p1,p2) ; ::_thesis: 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 )
percases ( p1 in LeftComp f or p2 in LeftComp f ) by A30, A38;
supposeA40: p1 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A13, A39;
suppose p1 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A40, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A40, Th15; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA41: p2 in LeftComp f ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( p1 in RightComp f or p2 in RightComp f ) by A13, A39;
suppose p1 in RightComp f ; ::_thesis: 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 )
hence  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 ) by A41, Th15; ::_thesis: verum
end;
suppose p2 in RightComp f ; ::_thesis: 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 )
then  LeftComp f meets RightComp f by A41, XBOOLE_0:3;
hence  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 ) by GOBRD14:14; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
end;
percases ( rl in LSeg (p1,p2) or not rl in LSeg (p1,p2) ) ;
supposeA42: rl in LSeg (p1,p2) ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( rp in LSeg (p1,p2) or not rp in LSeg (p1,p2) ) ;
suppose rp in LSeg (p1,p2) ; ::_thesis: 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 )
hence  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 ) by A32, A42; ::_thesis: verum
end;
suppose not rp in LSeg (p1,p2) ; ::_thesis: 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 )
hence  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 ) by A37, A42; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA43: not rl in LSeg (p1,p2) ; ::_thesis: 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 )
now__::_thesis:_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_)
percases ( rp in LSeg (p1,p2) or not rp in LSeg (p1,p2) ) ;
suppose rp in LSeg (p1,p2) ; ::_thesis: 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 )
hence  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 ) by A25, A43; ::_thesis: verum
end;
suppose not rp in LSeg (p1,p2) ; ::_thesis: 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 )
hence  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 ) by A18, A43; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
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 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 )
let f be non constant standard special_circular_sequence; ::_thesis: 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 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( (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) implies 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 ) )
assume that
A1: (L~ f) /\ (LSeg (p1,p2)) = {p} and
A2: ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) ; ::_thesis: ( p1 in L~ f or p2 in L~ f or not rng f misses LSeg (p1,p2) or 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 ) )
A3: p in {p} by TARSKI:def_1;
then A4: p in LSeg (p1,p2) by A1, XBOOLE_0:def_4;
A5: p in LSeg (p2,p1) by A1, A3, XBOOLE_0:def_4;
 p in L~ f by A1, A3, XBOOLE_0:def_4;
then consider LS being set  such that
A6: ( p in LS & LS in  {  (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f )  }  ) by TARSKI:def_4;
set G = GoB f;
assume that
A7: ( not p1 in L~ f & not p2 in L~ f ) and
A8: rng f misses LSeg (p1,p2) ; ::_thesis: 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 )
consider k being Element of NAT  such that
A9: LS = LSeg (f,k) and
A10: 1 <= k and
A11: k + 1 <= len f by A6;
A12: f is_sequence_on GoB f by GOBOARD5:def_5;
then consider i1, j1, i2, j2 being Element of NAT  such that
A13: [i1,j1] in Indices (GoB f) and
A14: f /. k = (GoB f) * (i1,j1) and
A15: [i2,j2] in Indices (GoB f) and
A16: f /. (k + 1) = (GoB f) * (i2,j2) and
A17: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3;
A18: 1 <= i1 by A13, MATRIX_1:38;
 1 <= k + 1 by A10, NAT_1:13;
then A19: k + 1 in dom f by A11, FINSEQ_3:25;
then  f . (k + 1) in rng f by FUNCT_1:3;
then  f /. (k + 1) in rng f by A19, PARTFUN1:def_6;
then A20: p <> f /. (k + 1) by A8, A4, XBOOLE_0:3;
A21: i2 <= len (GoB f) by A15, MATRIX_1:38;
then A22: ( i2 = i1 + 1 implies i1 < len (GoB f) ) by NAT_1:13;
then A23: ( j1 = width (GoB f) & i2 = i1 + 1 implies Int (cell ((GoB f),i1,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s )  }  ) by A18, GOBOARD6:25;
A24: 1 <= j1 by A13, MATRIX_1:38;
then A25: ( j1 < width (GoB f) & i2 = i1 + 1 implies Int (cell ((GoB f),i1,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  ) by A18, A22, GOBOARD6:26;
A26: j2 <= width (GoB f) by A15, MATRIX_1:38;
then A27: ( j2 = j1 + 1 implies j1 < width (GoB f) ) by NAT_1:13;
then A28: ( i1 = len (GoB f) & j2 = j1 + 1 implies Int (cell ((GoB f),i1,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  ) by A24, GOBOARD6:23;
A29: 1 <= j2 by A15, MATRIX_1:38;
A30: j1 <= width (GoB f) by A13, MATRIX_1:38;
then A31: ( j1 = j2 + 1 implies j2 < width (GoB f) ) by NAT_1:13;
then A32: ( i2 = len (GoB f) & j1 = j2 + 1 implies Int (cell ((GoB f),i2,j2)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }  ) by A29, GOBOARD6:23;
A33: 1 <= i2 by A15, MATRIX_1:38;
then A34: ( i2 < len (GoB f) & j1 = j2 + 1 implies Int (cell ((GoB f),i2,j2)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }  ) by A29, A31, GOBOARD6:26;
A35: i1 <= len (GoB f) by A13, MATRIX_1:38;
then A36: ( i1 = i2 + 1 implies i2 < len (GoB f) ) by NAT_1:13;
then A37: ( j1 = width (GoB f) & i1 = i2 + 1 implies Int (cell ((GoB f),i2,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s )  }  ) by A33, GOBOARD6:25;
 k < len f by A11, NAT_1:13;
then A38: k in dom f by A10, FINSEQ_3:25;
then  f . k in rng f by FUNCT_1:3;
then  f /. k in rng f by A38, PARTFUN1:def_6;
then A39: p <> f /. k by A8, A4, XBOOLE_0:3;
A40: j1 -' 1 < j1 by A24, JORDAN5B:1;
A41: now__::_thesis:_(_1_<_j1_&_i2_=_i1_+_1_implies_Int_(cell_((GoB_f),i1,(j1_-'_1)))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_(i1,1))_`1_<_r_&_r_<_((GoB_f)_*_((i1_+_1),1))_`1_&_((GoB_f)_*_(1,(j1_-'_1)))_`2_<_s_&_s_<_((GoB_f)_*_(1,((j1_-'_1)_+_1)))_`2_)__}__)
assume  ( 1 < j1 & i2 = i1 + 1 ) ; ::_thesis: Int (cell ((GoB f),i1,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )  }
then A42: ( i1 < len (GoB f) & 1 <= j1 -' 1 ) by A21, NAT_1:13, NAT_D:49;
 ( 1 <= i1 & j1 -' 1 < width (GoB f) ) by A13, A30, A40, MATRIX_1:38, XXREAL_0:2;
hence  Int (cell ((GoB f),i1,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )  }  by A42, GOBOARD6:26; ::_thesis: verum
end;
A43: ( j1 < width (GoB f) & i1 = i2 + 1 implies Int (cell ((GoB f),i2,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  ) by A33, A24, A36, GOBOARD6:26;
A44: now__::_thesis:_(_1_<_j1_&_i1_=_i2_+_1_implies_Int_(cell_((GoB_f),i2,(j1_-'_1)))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_(i2,1))_`1_<_r_&_r_<_((GoB_f)_*_((i2_+_1),1))_`1_&_((GoB_f)_*_(1,(j1_-'_1)))_`2_<_s_&_s_<_((GoB_f)_*_(1,((j1_-'_1)_+_1)))_`2_)__}__)
assume  ( 1 < j1 & i1 = i2 + 1 ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )  }
then A45: ( i2 < len (GoB f) & 1 <= j1 -' 1 ) by A35, NAT_1:13, NAT_D:49;
 ( 1 <= i2 & j1 -' 1 < width (GoB f) ) by A15, A30, A40, MATRIX_1:38, XXREAL_0:2;
hence  Int (cell ((GoB f),i2,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )  }  by A45, GOBOARD6:26; ::_thesis: verum
end;
A46: now__::_thesis:_(_1_=_j1_&_i1_=_i2_+_1_implies_Int_(cell_((GoB_f),i2,(j1_-'_1)))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_(i2,1))_`1_<_r_&_r_<_((GoB_f)_*_((i2_+_1),1))_`1_&_s_<_((GoB_f)_*_(1,1))_`2_)__}__)
assume that
A47: 1 = j1 and
A48: i1 = i2 + 1 ; ::_thesis: Int (cell ((GoB f),i2,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 )  }
 Int (cell ((GoB f),i2,0)) = Int (cell ((GoB f),i2,(j1 -' 1))) by A47, NAT_2:8;
hence  Int (cell ((GoB f),i2,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 )  }  by A33, A36, A48, GOBOARD6:24; ::_thesis: verum
end;
A49: ( j1 = j2 & i2 = i1 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,j1)) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,(j1 -' 1))) ) ) by A12, A10, A11, A13, A14, A15, A16, GOBRD13:23, GOBRD13:24;
A50: p in LSeg ((f /. (k + 1)),(f /. k)) by A6, A9, A10, A11, TOPREAL1:def_3;
A51: now__::_thesis:_(_i1_=_i2_&_j1_=_j2_+_1_implies_(_((GoB_f)_*_(1,j2))_`2_<_p_`2_&_p_`2_<_((GoB_f)_*_(1,(j2_+_1)))_`2_)_)
assume that
A52: i1 = i2 and
A53: j1 = j2 + 1 ; ::_thesis: ( ((GoB f) * (1,j2)) `2 < p `2 & p `2 < ((GoB f) * (1,(j2 + 1))) `2 )
 j2 < j1 by A53, NAT_1:13;
then  (f /. (k + 1)) `2 < (f /. k) `2 by A14, A16, A35, A18, A30, A29, A52, GOBOARD5:4;
then A54: ( (f /. (k + 1)) `2 < p `2 & p `2 < (f /. k) `2 ) by A39, A50, A20, TOPREAL6:30;
 ( 1 <= j2 + 1 & j2 + 1 <= width (GoB f) ) by A13, A53, MATRIX_1:38;
hence  ( ((GoB f) * (1,j2)) `2 < p `2 & p `2 < ((GoB f) * (1,(j2 + 1))) `2 ) by A14, A16, A35, A18, A26, A29, A52, A53, A54, GOBOARD5:1; ::_thesis: verum
end;
A55: now__::_thesis:_(_i1_=_i2_&_j2_=_j1_+_1_implies_(_((GoB_f)_*_(1,j1))_`2_<_p_`2_&_p_`2_<_((GoB_f)_*_(1,(j1_+_1)))_`2_)_)
assume that
A56: i1 = i2 and
A57: j2 = j1 + 1 ; ::_thesis: ( ((GoB f) * (1,j1)) `2 < p `2 & p `2 < ((GoB f) * (1,(j1 + 1))) `2 )
 j1 < j2 by A57, NAT_1:13;
then  (f /. k) `2 < (f /. (k + 1)) `2 by A14, A16, A35, A18, A24, A26, A56, GOBOARD5:4;
then  ( (f /. k) `2 < p `2 & p `2 < (f /. (k + 1)) `2 ) by A39, A50, A20, TOPREAL6:30;
hence  ( ((GoB f) * (1,j1)) `2 < p `2 & p `2 < ((GoB f) * (1,(j1 + 1))) `2 ) by A14, A16, A33, A35, A24, A30, A26, A29, A56, A57, GOBOARD5:1; ::_thesis: verum
end;
A58: now__::_thesis:_(_1_=_i2_&_j1_=_j2_+_1_implies_Int_(cell_((GoB_f),(i2_-'_1),j2))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_r_<_((GoB_f)_*_(1,1))_`1_&_((GoB_f)_*_(1,j2))_`2_<_s_&_s_<_((GoB_f)_*_(1,(j2_+_1)))_`2_)__}__)
assume that
A59: 1 = i2 and
A60: j1 = j2 + 1 ; ::_thesis: Int (cell ((GoB f),(i2 -' 1),j2)) =  {  |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }
 Int (cell ((GoB f),(i2 -' 1),j2)) = Int (cell ((GoB f),0,j2)) by A59, NAT_2:8;
hence  Int (cell ((GoB f),(i2 -' 1),j2)) =  {  |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }  by A29, A31, A60, GOBOARD6:20; ::_thesis: verum
end;
 (LSeg (p1,p2)) /\ (LSeg (f,k)) = {p} by A1, A6, A9, TOPREAL3:19, ZFMISC_1:124;
then A61: (LSeg (p1,p2)) /\ (LSeg ((f /. k),(f /. (k + 1)))) = {p} by A10, A11, TOPREAL1:def_3;
A62: ( i1 < len (GoB f) & j2 = j1 + 1 implies Int (cell ((GoB f),i1,j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  ) by A18, A24, A27, GOBOARD6:26;
A63: now__::_thesis:_(_1_=_i1_&_j2_=_j1_+_1_implies_Int_(cell_((GoB_f),(i1_-'_1),j1))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_r_<_((GoB_f)_*_(1,1))_`1_&_((GoB_f)_*_(1,j1))_`2_<_s_&_s_<_((GoB_f)_*_(1,(j1_+_1)))_`2_)__}__)
assume that
A64: 1 = i1 and
A65: j2 = j1 + 1 ; ::_thesis: Int (cell ((GoB f),(i1 -' 1),j1)) =  {  |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }
 Int (cell ((GoB f),(i1 -' 1),j1)) = Int (cell ((GoB f),0,j1)) by A64, NAT_2:8;
hence  Int (cell ((GoB f),(i1 -' 1),j1)) =  {  |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  by A24, A27, A65, GOBOARD6:20; ::_thesis: verum
end;
A66: ( i1 = i2 & j1 = j2 + 1 implies ( Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),(i2 -' 1),j2)) & Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,j2)) ) ) by A12, A10, A11, A13, A14, A15, A16, GOBRD13:27, GOBRD13:28;
A67: now__::_thesis:_for_r_being_Point_of_(TOP-REAL_2)_st_r_in_Int_(left_cell_(f,k,(GoB_f)))_holds_
(_r_in_left_cell_(f,k,(GoB_f))_&_not_r_in_L~_f_)
let r be Point of (TOP-REAL 2); ::_thesis: ( r in Int (left_cell (f,k,(GoB f))) implies ( r in left_cell (f,k,(GoB f)) & not r in L~ f ) )
assume A68: r in Int (left_cell (f,k,(GoB f))) ; ::_thesis: ( r in left_cell (f,k,(GoB f)) & not r in L~ f )
 Int (left_cell (f,k,(GoB f))) c= left_cell (f,k,(GoB f)) by TOPS_1:16;
hence  r in left_cell (f,k,(GoB f)) by A68; ::_thesis: not r in L~ f
 Int (left_cell (f,k,(GoB f))) misses L~ f by A12, A10, A11, JORDAN9:15;
hence  not r in L~ f by A68, XBOOLE_0:3; ::_thesis: verum
end;
A69: now__::_thesis:_for_r_being_Point_of_(TOP-REAL_2)_st_r_in_Int_(right_cell_(f,k,(GoB_f)))_holds_
(_r_in_right_cell_(f,k,(GoB_f))_&_not_r_in_L~_f_)
let r be Point of (TOP-REAL 2); ::_thesis: ( r in Int (right_cell (f,k,(GoB f))) implies ( r in right_cell (f,k,(GoB f)) & not r in L~ f ) )
assume A70: r in Int (right_cell (f,k,(GoB f))) ; ::_thesis: ( r in right_cell (f,k,(GoB f)) & not r in L~ f )
 Int (right_cell (f,k,(GoB f))) c= right_cell (f,k,(GoB f)) by TOPS_1:16;
hence  r in right_cell (f,k,(GoB f)) by A70; ::_thesis: not r in L~ f
 Int (right_cell (f,k,(GoB f))) misses L~ f by A12, A10, A11, JORDAN9:15;
hence  not r in L~ f by A70, XBOOLE_0:3; ::_thesis: verum
end;
A71: now__::_thesis:_(_1_=_j1_&_i2_=_i1_+_1_implies_Int_(cell_((GoB_f),i1,(j1_-'_1)))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_(i1,1))_`1_<_r_&_r_<_((GoB_f)_*_((i1_+_1),1))_`1_&_s_<_((GoB_f)_*_(1,1))_`2_)__}__)
assume that
A72: 1 = j1 and
A73: i2 = i1 + 1 ; ::_thesis: Int (cell ((GoB f),i1,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 )  }
 Int (cell ((GoB f),i1,0)) = Int (cell ((GoB f),i1,(j1 -' 1))) by A72, NAT_2:8;
hence  Int (cell ((GoB f),i1,(j1 -' 1))) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 )  }  by A18, A22, A73, GOBOARD6:24; ::_thesis: verum
end;
 ( LSeg (f,k) is vertical or LSeg (f,k) is horizontal ) by SPPOL_1:19;
then  ( LSeg ((f /. k),(f /. (k + 1))) is vertical or LSeg ((f /. k),(f /. (k + 1))) is horizontal ) by A10, A11, TOPREAL1:def_3;
then A74: ( (f /. k) `1 = (f /. (k + 1)) `1 or (f /. k) `2 = (f /. (k + 1)) `2 ) by SPPOL_1:15, SPPOL_1:16;
A75: now__::_thesis:_(_j1_=_j2_&_i2_=_i1_+_1_implies_(_((GoB_f)_*_(i1,1))_`1_<_p_`1_&_p_`1_<_((GoB_f)_*_((i1_+_1),1))_`1_)_)
assume that
A76: j1 = j2 and
A77: i2 = i1 + 1 ; ::_thesis: ( ((GoB f) * (i1,1)) `1 < p `1 & p `1 < ((GoB f) * ((i1 + 1),1)) `1 )
 i1 < i2 by A77, NAT_1:13;
then  (f /. k) `1 < (f /. (k + 1)) `1 by A14, A16, A21, A18, A26, A29, A76, GOBOARD5:3;
then  ( (f /. k) `1 < p `1 & p `1 < (f /. (k + 1)) `1 ) by A39, A50, A20, TOPREAL6:29;
hence  ( ((GoB f) * (i1,1)) `1 < p `1 & p `1 < ((GoB f) * ((i1 + 1),1)) `1 ) by A14, A16, A21, A33, A35, A18, A30, A29, A76, A77, GOBOARD5:2; ::_thesis: verum
end;
A78: i2 -' 1 < i2 by A33, JORDAN5B:1;
A79: now__::_thesis:_(_1_<_i2_&_j1_=_j2_+_1_implies_Int_(cell_((GoB_f),(i2_-'_1),j2))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_((i2_-'_1),1))_`1_<_r_&_r_<_((GoB_f)_*_(((i2_-'_1)_+_1),1))_`1_&_((GoB_f)_*_(1,j2))_`2_<_s_&_s_<_((GoB_f)_*_(1,(j2_+_1)))_`2_)__}__)
assume  ( 1 < i2 & j1 = j2 + 1 ) ; ::_thesis: Int (cell ((GoB f),(i2 -' 1),j2)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }
then A80: ( 1 <= i2 -' 1 & j2 < width (GoB f) ) by A30, NAT_1:13, NAT_D:49;
 ( i2 -' 1 < len (GoB f) & 1 <= j2 ) by A15, A21, A78, MATRIX_1:38, XXREAL_0:2;
hence  Int (cell ((GoB f),(i2 -' 1),j2)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 )  }  by A80, GOBOARD6:26; ::_thesis: verum
end;
A81: ( j1 = j2 & i1 = i2 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,(j1 -' 1))) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,j1)) ) ) by A12, A10, A11, A13, A14, A15, A16, GOBRD13:25, GOBRD13:26;
A82: now__::_thesis:_(_j1_=_j2_&_i1_=_i2_+_1_implies_(_((GoB_f)_*_(i2,1))_`1_<_p_`1_&_p_`1_<_((GoB_f)_*_((i2_+_1),1))_`1_)_)
assume that
A83: j1 = j2 and
A84: i1 = i2 + 1 ; ::_thesis: ( ((GoB f) * (i2,1)) `1 < p `1 & p `1 < ((GoB f) * ((i2 + 1),1)) `1 )
 i2 < i1 by A84, NAT_1:13;
then  ((GoB f) * (i2,j1)) `1 < ((GoB f) * (i1,j1)) `1 by A33, A35, A24, A30, GOBOARD5:3;
then  ( (f /. (k + 1)) `1 < p `1 & p `1 < (f /. k) `1 ) by A14, A16, A39, A50, A20, A83, TOPREAL6:29;
hence  ( ((GoB f) * (i2,1)) `1 < p `1 & p `1 < ((GoB f) * ((i2 + 1),1)) `1 ) by A14, A16, A21, A33, A35, A18, A26, A29, A83, A84, GOBOARD5:2; ::_thesis: verum
end;
A85: i1 -' 1 < i1 by A18, JORDAN5B:1;
A86: now__::_thesis:_(_1_<_i1_&_j2_=_j1_+_1_implies_Int_(cell_((GoB_f),(i1_-'_1),j1))_=__{__|[r,s]|_where_r,_s_is_Real_:_(_((GoB_f)_*_((i1_-'_1),1))_`1_<_r_&_r_<_((GoB_f)_*_(((i1_-'_1)_+_1),1))_`1_&_((GoB_f)_*_(1,j1))_`2_<_s_&_s_<_((GoB_f)_*_(1,(j1_+_1)))_`2_)__}__)
assume  ( 1 < i1 & j2 = j1 + 1 ) ; ::_thesis: Int (cell ((GoB f),(i1 -' 1),j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }
then A87: ( 1 <= i1 -' 1 & j1 < width (GoB f) ) by A26, NAT_1:13, NAT_D:49;
 ( i1 -' 1 < len (GoB f) & 1 <= j1 ) by A13, A35, A85, MATRIX_1:38, XXREAL_0:2;
hence  Int (cell ((GoB f),(i1 -' 1),j1)) =  {  |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 )  }  by A87, GOBOARD6:26; ::_thesis: verum
end;
A88: ( i1 = i2 & j2 = j1 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),(i1 -' 1),j1)) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,j1)) ) ) by A12, A10, A11, A13, A14, A15, A16, GOBRD13:21, GOBRD13:22;
A89: ( p <> p1 & p <> p2 ) by A1, A7, A3, XBOOLE_0:def_4;
then A90: ( p1 `2 = p2 `2 implies i1 = i2 ) by A13, A14, A15, A16, A74, A61, A39, Th29, JORDAN1G:7;
A91: ( p1 `1 = p2 `1 implies j1 = j2 ) by A13, A14, A15, A16, A74, A61, A89, A39, Th29, JORDAN1G:6;
percases ( p1 `2 = p2 `2 or p1 `1 = p2 `1 ) by A2;
supposeA92: p1 `2 = p2 `2 ; ::_thesis: 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 )
 Int (right_cell (f,k,(GoB f))) <> {} by A12, A10, A11, JORDAN9:9;
then consider rp9 being set  such that
A93: rp9 in Int (right_cell (f,k,(GoB f))) by XBOOLE_0:def_1;
reconsider rp9 = rp9 as Point of (TOP-REAL 2) by A93;
reconsider rp = |[(rp9 `1),(p `2)]| as Point of (TOP-REAL 2) ;
A94: p `2 = p1 `2 by A5, A92, GOBOARD7:6;
A95: now__::_thesis:_(_j1_=_j2_+_1_&_1_<_i2_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A96: ( j1 = j2 + 1 & 1 < i2 ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A79, A92, A93, Th29, JORDAN1G:7;
then  ( ((GoB f) * ((i2 -' 1),1)) `1 < rp9 `1 & rp9 `1 < ((GoB f) * (((i2 -' 1) + 1),1)) `1 ) by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A79, A92, A96, Th29, JORDAN1G:7; ::_thesis: verum
end;
A97: now__::_thesis:_(_j1_=_j2_+_1_&_1_=_i2_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A98: ( j1 = j2 + 1 & 1 = i2 ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A58, A92, A93, Th29, JORDAN1G:7;
then  rp9 `1 < ((GoB f) * (1,1)) `1 by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A58, A92, A98, Th29, JORDAN1G:7; ::_thesis: verum
end;
 Int (left_cell (f,k,(GoB f))) <> {} by A12, A10, A11, JORDAN9:9;
then consider rl9 being set  such that
A99: rl9 in Int (left_cell (f,k,(GoB f))) by XBOOLE_0:def_1;
reconsider rl9 = rl9 as Point of (TOP-REAL 2) by A99;
reconsider rl = |[(rl9 `1),(p `2)]| as Point of (TOP-REAL 2) ;
A100: ( rl `2 = p `2 & rp `2 = p `2 ) by EUCLID:52;
A101: now__::_thesis:_(_j2_=_j1_+_1_&_1_<_i1_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A102: ( j2 = j1 + 1 & 1 < i1 ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A86, A92, A99, Th29, JORDAN1G:7;
then  ( ((GoB f) * ((i1 -' 1),1)) `1 < rl9 `1 & rl9 `1 < ((GoB f) * (((i1 -' 1) + 1),1)) `1 ) by EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A86, A92, A102, Th29, JORDAN1G:7; ::_thesis: verum
end;
A103: now__::_thesis:_(_j2_=_j1_+_1_&_1_=_i1_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A104: ( j2 = j1 + 1 & 1 = i1 ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A63, A92, A99, Th29, JORDAN1G:7;
then  rl9 `1 < ((GoB f) * (1,1)) `1 by EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A63, A92, A104, Th29, JORDAN1G:7; ::_thesis: verum
end;
A105: rl `1 = rl9 `1 by EUCLID:52;
A106: now__::_thesis:_(_j1_=_j2_+_1_&_i2_=_len_(GoB_f)_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A107: ( j1 = j2 + 1 & i2 = len (GoB f) ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A32, A92, A99, Th29, JORDAN1G:7;
then  ((GoB f) * ((len (GoB f)),1)) `1 < rl `1 by A105, EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A32, A92, A105, A107, Th29, JORDAN1G:7; ::_thesis: verum
end;
A108: now__::_thesis:_(_j2_=_j1_+_1_&_i1_=_len_(GoB_f)_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A109: ( j2 = j1 + 1 & i1 = len (GoB f) ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A28, A92, A93, Th29, JORDAN1G:7;
then  ((GoB f) * ((len (GoB f)),1)) `1 < rp9 `1 by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A28, A92, A109, Th29, JORDAN1G:7; ::_thesis: verum
end;
A110: now__::_thesis:_(_j2_=_j1_+_1_&_i1_<_len_(GoB_f)_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A111: ( j2 = j1 + 1 & i1 < len (GoB f) ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A62, A92, A93, Th29, JORDAN1G:7;
then  ( ((GoB f) * (i1,1)) `1 < rp9 `1 & rp9 `1 < ((GoB f) * ((i1 + 1),1)) `1 ) by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A62, A92, A111, Th29, JORDAN1G:7; ::_thesis: verum
end;
A112: now__::_thesis:_(_j1_=_j2_+_1_&_i2_<_len_(GoB_f)_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A113: ( j1 = j2 + 1 & i2 < len (GoB f) ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A34, A92, A99, Th29, JORDAN1G:7;
then  ( ((GoB f) * (i2,1)) `1 < rl `1 & rl `1 < ((GoB f) * ((i2 + 1),1)) `1 ) by A105, EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A34, A92, A105, A113, Th29, JORDAN1G:7; ::_thesis: verum
end;
now__::_thesis:_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_)
percases ( j1 = j2 + 1 or j2 = j1 + 1 ) by A17, A90, A92;
supposeA114: j1 = j2 + 1 ; ::_thesis: 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 )
 rp in Int (right_cell (f,k,(GoB f)))
proof
percases ( 1 < i2 or 1 = i2 ) by A33, XXREAL_0:1;
suppose 1 < i2 ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A95, A114; ::_thesis: verum
end;
suppose 1 = i2 ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A97, A114; ::_thesis: verum
end;
end;
end;
then A115: ( rp in right_cell (f,k,(GoB f)) & not rp in L~ f ) by A69;
 rl in Int (left_cell (f,k,(GoB f)))
proof
percases ( i2 < len (GoB f) or i2 = len (GoB f) ) by A21, XXREAL_0:1;
suppose i2 < len (GoB f) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A112, A114; ::_thesis: verum
end;
suppose i2 = len (GoB f) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A106, A114; ::_thesis: verum
end;
end;
end;
then  ( rl in left_cell (f,k,(GoB f)) & not rl in L~ f ) by A67;
hence  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 ) by A1, A7, A6, A9, A10, A11, A92, A94, A100, A115, Th31; ::_thesis: verum
end;
supposeA116: j2 = j1 + 1 ; ::_thesis: 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 )
 rp in Int (right_cell (f,k,(GoB f)))
proof
percases ( i1 < len (GoB f) or i1 = len (GoB f) ) by A35, XXREAL_0:1;
suppose i1 < len (GoB f) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A110, A116; ::_thesis: verum
end;
suppose i1 = len (GoB f) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A108, A116; ::_thesis: verum
end;
end;
end;
then A117: ( rp in right_cell (f,k,(GoB f)) & not rp in L~ f ) by A69;
 rl in Int (left_cell (f,k,(GoB f)))
proof
percases ( 1 < i1 or 1 = i1 ) by A18, XXREAL_0:1;
suppose 1 < i1 ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A101, A116; ::_thesis: verum
end;
suppose 1 = i1 ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A103, A116; ::_thesis: verum
end;
end;
end;
then  ( rl in left_cell (f,k,(GoB f)) & not rl in L~ f ) by A67;
hence  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 ) by A1, A7, A6, A9, A10, A11, A92, A94, A100, A117, Th31; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
supposeA118: p1 `1 = p2 `1 ; ::_thesis: 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 )
 Int (left_cell (f,k,(GoB f))) <> {} by A12, A10, A11, JORDAN9:9;
then consider rl9 being set  such that
A119: rl9 in Int (left_cell (f,k,(GoB f))) by XBOOLE_0:def_1;
reconsider rl9 = rl9 as Point of (TOP-REAL 2) by A119;
reconsider rl = |[(p `1),(rl9 `2)]| as Point of (TOP-REAL 2) ;
A120: p `1 = p1 `1 by A5, A118, GOBOARD7:5;
A121: rl `2 = rl9 `2 by EUCLID:52;
A122: now__::_thesis:_(_i1_=_i2_+_1_&_1_=_j1_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A123: ( i1 = i2 + 1 & 1 = j1 ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A81, A46, A118, A119, Th29, JORDAN1G:6;
then  rl `2 < ((GoB f) * (1,1)) `2 by A121, EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A46, A118, A121, A123, Th29, JORDAN1G:6; ::_thesis: verum
end;
A124: now__::_thesis:_(_i2_=_i1_+_1_&_j1_<_width_(GoB_f)_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A125: ( i2 = i1 + 1 & j1 < width (GoB f) ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A49, A25, A118, A119, Th29, JORDAN1G:6;
then  ( ((GoB f) * (1,j1)) `2 < rl `2 & rl `2 < ((GoB f) * (1,(j1 + 1))) `2 ) by A121, EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A25, A118, A121, A125, Th29, JORDAN1G:6; ::_thesis: verum
end;
 Int (right_cell (f,k,(GoB f))) <> {} by A12, A10, A11, JORDAN9:9;
then consider rp9 being set  such that
A126: rp9 in Int (right_cell (f,k,(GoB f))) by XBOOLE_0:def_1;
reconsider rp9 = rp9 as Point of (TOP-REAL 2) by A126;
reconsider rp = |[(p `1),(rp9 `2)]| as Point of (TOP-REAL 2) ;
A127: ( rl `1 = p `1 & rp `1 = p `1 ) by EUCLID:52;
A128: now__::_thesis:_(_i2_=_i1_+_1_&_1_<_j1_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A129: ( i2 = i1 + 1 & 1 < j1 ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A49, A41, A118, A126, Th29, JORDAN1G:6;
then  ( ((GoB f) * (1,(j1 -' 1))) `2 < rp9 `2 & rp9 `2 < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A41, A118, A129, Th29, JORDAN1G:6; ::_thesis: verum
end;
A130: now__::_thesis:_(_i2_=_i1_+_1_&_1_=_j1_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A131: ( i2 = i1 + 1 & 1 = j1 ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A49, A71, A118, A126, Th29, JORDAN1G:6;
then  rp9 `2 < ((GoB f) * (1,1)) `2 by EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A71, A118, A131, Th29, JORDAN1G:6; ::_thesis: verum
end;
A132: rp `2 = rp9 `2 by EUCLID:52;
A133: now__::_thesis:_(_i1_=_i2_+_1_&_j1_=_width_(GoB_f)_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A134: ( i1 = i2 + 1 & j1 = width (GoB f) ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s ) by A13, A14, A15, A16, A74, A61, A89, A39, A81, A37, A118, A126, Th29, JORDAN1G:6;
then  ((GoB f) * (1,(width (GoB f)))) `2 < rp `2 by A132, EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A37, A118, A132, A134, Th29, JORDAN1G:6; ::_thesis: verum
end;
A135: now__::_thesis:_(_i2_=_i1_+_1_&_j1_=_width_(GoB_f)_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A136: ( i2 = i1 + 1 & j1 = width (GoB f) ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s ) by A13, A14, A15, A16, A74, A61, A89, A39, A49, A23, A118, A119, Th29, JORDAN1G:6;
then  ((GoB f) * (1,(width (GoB f)))) `2 < rl9 `2 by EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A23, A118, A136, Th29, JORDAN1G:6; ::_thesis: verum
end;
A137: now__::_thesis:_(_i1_=_i2_+_1_&_1_<_j1_implies_rl_in_Int_(left_cell_(f,k,(GoB_f)))_)
assume A138: ( i1 = i2 + 1 & 1 < j1 ) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rl9 = |[r,s]| & ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A81, A44, A118, A119, Th29, JORDAN1G:6;
then  ( ((GoB f) * (1,(j1 -' 1))) `2 < rl9 `2 & rl9 `2 < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) by EUCLID:52;
hence  rl in Int (left_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A44, A118, A138, Th29, JORDAN1G:6; ::_thesis: verum
end;
A139: now__::_thesis:_(_i1_=_i2_+_1_&_j1_<_width_(GoB_f)_implies_rp_in_Int_(right_cell_(f,k,(GoB_f)))_)
assume A140: ( i1 = i2 + 1 & j1 < width (GoB f) ) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
then  ex r, s being Real st
( rp9 = |[r,s]| & ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A81, A43, A118, A126, Th29, JORDAN1G:6;
then  ( ((GoB f) * (1,j1)) `2 < rp `2 & rp `2 < ((GoB f) * (1,(j1 + 1))) `2 ) by A132, EUCLID:52;
hence  rp in Int (right_cell (f,k,(GoB f))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A43, A118, A132, A140, Th29, JORDAN1G:6; ::_thesis: verum
end;
now__::_thesis:_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_)
percases ( i1 = i2 + 1 or i2 = i1 + 1 ) by A17, A91, A118;
supposeA141: i1 = i2 + 1 ; ::_thesis: 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 )
 rp in Int (right_cell (f,k,(GoB f)))
proof
percases ( j1 < width (GoB f) or j1 = width (GoB f) ) by A30, XXREAL_0:1;
suppose j1 < width (GoB f) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A139, A141; ::_thesis: verum
end;
suppose j1 = width (GoB f) ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A133, A141; ::_thesis: verum
end;
end;
end;
then A142: ( rp in right_cell (f,k,(GoB f)) & not rp in L~ f ) by A69;
 rl in Int (left_cell (f,k,(GoB f)))
proof
percases ( 1 < j1 or 1 = j1 ) by A24, XXREAL_0:1;
suppose 1 < j1 ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A137, A141; ::_thesis: verum
end;
suppose 1 = j1 ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A122, A141; ::_thesis: verum
end;
end;
end;
then  ( rl in left_cell (f,k,(GoB f)) & not rl in L~ f ) by A67;
hence  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 ) by A1, A7, A6, A9, A10, A11, A118, A120, A127, A142, Th31; ::_thesis: verum
end;
supposeA143: i2 = i1 + 1 ; ::_thesis: 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 )
 rl in Int (left_cell (f,k,(GoB f)))
proof
percases ( j1 < width (GoB f) or j1 = width (GoB f) ) by A30, XXREAL_0:1;
suppose j1 < width (GoB f) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A124, A143; ::_thesis: verum
end;
suppose j1 = width (GoB f) ; ::_thesis: rl in Int (left_cell (f,k,(GoB f)))
hence  rl in Int (left_cell (f,k,(GoB f))) by A135, A143; ::_thesis: verum
end;
end;
end;
then A144: ( rl in left_cell (f,k,(GoB f)) & not rl in L~ f ) by A67;
 rp in Int (right_cell (f,k,(GoB f)))
proof
percases ( 1 < j1 or 1 = j1 ) by A24, XXREAL_0:1;
suppose 1 < j1 ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A128, A143; ::_thesis: verum
end;
suppose 1 = j1 ; ::_thesis: rp in Int (right_cell (f,k,(GoB f)))
hence  rp in Int (right_cell (f,k,(GoB f))) by A130, A143; ::_thesis: verum
end;
end;
end;
then  ( rp in right_cell (f,k,(GoB f)) & not rp in L~ f ) by A69;
hence  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 ) by A1, A7, A6, A9, A10, A11, A118, A120, A127, A144, Th31; ::_thesis: verum
end;
end;
end;
hence  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 ) ; ::_thesis: verum
end;
end;
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 Element of 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
let f be non constant standard special_circular_sequence; ::_thesis: for g being special FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds
for k being Element of 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 ) )
let g be special FinSequence of (TOP-REAL 2); ::_thesis: ( f,g are_in_general_position implies for k being Element of 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 ) ) )
assume A1: f,g are_in_general_position ; ::_thesis: for k being Element of 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 ) )
A2: g is_in_general_position_wrt f by A1, Def2;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len g implies ( 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 ) ) )
assume that
A3: 1 <= k and
A4: k + 1 <= len g ; ::_thesis: ( 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 ) )
A5: g . k in (L~ f) ` by A1, A3, A4, Th8;
then A6: not g . k in L~ f by XBOOLE_0:def_5;
A7: g . (k + 1) in (L~ f) ` by A1, A3, A4, Th8;
then A8: not g . (k + 1) in L~ f by XBOOLE_0:def_5;
A9: k < len g by A4, NAT_1:13;
then A10: k in dom g by A3, FINSEQ_3:25;
then A11: g /. k = g . k by PARTFUN1:def_6;
then A12: g . k in LSeg (g,k) by A3, A4, TOPREAL1:21;
set m = (L~ f) /\ (LSeg (g,k));
set p1 = g /. k;
set p2 = g /. (k + 1);
A13: LSeg (g,k) = LSeg ((g /. k),(g /. (k + 1))) by A3, A4, TOPREAL1:def_3;
 ( LSeg (g,k) is vertical or LSeg (g,k) is horizontal ) by SPPOL_1:19;
then A14: ( (g /. k) `1 = (g /. (k + 1)) `1 or (g /. k) `2 = (g /. (k + 1)) `2 ) by A13, SPPOL_1:15, SPPOL_1:16;
A15: rng g c= the carrier of (TOP-REAL 2) by FINSEQ_1:def_4;
 1 <= k + 1 by A3, NAT_1:13;
then A16: k + 1 in dom g by A4, FINSEQ_3:25;
then A17: g /. (k + 1) = g . (k + 1) by PARTFUN1:def_6;
then A18: g . (k + 1) in LSeg (g,k) by A3, A4, TOPREAL1:21;
 g . (k + 1) in rng g by A16, FUNCT_1:3;
then reconsider gk1 = g . (k + 1) as Point of (TOP-REAL 2) by A15;
 g . k in rng g by A10, FUNCT_1:3;
then reconsider gk = g . k as Point of (TOP-REAL 2) by A15;
 LSeg (gk,gk1) = LSeg (g,k) by A3, A4, A11, A17, TOPREAL1:def_3;
then A19: LSeg (g,k) is convex ;
A20: f is_in_general_position_wrt g by A1, Def2;
then A21: L~ f misses rng g by Def1;
percases ( not (L~ f) /\ (LSeg (g,k)) = {} or (L~ f) /\ (LSeg (g,k)) = {} ) ;
supposeA22: not (L~ f) /\ (LSeg (g,k)) = {} ; ::_thesis: ( 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 ) )
 (L~ f) /\ (LSeg (g,k)) is trivial by A3, A9, A20, Def1;
then consider x being set  such that
A23: (L~ f) /\ (LSeg (g,k)) = {x} by A22, ZFMISC_1:131;
 x in (L~ f) /\ (LSeg (g,k)) by A23, TARSKI:def_1;
then reconsider p = x as Point of (TOP-REAL 2) ;
A24: g /. (k + 1) = g . (k + 1) by A16, PARTFUN1:def_6;
then A25: g /. (k + 1) in rng g by A16, FUNCT_1:3;
A26: g /. k = g . k by A10, PARTFUN1:def_6;
then A27: g /. k in rng g by A10, FUNCT_1:3;
A28: now__::_thesis:_(_not_g_/._k_in_L~_f_&_not_g_/._(k_+_1)_in_L~_f_)
assume A29: ( g /. k in L~ f or g /. (k + 1) in L~ f ) ; ::_thesis: contradiction
percases ( g /. k in L~ f or g /. (k + 1) in L~ f ) by A29;
suppose g /. k in L~ f ; ::_thesis: contradiction
hence  contradiction by A21, A27, XBOOLE_0:3; ::_thesis: verum
end;
suppose g /. (k + 1) in L~ f ; ::_thesis: contradiction
hence  contradiction by A21, A25, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
 rng f misses L~ g by A2, Def1;
then A30: rng f misses LSeg ((g /. k),(g /. (k + 1))) by A13, TOPREAL3:19, XBOOLE_1:63;
 (L~ f) /\ (LSeg ((g /. k),(g /. (k + 1)))) = {p} by A3, A4, A23, TOPREAL1:def_3;
hence  ( 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 ) ) by A14, A23, A26, A24, A28, A30, Th2, Th32, CARD_1:30; ::_thesis: verum
end;
supposeA31: (L~ f) /\ (LSeg (g,k)) = {} ; ::_thesis: ( 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 ) )
then A32: LSeg (g,k) misses L~ f by XBOOLE_0:def_7;
then A33: ( not g . (k + 1) in RightComp f or not g . k in LeftComp f ) by A19, A12, A18, JORDAN1J:36;
A34: now__::_thesis:_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_)
percases ( not gk in RightComp f or not g . (k + 1) in LeftComp f ) by A19, A12, A18, A32, JORDAN1J:36;
supposeA35: not gk in RightComp f ; ::_thesis: 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 )
A36: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1;
 ( gk in LeftComp f & g . (k + 1) in LeftComp f ) by A6, A7, A8, A33, A35, GOBRD14:17;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A36; ::_thesis: verum
end;
supposeA37: not g . (k + 1) in LeftComp f ; ::_thesis: 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 )
A38: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2;
 ( g . (k + 1) in RightComp f & g . k in RightComp f ) by A5, A6, A7, A8, A33, A37, GOBRD14:18;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & g . k in C & g . (k + 1) in C ) by A38; ::_thesis: verum
end;
end;
end;
 card ((L~ f) /\ (LSeg (g,k))) = 2 * 0 by A31, CARD_1:27;
hence  ( 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 ) ) by A34; ::_thesis: verum
end;
end;
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 ) )
proof
let f1, f2, g1 be special FinSequence of (TOP-REAL 2); ::_thesis: ( 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. implies ( 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 ) ) )
assume that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: f1 ^' f2,g1 are_in_general_position and
A3: len g1 >= 2 and
A4: ( g1 is unfolded & g1 is s.n.c. ) ; ::_thesis: ( 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 ) )
reconsider g1 = g1 as special unfolded s.n.c. FinSequence of (TOP-REAL 2) by A4;
set Lf = L~ (f1 ^' f2);
 f1 ^' f2 is_in_general_position_wrt g1 by A2, Def2;
then A5: L~ (f1 ^' f2) misses rng g1 by Def1;
defpred S1[ Nat] means ( $1 <= len g1 implies for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg $1) holds
( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) );
A6: dom g1 = Seg (len g1) by FINSEQ_1:def_3;
A7: 1 + 1 <= len g1 by A3;
A8: now__::_thesis:_for_k_being_Nat_st_k_>=_2_&_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( k >= 2 & S1[k] implies S1[k + 1] )
assume that
A9: k >= 2 and
A10: S1[k] ; ::_thesis: S1[k + 1]
A11: k in NAT by ORDINAL1:def_12;
A12: 1 <= k by A9, XXREAL_0:2;
then A13: 1 <= k + 1 by NAT_1:13;
now__::_thesis:_(_k_+_1_<=_len_g1_implies_for_a_being_FinSequence_of_(TOP-REAL_2)_st_a_=_g1_|_(Seg_(k_+_1))_holds_
(_card_((L~_(f1_^'_f2))_/\_(L~_a))_is_even_Element_of_NAT_iff_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_(f1_^'_f2))_`_&_a_._1_in_C_&_a_._(len_a)_in_C_)_)_)
reconsider b = g1 | (Seg k) as FinSequence of (TOP-REAL 2) by FINSEQ_1:18;
 1 in Seg k by A12, FINSEQ_1:1;
then A14: b . 1 = g1 . 1 by FUNCT_1:49;
reconsider s1 = (L~ (f1 ^' f2)) /\ (L~ b) as finite set by A2, A11, Th6, Th11;
set c = LSeg (g1,k);
A15: k in Seg k by A12, FINSEQ_1:1;
reconsider s2 = (L~ (f1 ^' f2)) /\ (LSeg (g1,k)) as finite set by A2, A11, Th12;
A16: k <= k + 1 by NAT_1:13;
then A17: Seg k c= Seg (k + 1) by FINSEQ_1:5;
 k >= 1 + 1 by A9;
then A18: 1 < k by NAT_1:13;
A19: g1 . 1 in (L~ (f1 ^' f2)) ` by A2, A7, Th8;
assume A20: k + 1 <= len g1 ; ::_thesis: for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg (k + 1)) holds
( card ((L~ (f1 ^' f2)) /\ (L~ b2)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b3 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b3 & C . (len C) in b3 ) )
then A21: ( g1 . (k + 1) in (L~ (f1 ^' f2)) ` & g1 . k in (L~ (f1 ^' f2)) ` ) by A2, A11, A12, Th8;
let a be FinSequence of (TOP-REAL 2); ::_thesis: ( a = g1 | (Seg (k + 1)) implies ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) ) )
assume A22: a = g1 | (Seg (k + 1)) ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )
A23: dom a = (dom g1) /\ (Seg (k + 1)) by A22, RELAT_1:61;
A24: k + 1 in Seg (k + 1) by A13, FINSEQ_1:1;
then A25: g1 . (k + 1) = a . (k + 1) by A22, FUNCT_1:49
.= a . (len a) by A20, A22, FINSEQ_1:17 ;
A26: k + 1 in Seg (len g1) by A13, A20, FINSEQ_1:1;
then A27: k + 1 in dom a by A6, A24, A23, XBOOLE_0:def_4;
then A28: a /. (k + 1) = a . (k + 1) by PARTFUN1:def_6
.= g1 . (k + 1) by A22, A27, FUNCT_1:47
.= g1 /. (k + 1) by A6, A26, PARTFUN1:def_6 ;
A29: len a = k + 1 by A20, A22, FINSEQ_1:17;
 g1 | (k + 1) = a by A22, FINSEQ_1:def_15;
then  (L~ (a | k)) /\ (LSeg (a,k)) = {(a /. k)} by A11, A29, A18, GOBOARD2:4;
then A30: (L~ (a | k)) /\ (LSeg ((a /. k),(a /. (k + 1)))) = {(a /. k)} by A12, A29, TOPREAL1:def_3;
 1 in Seg (k + 1) by A13, FINSEQ_1:1;
then A31: g1 . 1 = a . 1 by A22, FUNCT_1:49;
reconsider s = (L~ (f1 ^' f2)) /\ (L~ a) as finite set by A2, A22, Th6, Th11;
A32: a = g1 | (k + 1) by A22, FINSEQ_1:def_15;
A33: k < len g1 by A20, NAT_1:13;
then A34: k in dom g1 by A6, A12, FINSEQ_1:1;
A35: a | k = (g1 | (Seg (k + 1))) | (Seg k) by A22, FINSEQ_1:def_15
.= g1 | (Seg k) by A17, FUNCT_1:51
.= g1 | k by FINSEQ_1:def_15 ;
A36: b . (len b) = b . k by A33, FINSEQ_1:17
.= g1 . k by A15, FUNCT_1:49 ;
 k in Seg (k + 1) by A12, A16, FINSEQ_1:1;
then A37: k in dom a by A34, A23, XBOOLE_0:def_4;
then a /. k = a . k by PARTFUN1:def_6
.= g1 . k by A22, A37, FUNCT_1:47
.= g1 /. k by A34, PARTFUN1:def_6 ;
then  (L~ b) /\ (LSeg ((g1 /. k),(g1 /. (k + 1)))) = {(g1 /. k)} by A35, A28, A30, FINSEQ_1:def_15;
then  (L~ b) /\ (LSeg (g1,k)) = {(g1 /. k)} by A12, A20, TOPREAL1:def_3;
then A38: (L~ b) /\ (LSeg (g1,k)) = {(g1 . k)} by A34, PARTFUN1:def_6;
A39: s1 misses s2
proof
assume  s1 meets s2 ; ::_thesis: contradiction
then consider x being set  such that
A40: x in s1 and
A41: x in s2 by XBOOLE_0:3;
 ( x in L~ b & x in LSeg (g1,k) ) by A40, A41, XBOOLE_0:def_4;
then  x in (L~ b) /\ (LSeg (g1,k)) by XBOOLE_0:def_4;
then  x = g1 . k by A38, TARSKI:def_1;
then A42: x in rng g1 by A34, FUNCT_1:3;
 x in L~ (f1 ^' f2) by A40, XBOOLE_0:def_4;
hence  contradiction by A5, A42, XBOOLE_0:3; ::_thesis: verum
end;
 k + 1 in dom g1 by A6, A13, A20, FINSEQ_1:1;
then  L~ a = (L~ (g1 | k)) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by A34, A32, TOPREAL3:38
.= (L~ b) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by FINSEQ_1:def_15
.= (L~ b) \/ (LSeg (g1,k)) by A12, A20, TOPREAL1:def_3 ;
then A43: s = s1 \/ s2 by XBOOLE_1:23;
percases ( card s1 is even Element of NAT or not card s1 is even Element of NAT ) ;
supposeA44: card s1 is even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )
then reconsider c1 = card ((L~ (f1 ^' f2)) /\ (L~ b)) as even Integer ;
now__::_thesis:_(_card_((L~_(f1_^'_f2))_/\_(L~_a))_is_even_Element_of_NAT_iff_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_(f1_^'_f2))_`_&_a_._1_in_C_&_a_._(len_a)_in_C_)_)
percases ( card s2 is even Element of NAT or not card s2 is even Element of NAT ) ;
supposeA45: card s2 is even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
then reconsider c2 = card ((L~ (f1 ^' f2)) /\ (LSeg (g1,k))) as even Integer ;
reconsider c = card s as Integer ;
A46: ( c = c1 + c2 & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & b . 1 in C & b . (len b) in C ) ) by A10, A20, A43, A39, A44, CARD_2:40, NAT_1:13;
 ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . k in C & g1 . (k + 1) in C ) by A1, A2, A11, A12, A20, A45, Th33;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) by A1, A31, A25, A14, A36, A46, Th16; ::_thesis: verum
end;
supposeA47: card s2 is not even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
then reconsider c2 = card ((L~ (f1 ^' f2)) /\ (LSeg (g1,k))) as odd Integer ;
reconsider c = card s as Integer ;
A48: ( c = c1 + c2 & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & b . 1 in C & b . (len b) in C ) ) by A10, A20, A43, A39, A44, CARD_2:40, NAT_1:13;
 for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not g1 . k in C or not g1 . (k + 1) in C ) by A1, A2, A11, A12, A20, A47, Th33;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) by A1, A31, A25, A14, A36, A48, Th16; ::_thesis: verum
end;
end;
end;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; ::_thesis: verum
end;
supposeA49: card s1 is not even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )
then reconsider c1 = card ((L~ (f1 ^' f2)) /\ (L~ b)) as odd Integer ;
now__::_thesis:_(_card_((L~_(f1_^'_f2))_/\_(L~_a))_is_even_Element_of_NAT_iff_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_(f1_^'_f2))_`_&_a_._1_in_C_&_a_._(len_a)_in_C_)_)
percases ( card s2 is even Element of NAT or not card s2 is even Element of NAT ) ;
supposeA50: card s2 is even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
then reconsider c2 = card ((L~ (f1 ^' f2)) /\ (LSeg (g1,k))) as even Integer ;
reconsider c = card s as Integer ;
A51: ( c = c1 + c2 & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not b . 1 in C or not b . (len b) in C ) ) ) by A10, A20, A43, A39, A49, CARD_2:40, NAT_1:13;
 ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . k in C & g1 . (k + 1) in C ) by A1, A2, A11, A12, A20, A50, Th33;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) by A1, A31, A25, A14, A36, A51, Th16; ::_thesis: verum
end;
supposeA52: card s2 is not even Element of NAT ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
then reconsider c2 = card ((L~ (f1 ^' f2)) /\ (LSeg (g1,k))) as odd Integer ;
reconsider c = card s as Integer ;
A53: ( c = c1 + c2 & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not b . 1 in C or not b . (len b) in C ) ) ) by A10, A20, A43, A39, A49, CARD_2:40, NAT_1:13;
 for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not g1 . k in C or not g1 . (k + 1) in C ) by A1, A2, A11, A12, A20, A52, Th33;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) by A1, A31, A19, A21, A25, A14, A36, A53, Th17; ::_thesis: verum
end;
end;
end;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 dom g1 = Seg (len g1) by FINSEQ_1:def_3;
then A54: g1 | (Seg (len g1)) = g1 by RELAT_1:69;
A55: 2 in dom g1 by A3, FINSEQ_3:25;
A56: 1 <= len g1 by A3, XXREAL_0:2;
then A57: 1 in dom g1 by FINSEQ_3:25;
now__::_thesis:_for_a_being_FinSequence_of_(TOP-REAL_2)_st_a_=_g1_|_(Seg_2)_holds_
(_card_((L~_(f1_^'_f2))_/\_(L~_a))_is_even_Element_of_NAT_iff_ex_C_being_Subset_of_(TOP-REAL_2)_st_
(_C_is_a_component_of_(L~_(f1_^'_f2))_`_&_a_._1_in_C_&_a_._(len_a)_in_C_)_)
 g1 | 1 = g1 | (Seg 1) by FINSEQ_1:def_15;
then A58: len (g1 | 1) = 1 by A56, FINSEQ_1:17;
A59: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2;
let a be FinSequence of (TOP-REAL 2); ::_thesis: ( a = g1 | (Seg 2) implies ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) )
assume A60: a = g1 | (Seg 2) ; ::_thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
A61: a . (len a) = a . 2 by A3, A60, FINSEQ_1:17
.= g1 . (1 + 1) by A60, A59, FUNCT_1:49 ;
 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2;
then A62: a . 1 = g1 . 1 by A60, FUNCT_1:49;
L~ a = L~ (g1 | 2) by A60, FINSEQ_1:def_15
.= (L~ (g1 | 1)) \/ (LSeg ((g1 /. 1),(g1 /. (1 + 1)))) by A57, A55, TOPREAL3:38
.= (L~ (g1 | 1)) \/ (LSeg (g1,1)) by A3, TOPREAL1:def_3
.= {} \/ (LSeg (g1,1)) by A58, TOPREAL1:22
.= LSeg (g1,1) ;
hence  ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) by A1, A2, A3, A62, A61, Th33; ::_thesis: verum
end;
then A63: S1[2] ;
 for k being Nat st k >= 2 holds
S1[k] from NAT_1:sch_8(A63, A8);
hence  ( 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 ) ) by A3, A54; ::_thesis: verum
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 )
proof
let f1, f2, g1, g2 be special FinSequence of (TOP-REAL 2); ::_thesis: ( 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 implies 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 ) )
assume 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 ; ::_thesis: 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 )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( 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 ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) )
assume that
A6: ( f1 . 1 = p1 & f1 . (len f1) = p2 ) and
A7: ( g1 . 1 = q1 & g1 . (len g1) = q2 ) and
A8: f1 /. (len f1) = f2 /. 1 and
A9: g1 /. (len g1) = g2 /. 1 and
A10: p1 in (L~ f1) /\ (L~ f2) and
A11: q1 in (L~ g1) /\ (L~ g2) and
A12: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) ; ::_thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C )
A13: f1 ^' f2,g1 are_in_general_position by A5, Th7;
A14: now__::_thesis:_(_not_len_f1_=_0_&_not_len_f1_=_1_&_not_len_f2_=_0_&_not_len_f2_=_1_)
assume A15: ( len f1 = 0 or len f1 = 1 or len f2 = 0 or len f2 = 1 ) ; ::_thesis: contradiction
percases ( len f1 = 0 or len f1 = 1 or len f2 = 0 or len f2 = 1 ) by A15;
suppose ( len f1 = 0 or len f1 = 1 ) ; ::_thesis: contradiction
then  L~ f1 = {} by TOPREAL1:22;
hence  contradiction by A10; ::_thesis: verum
end;
suppose ( len f2 = 0 or len f2 = 1 ) ; ::_thesis: contradiction
then  L~ f2 = {} by TOPREAL1:22;
hence  contradiction by A10; ::_thesis: verum
end;
end;
end;
then A16: not len f2 is trivial by NAT_2:def_1;
then A17: not f2 is trivial by Lm2;
A18: now__::_thesis:_(_not_len_g1_=_0_&_not_len_g1_=_1_&_not_len_g2_=_0_&_not_len_g2_=_1_)
assume A19: ( len g1 = 0 or len g1 = 1 or len g2 = 0 or len g2 = 1 ) ; ::_thesis: contradiction
percases ( len g1 = 0 or len g1 = 1 or len g2 = 0 or len g2 = 1 ) by A19;
suppose ( len g1 = 0 or len g1 = 1 ) ; ::_thesis: contradiction
then  L~ g1 = {} by TOPREAL1:22;
hence  contradiction by A11; ::_thesis: verum
end;
suppose ( len g2 = 0 or len g2 = 1 ) ; ::_thesis: contradiction
then  L~ g2 = {} by TOPREAL1:22;
hence  contradiction by A11; ::_thesis: verum
end;
end;
end;
then A20: not len g2 is trivial by NAT_2:def_1;
then A21: not g2 is trivial by Lm2;
A22: not len g1 is trivial by A18, NAT_2:def_1;
then A23: not g1 is empty by Lm2;
 len g2 >= 1 + 1 by A20, NAT_2:29;
then A24: ( g1 is unfolded & g1 is s.n.c. ) by A2, Th4;
 len g1 >= 2 by A22, NAT_2:29;
then A25: card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT by A1, A7, A12, A13, A24, Th34;
 len f2 >= 1 + 1 by A16, NAT_2:29;
then A26: ( f1 is unfolded & f1 is s.n.c. ) by A1, Th4;
A27: g1 ^' g2,f1 are_in_general_position by A5, Th7;
A28: not len f1 is trivial by A14, NAT_2:def_1;
then  not f1 is empty by Lm2;
then A29: (L~ (f1 ^' f2)) /\ (L~ g1) = ((L~ f1) \/ (L~ f2)) /\ (L~ g1) by A8, A17, TOPREAL8:35
.= ((L~ f1) /\ (L~ g1)) \/ ((L~ f2) /\ (L~ g1)) by XBOOLE_1:23
.= ((L~ f1) /\ (L~ g1)) \/ {} by A4, 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 A9, A23, A21, TOPREAL8:35 ;
 len f1 >= 2 by A28, NAT_2:29;
hence  ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) by A2, A6, A29, A27, A26, A25, Th34; ::_thesis: verum
end;