:: On the General Position of Special Polygons :: by Mariusz Giero :: :: Received May 27, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin Lm1: for f being FinSequence st dom f is trivial holds len f is trivial proofend; Lm2: for f being FinSequence st f is trivial holds len f is trivial proofend; theorem :: JORDAN12:1 for i being Element of NAT st 1 < i holds 0 < i -' 1 proofend; theorem Th2: :: JORDAN12:2 1 is odd proofend; 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 ) proofend; 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. proofend; 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. ) proofend; theorem Th5: :: JORDAN12:5 for g1, g2 being FinSequence of (TOP-REAL 2) holds L~ g1 c= L~ (g1 ^' g2) proofend; 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 proofend; 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 proofend; 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) ` ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) ) proofend; 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 ) ) ) proofend; 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 ) proofend; 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 ) proofend; 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 toTARSKI: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 proofend; 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 toTARSKI: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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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) proofend; 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 proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) proofend;