The Mizar article:

On the General Position of Special Polygons

by
Mariusz Giero

Received May 27, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: JORDAN12
[ MML identifier index ]


environ

 vocabulary JORDAN12, FINSEQ_1, EUCLID, TOPREAL1, BOOLE, RELAT_1, REALSET1,
      PRE_TOPC, FUNCT_1, GRAPH_2, GOBOARD5, CONNSP_1, SUBSET_1, CARD_1,
      MATRIX_2, INT_1, FINSET_1, TARSKI, SETFAM_1, ARYTM_1, SEQM_3, RELAT_2,
      GOBOARD9, MCART_1, MATRIX_1, GOBOARD2, FINSEQ_4, GOBOARD1, JORDAN1,
      TOPS_1, TREES_1, SPPOL_1, FINSEQ_5;
 notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, XCMPLX_0, XREAL_0, REAL_1,
      NAT_1, BINARITH, ABIAN, INT_1, GRAPH_2, RELAT_1, CARD_1, FINSET_1,
      FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, REALSET1, PRE_TOPC,
      TOPS_1, CONNSP_1, EUCLID, TOPREAL1, SPPOL_1, JORDAN1, GOBOARD1, GOBOARD2,
      GOBOARD5, GOBOARD9, GOBRD13;
 constructors REALSET1, FINSEQ_4, GRAPH_2, CONNSP_1, ABIAN, INT_1, GOBOARD9,
      TOPS_1, GOBOARD2, BINARITH, GOBRD13, JORDAN1, SPPOL_1, COMPTS_1,
      MEMBERED;
 clusters RELSET_1, SPPOL_2, EUCLID, GOBOARD5, ABIAN, YELLOW13, SUBSET_1,
      INT_1, GOBOARD2, GOBOARD9, JORDAN10, TEX_2, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, TARSKI, GOBOARD5, TOPREAL1, JORDAN1;
 theorems SPPOL_1, XBOOLE_0, TOPREAL1, JORDAN4, TARSKI, SPPOL_2, FUNCT_1,
      FINSEQ_4, FINSEQ_1, NAT_1, SETFAM_1, FINSET_1, LATTICE4, CARD_2, RELAT_1,
      TOPREAL3, GOBOARD9, AXIOMS, CARD_1, SUBSET_1, GOBRD14, JORDAN1H, GOBRD12,
      JORDAN9, XBOOLE_1, JORDAN1, GOBOARD5, JORDAN8, GOBRD13, GOBOARD6, EUCLID,
      GOBOARD7, TOPS_1, NAT_2, JORDAN1G, SPRECT_3, SPRECT_2, REAL_1, JORDAN1J,
      BINARITH, FINSEQ_5, AMI_5, GOBRD11, RLVECT_1, TOPREAL6, GOBOARD2, CARD_5,
      SPRECT_1, REALSET1, TOPREAL8, GRAPH_2, FINSEQ_3, JORDAN3, JORDAN5B,
      XCMPLX_1;
 schemes FRAENKEL, INT_2;

begin

reserve i,j,k,n for Nat,
        X,Y,a,b,c,x for set,
        r,s for Real;

Lm1:
for R be Relation st R is trivial holds dom R is trivial
proof
  let R be Relation;
  assume
A1: R is trivial;
  per cases by A1,REALSET1:def 12;
  suppose R is empty;
  hence thesis by A1,RELAT_1:60;
  suppose ex x being set st R = {x};
  then consider x being set such that
A2:  R = {x};
    x in R by A2,TARSKI:def 1;
  then consider y being set such that
A3:  ex z be set st x=[y,z] by RELAT_1:def 1;
    dom R = {y} by A2,A3,RELAT_1:23;
  hence thesis;
  end;

Lm2:
for f being FinSequence st dom f is trivial holds len f is trivial
proof
  let f be FinSequence;
  assume
A1: dom f is trivial;
A2: Seg len f = dom f by FINSEQ_1:def 3;
  per cases by A1,REALSET1:def 12;
  suppose dom f is empty;
  then f = {} by FINSEQ_1:26;
  then len f = 0 by FINSEQ_1:25;
  hence thesis by REALSET1:def 12;
  suppose ex x being set st dom f = {x};
  hence thesis by A2,CARD_5:1,FINSEQ_3:22;
end;

Lm3:
for f be FinSequence st f is trivial holds len f is trivial
proof
  let f be FinSequence;
  assume f is trivial;
  then dom f is trivial by Lm1;
  hence thesis by Lm2;
end;

theorem
    1 < i implies 0 < i-'1
proof
assume A1: 1 < i;
A2:1-1=0;
  1-'1<i-'1 by A1,SPRECT_3:9;
hence 0 < i-'1 by A2,BINARITH:def 3;
end;

canceled;

theorem Th3:
1 is odd
proof
    1=2*0+1;
  hence 1 is odd;
end;

theorem Th4:
for f be FinSequence of TOP-REAL n
for i st 1 <= i & i + 1 <= len f holds
f/.i in rng f & f/.(i+1) in rng f
proof
  let f be FinSequence of TOP-REAL n;
  let i; assume
A1:  1 <= i & i + 1 <= len f;
then A2: i + 1 in dom f by GOBOARD2:3;
A3: i in dom f by A1,GOBOARD2:3;
  then f.i in rng f by FUNCT_1:12;
  hence f/.i in rng f by A3,FINSEQ_4:def 4;
    f.(i+1) in rng f by A2,FUNCT_1:12;
  hence f/.(i+1) in rng f by A2,FINSEQ_4:def 4;
end;

definition
 cluster s.n.c. -> s.c.c. FinSequence of TOP-REAL 2;
 coherence
  proof let f be FinSequence of TOP-REAL 2 such that
A1:  for i,j st i+1 < j holds LSeg(f,i) misses LSeg(f,j);
   let i,j; thus thesis by A1;
  end;
end;

theorem Th5:
for f,g be FinSequence of TOP-REAL 2 st
  f ^' g is unfolded s.c.c. & len g >= 2 holds f is unfolded s.n.c.
proof
  let f,g be FinSequence of TOP-REAL 2 such that
A1:  f ^' g is unfolded s.c.c. and
A2: len g >= 2;
       len g > 0 by A2,AXIOMS:22;
then A3: g <> {} by FINSEQ_1:25;
A4: now assume not f is s.n.c.;
 then consider i,j such that
A5:  i+1 < j & not LSeg(f,i) misses LSeg(f,j) by TOPREAL1:def 9;
  now assume not (1<=i & i+1 <= len f);
  then LSeg(f,i) = {} by TOPREAL1:def 5;
  hence contradiction by A5,XBOOLE_1:65;
end;
then A6:i<len f by NAT_1:38;
A7: now assume not (1<=j & j+1 <= len f);
then LSeg(f,j) = {} by TOPREAL1:def 5;
hence contradiction by A5,XBOOLE_1:65;
end;
then A8:j < len f by NAT_1:38;
  len (f^'g) + 1 = len f + len g by A3,GRAPH_2:13;
then len (f^'g) + 1 - 1 = len f + (len g - 1) by XCMPLX_1:29;
then A9: len (f^'g) = len f + (len g - 1) by XCMPLX_1:26;
  1 = 2-1;
then len g - 1 >= 1 by A2,REAL_1:49;
then len g - 1 > 0 by AXIOMS:22;
then len f < len (f^'g) by A9,REAL_1:69;
then A10: j+1 < len (f^'g) by A7,AXIOMS:22;
A11: LSeg(f^'g,i) = LSeg(f,i) by A6,TOPREAL8:28;
  LSeg(f^'g,j) = LSeg(f,j) by A8,TOPREAL8:28;
hence contradiction by A1,A5,A10,A11,GOBOARD5:def 4;
end;
  now assume not f is unfolded;
  then consider i such that
A12:   1 <= i & i + 2 <= len f & LSeg(f,i) /\ LSeg(f,i+1) <> {f/.(i+1)}
               by TOPREAL1:def 8;
      i+1 < i+1+1 by NAT_1:38;
    then i+1 < i+(1+1) by XCMPLX_1:1;
then A13: 1 <= i+1 & i+1 < len f by A12,AXIOMS:22,NAT_1:38;
then A14: i+1 in dom f by FINSEQ_3:27;
A15:len f <= len (f^'g) by TOPREAL8:7;
then A16: i+2 <= len (f^'g) by A12,AXIOMS:22;
      i+1 <= len (f^'g) by A13,A15,AXIOMS:22;
then A17: i+1 in dom (f^'g) by A13,FINSEQ_3:27;
A18: f/.(i+1) = f.(i+1) by A14,FINSEQ_4:def 4
            .= (f^'g).(i+1) by A13,GRAPH_2:14
            .= (f^'g)/.(i+1) by A17,FINSEQ_4:def 4;
    i < len f by A13,NAT_1:38;
then A19:LSeg(f^'g,i) = LSeg(f,i) by TOPREAL8:28;
    LSeg(f^'g,i+1) = LSeg(f,i+1)by A13,TOPREAL8:28;
 hence contradiction by A1,A12,A16,A18,A19,TOPREAL1:def 8;
end;
 hence f is unfolded s.n.c. by A4;
end;

theorem Th6:
for g1,g2 be FinSequence of TOP-REAL 2 holds L~g1 c= L~(g1^'g2)
proof
  let g1,g2 be FinSequence of TOP-REAL 2;
  let x such that
A1:  x in L~g1;
   x in union { LSeg(g1,i) : 1 <= i & i+1 <= len g1 } by A1,TOPREAL1:def 6;
  then consider a such that
A2:   x in a & a in { LSeg(g1,i) : 1 <= i & i+1 <= len g1 } by TARSKI:def 4;
  consider j such that
A3:  a = LSeg(g1,j) & 1 <= j & j+1 <= len g1 by A2;
       j < len g1 by A3,NAT_1:38;
then A4:  a = LSeg(g1^'g2,j) by A3,TOPREAL8:28;
    len g1 <= len (g1^'g2) by TOPREAL8:7;
  then j+1 <= len (g1^'g2) by A3,AXIOMS:22;
  then a in { LSeg(g1^'g2,i) : 1 <= i & i+1 <= len (g1^'g2) } by A3,A4;
  then x in union { LSeg(g1^'g2,i) : 1 <= i & i+1 <= len (g1^'g2) }
                     by A2,TARSKI:def 4;
  hence x in L~(g1^'g2) by TOPREAL1:def 6;
end;

begin

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

definition let n; let f1,f2 be FinSequence of TOP-REAL n;
  pred f1,f2 are_in_general_position means :Def2:
   f1 is_in_general_position_wrt f2 &
    f2 is_in_general_position_wrt f1;
  symmetry;
end;

theorem Th7:
for f1,f2 being FinSequence of TOP-REAL 2 st
f1,f2 are_in_general_position holds
for f being FinSequence of TOP-REAL 2 st f = f2|(Seg k)
holds f1,f are_in_general_position
proof
  let f1,f2 be FinSequence of TOP-REAL 2;
  assume that
A1:  f1,f2 are_in_general_position;
  let f be FinSequence of TOP-REAL 2 such that
A2:   f = f2|(Seg k);
A3: f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1
      by A1,Def2;
then A4: L~f1 misses rng f2 by Def1;
A5:f = f2|k by A2,TOPREAL1:def 1;
then A6: len f <= len f2 by FINSEQ_5:18;
A7: now
  let i such that
A8: 1<=i & i < len f;
A9: i+1<=len f by A8,NAT_1:38;
A10: i in dom(f2|k) by A5,A8,FINSEQ_3:27;
      1<=i+1 by A8,NAT_1:38;
then A11: i+1 in dom (f2|k) by A5,A9,FINSEQ_3:27;
A12: i+1<=len f2 by A6,A9,AXIOMS:22;
A13: f/.i = f2/.i by A5,A10,TOPREAL1:1;
A14: f/.(i+1) = f2/.(i+1) by A5,A11,TOPREAL1:1;
A15: i < len f2 by A12,NAT_1:38;
    LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A8,A9,TOPREAL1:def 5
           .= LSeg(f2,i) by A8,A12,A13,A14,TOPREAL1:def 5;
  hence L~f1 /\ LSeg(f,i) is trivial by A3,A8,A15,Def1;
end;
      rng f c= rng f2 by A2,RELAT_1:99;
    then rng f misses L~f1 by A4,XBOOLE_1:63;
then A16: f1 is_in_general_position_wrt f by A7,Def1;
A17: L~f2 misses rng f1 by A3,Def1;
A18:L~f c= L~f2 by A5,TOPREAL3:27;
then A19: L~f misses rng f1 by A17,XBOOLE_1:63;
  now
  let i such that
A20: 1<=i & i < len f1;
A21: L~f2 /\ LSeg(f1,i) is trivial by A3,A20,Def1;
    L~f /\ LSeg(f1,i) c= L~f2 /\ LSeg(f1,i) by A18,XBOOLE_1:26;
  hence L~f /\ LSeg(f1,i) is trivial by A21,SPRECT_1:1;
end;
  then f is_in_general_position_wrt f1 by A19,Def1;
  hence f1,f are_in_general_position by A16,Def2;
end;

theorem Th8:
for f1,f2,g1,g2 be FinSequence of TOP-REAL 2 st
  f1^'f2,g1^'g2 are_in_general_position holds
        f1^'f2,g1 are_in_general_position
proof
  let f1,f2,g1,g2 be FinSequence of TOP-REAL 2 such that
A1:  f1^'f2,g1^'g2 are_in_general_position;
A2:  f1^'f2 is_in_general_position_wrt g1^'g2 &
         g1^'g2 is_in_general_position_wrt f1^'f2 by A1,Def2;
then A3: L~(f1^'f2) misses rng (g1^'g2) by Def1;
      rng g1 c= rng (g1^'g2) by TOPREAL8:10;
then A4: L~(f1^'f2) misses rng g1 by A3,XBOOLE_1:63;
A5: L~(g1^'g2) misses rng (f1^'f2) by A2,Def1;
      L~g1 c= L~(g1^'g2) by Th6;
then A6: L~g1 misses rng (f1^'f2) by A5,XBOOLE_1:63;
A7: now
let i such that
A8: 1<=i & i < len (f1^'f2);
      L~g1 c= L~(g1^'g2) by Th6;
then A9:L~g1 /\ LSeg(f1^'f2,i) c= L~(g1^'g2) /\ LSeg(f1^'f2,i) by XBOOLE_1:26;
    L~(g1^'g2) /\ LSeg(f1^'f2,i) is trivial by A2,A8,Def1;
  hence L~g1 /\ LSeg(f1^'f2,i) is trivial by A9,SPRECT_1:1;
end;
  now
   let i such that
A10: 1<=i & i < len g1;
     len g1 <= len (g1^'g2) by TOPREAL8:7;
   then i < len (g1^'g2) by A10,AXIOMS:22;
   then L~(f1^'f2) /\ LSeg(g1^'g2,i) is trivial by A2,A10,Def1;
   hence L~(f1^'f2) /\ LSeg(g1,i) is trivial by A10,TOPREAL8:28;
end;
then f1^'f2 is_in_general_position_wrt g1 & g1 is_in_general_position_wrt f1^'
f2
        by A4,A6,A7,Def1;
  hence f1^'f2,g1 are_in_general_position by Def2;
end;

reserve f,g for FinSequence of TOP-REAL 2;

theorem Th9:
for k,f,g st 1<=k & k+1<=len g &
        f,g are_in_general_position holds g.k in (L~f)` & g.(k+1) in (L~f)`
proof
let k,f,g such that
A1: 1<=k & k+1<=len g and
A2: f,g are_in_general_position;
      f is_in_general_position_wrt g by A2,Def2;
then A3: L~f misses rng g by Def1;
A4: 1<=k+1 by A1,NAT_1:38;
      k < len g by A1,NAT_1:38;
then A5: k in dom g by A1,FINSEQ_3:27;
A6: k+1 in dom g by A1,A4,FINSEQ_3:27;
A7: g.k in rng g by A5,FUNCT_1:12;
A8: rng g c= the carrier of TOP-REAL 2 by FINSEQ_1:def 4;
A9: g.(k+1) in rng g by A6,FUNCT_1:12;
  now
  assume not g.k in (L~f)`;
  then g.k in (the carrier of TOP-REAL 2) \ (L~f)` by A7,A8,XBOOLE_0:def 4;
  then g.k in (L~f)`` by SUBSET_1:def 5;
  hence contradiction by A3,A7,XBOOLE_0:3;
end;
hence g.k in (L~f)`;
  now
  assume not g.(k+1) in (L~f)`;
  then g.(k+1) in (the carrier of TOP-REAL 2) \ (L~f)`
    by A8,A9,XBOOLE_0:def 4;
  then g.(k+1) in (L~f)`` by SUBSET_1:def 5;
  hence contradiction by A3,A9,XBOOLE_0:3;
end;
hence g.(k+1) in (L~f)`;
end;

theorem Th10:
for f1,f2 be FinSequence of TOP-REAL 2
           st f1,f2 are_in_general_position
for i,j st (1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2)
    holds LSeg(f1,i) /\ LSeg(f2,j) is trivial
proof
  let f1,f2 be FinSequence of TOP-REAL 2 such that
A1:  f1,f2 are_in_general_position;
  let i,j such that
A2:  1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2;
A3: f1 is_in_general_position_wrt f2 &
     f2 is_in_general_position_wrt f1 by A1,Def2;
then A4: L~f1 misses rng f2 by Def1;
A5: L~f2 misses rng f1 by A3,Def1;
    now
    assume A6: LSeg(f1,i) /\ LSeg(f2,j) is non trivial;
    set A = LSeg(f1,i) /\ LSeg(f2,j);
    set A1 = LSeg(f1,i), A2 = LSeg(f2,j);
    set B1 = LSeg(f1/.i,f1/.(i+1)), B2 = LSeg(f2/.j,f2/.(j+1));
    consider a1,a2 being set such that
A7: a1 in A & a2 in A & a1 <> a2 by A6,SPPOL_1:3;
A8: a1 in A1 & a1 in A2 & a2 in A1 & a2 in A2 by A7,XBOOLE_0:def 3;
    reconsider a1, a2 as Point of TOP-REAL 2 by A7;
A9: A1 = B1 by A2,TOPREAL1:def 5;
A10: a2 in B2 by A2,A8,TOPREAL1:def 5;
A11: a1 in B2 by A2,A8,TOPREAL1:def 5;
A12:a2 in B1 by A7,A9,XBOOLE_0:def 3;
A13: a1 in LSeg(f1/.i,a2) \/ LSeg(a2,f1/.(i+1)) by A8,A9,TOPREAL1:11;
A14:a1 in LSeg(f2/.j,a2) \/ LSeg(a2,f2/.(j+1)) by A10,A11,TOPREAL1:11;
      f2/.j in B2 by TOPREAL1:6;
then A15: LSeg(a2, f2/.j) c= B2 by A10,TOPREAL1:12;
      f1/.i in B1 by TOPREAL1:6;
then A16: LSeg(a2, f1/.i) c= B1 by A12,TOPREAL1:12;
      f1/.(i+1) in B1 by TOPREAL1:6;
then A17:LSeg(a2,f1/.(i+1)) c= B1 by A12,TOPREAL1:12;
      f2/.(j+1) in B2 by TOPREAL1:6;
then A18:LSeg(a2,f2/.(j+1)) c= B2 by A10,TOPREAL1:12;
A19: f1/.i in rng f1 by A2,Th4;
A20: f2/.j in rng f2 by A2,Th4;
A21:f1/.(i+1) in rng f1 by A2,Th4;
A22:f2/.(j+1) in rng f2 by A2,Th4;
    per cases by A13,XBOOLE_0:def 2;
    suppose A23:a1 in LSeg(f1/.i,a2);
      now per cases by A14,XBOOLE_0:def 2;
      suppose a1 in LSeg(f2/.j,a2);
        then f1/.i in LSeg(a2,f2/.j) or
        f2/.j in LSeg(a2,f1/.i) by A7,A23,JORDAN4:53;
then A24:     f1/.i in B2 or f2/.j in B1 by A15,A16;
          now per cases by A2,A24,TOPREAL1:def 5;
          suppose f1/.i in A2;
          then f1/.i in L~f2 by SPPOL_2:17;
          hence contradiction by A5,A19,XBOOLE_0:3;
          suppose f2/.j in A1;
          then f2/.j in L~f1 by SPPOL_2:17;
          hence contradiction by A4,A20,XBOOLE_0:3;
        end;
      hence contradiction;
      suppose a1 in LSeg(a2,f2/.(j+1));
      then f1/.i in LSeg(a2,f2/.(j+1)) or
          f2/.(j+1) in LSeg(a2,f1/.i) by A7,A23,JORDAN4:53;
then A25:  f1/.i in B2 or f2/.(j+1) in B1 by A16,A18;
        now per cases by A2,A25,TOPREAL1:def 5;
        suppose f1/.i in A2;
        then f1/.i in L~f2 by SPPOL_2:17;
        hence contradiction by A5,A19,XBOOLE_0:3;
        suppose f2/.(j+1) in A1;
          then f2/.(j+1) in L~f1 by SPPOL_2:17;
        hence contradiction by A4,A22,XBOOLE_0:3;
      end;
      hence contradiction;
    end;
    hence contradiction;
    suppose A26: a1 in LSeg(a2,f1/.(i+1));
        now per cases by A14,XBOOLE_0:def 2;
        suppose a1 in LSeg(f2/.j,a2);
        then f1/.(i+1) in LSeg(a2,f2/.j) or
        f2/.j in LSeg(a2,f1/.(i+1)) by A7,A26,JORDAN4:53;
then A27:    f1/.(i+1) in B2 or f2/.j in B1 by A15,A17;
          now per cases by A2,A27,TOPREAL1:def 5;
          suppose f1/.(i+1) in A2;
          then f1/.(i+1) in L~f2 by SPPOL_2:17;
          hence contradiction by A5,A21,XBOOLE_0:3;
          suppose f2/.j in A1;
          then f2/.j in L~f1 by SPPOL_2:17;
          hence contradiction by A4,A20,XBOOLE_0:3;
        end;
        hence contradiction;
         suppose a1 in LSeg(a2,f2/.(j+1));
      then f1/.(i+1) in LSeg(a2,f2/.(j+1)) or
      f2/.(j+1) in LSeg(a2,f1/.(i+1)) by A7,A26,JORDAN4:53;
then A28:  f1/.(i+1) in B2 or f2/.(j+1) in B1 by A17,A18;
        now per cases by A2,A28,TOPREAL1:def 5;
        suppose f1/.(i+1) in A2;
          then f1/.(i+1) in L~f2 by SPPOL_2:17;
          hence contradiction by A5,A21,XBOOLE_0:3;
        suppose f2/.(j+1) in A1;
          then f2/.(j+1) in L~f1 by SPPOL_2:17;
          hence contradiction by A4,A22,XBOOLE_0:3;
      end;
      hence contradiction;
    end;
    hence contradiction;
  end;
  hence LSeg(f1,i) /\ LSeg(f2,j) is trivial;
end;

theorem Th11:
for f,g holds
INTERSECTION({ LSeg(f,i) : 1 <= i & i+1 <= len f },
                { LSeg(g,j) : 1 <= j & j+1 <= len g }) is finite
proof
  let f,g;
set AL = { LSeg(f,i) : 1 <= i & i+1 <= len f };
set BL = { LSeg(g,j) : 1 <= j & j+1 <= len g };
deffunc F(set,set)=$1 /\ $2;
set IN = { F(X,Y) where X is Subset of TOP-REAL 2,
                  Y is Subset of TOP-REAL 2
             : X in AL & Y in BL };
A1: AL is finite by SPPOL_1:45;
A2: BL is finite by SPPOL_1:45;
A3: IN is finite from CartFin(A1,A2);
set C = INTERSECTION(AL,BL);
  IN = C
proof
  thus IN c= C
    proof
      let a such that
A4:      a in IN;
      consider X,Y be Subset of TOP-REAL 2 such that
A5: a = X /\ Y & X in AL & Y in BL by A4;
      thus a in C by A5,SETFAM_1:def 5;
    end;
  thus C c= IN
  proof
    let a; assume a in C;
    then consider X,Y such that
A6: X in AL & Y in BL & a = X /\ Y by SETFAM_1:def 5;
    consider i such that
A7: X = LSeg(f,i) & 1 <= i & i+1 <= len f by A6;
    consider j such that
A8: Y = LSeg(g,j) & 1 <= j & j+1 <= len g by A6;
    reconsider X,Y as Subset of TOP-REAL 2 by A7,A8;
      X /\ Y in IN by A6;
    hence a in IN by A6;
  end;
end;
hence thesis by A3;
end;

theorem Th12:
for f,g st f,g are_in_general_position holds
      L~f /\ L~g is finite
proof
  let f,g such that
A1:  f,g are_in_general_position;
set AL = { LSeg(f,i) : 1 <= i & i+1 <= len f };
set BL = { LSeg(g,j) : 1 <= j & j+1 <= len g };
A2: L~f /\ L~g = L~f /\ union BL by TOPREAL1:def 6
    .= union AL /\ union BL by TOPREAL1:def 6
    .= union INTERSECTION(AL,BL) by LATTICE4:2;
A3: INTERSECTION(AL,BL) is finite by Th11;
  now
  let Z be set such that
A4:  Z in INTERSECTION(AL,BL);
  consider X,Y be set such that
A5: X in AL & Y in BL & Z = X /\ Y by A4,SETFAM_1:def 5;
  consider i be Nat such that
A6: X = LSeg(f,i) & 1 <= i & i+1 <= len f by A5;
  consider j be Nat such that
A7:  Y = LSeg(g,j) & 1 <= j & j+1 <= len g by A5;
  Z is trivial set by A1,A5,A6,A7,Th10;
hence Z is finite;
end;
hence L~f /\ L~g is finite by A2,A3,FINSET_1:25;
end;

theorem Th13:
 for f,g st f,g are_in_general_position
   for k holds L~f /\ LSeg(g,k) is finite
proof
   let f,g such that A1: f,g are_in_general_position;
   let k;
A2:LSeg(g,k) c= L~g by TOPREAL3:26;
A3:L~f /\ L~g is finite by A1,Th12;
     L~f /\ L~g /\ LSeg(g,k) = L~f /\ (L~g /\ LSeg(g,k)) by XBOOLE_1:16
                        .= L~f /\ LSeg(g,k) by A2,XBOOLE_1:28;
   hence L~f /\ LSeg(g,k) is finite by A3,FINSET_1:15;
end;

begin

reserve f for non constant standard special_circular_sequence,

        p,p1,p2,q for Point of TOP-REAL 2;

theorem Th14:
  for f,p1,p2 st LSeg(p1,p2) misses L~f
  holds (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C))
proof
  let f,p1,p2;
  assume A1: LSeg(p1,p2) misses L~f;
A2:  LSeg(p1,p2) is connected by GOBOARD9:8;
A3:  p1 in LSeg(p1,p2) by TOPREAL1:6;
A4:  p2 in LSeg(p1,p2) by TOPREAL1:6;
then A5:  not (p2 in RightComp f & p1 in LeftComp f) by A1,A2,A3,JORDAN1J:36;
A6: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A7: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
A8: not p1 in L~f by A1,A3,XBOOLE_0:3;
A9: not p2 in L~f by A1,A4,XBOOLE_0:3;
    now per cases by A1,A2,A3,A4,JORDAN1J:36;
    suppose A10:not p1 in RightComp f;
then A11: p1 in LeftComp f by A8,GOBRD14:27;
      p2 in LeftComp f by A5,A8,A9,A10,GOBRD14:27;
    hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)) by A6,A11;
    suppose A12: not p2 in LeftComp f;
then A13: p2 in RightComp f by A9,GOBRD14:28;
      p1 in RightComp f by A5,A8,A9,A12,GOBRD14:28;
    hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)) by A7,A13;
  end;
hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C));
end;

theorem Th15:
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
     a in C & b in C))
  iff ((a in RightComp f & b in RightComp f) or
           (a in LeftComp f & b in LeftComp f))
proof
A1:   LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A2:   RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  thus (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
     a in C & b in C))
  implies ((a in RightComp f & b in RightComp f) or
           (a in LeftComp f & b in LeftComp f)) by JORDAN1H:30;
  thus ((a in RightComp f & b in RightComp f) or
           (a in LeftComp f & b in LeftComp f)) implies
   (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
          a in C & b in C)) by A1,A2;
end;

theorem Th16:
a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
                           (C is_a_component_of (L~f)` & a in C & b in C))
  iff ((a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f))
proof
A1: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A2: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  thus a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
                           (C is_a_component_of (L~f)` & a in C & b in C))
  implies ((a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f))
  proof
  assume that
A3:  a in (L~f)` & b in (L~f)` and
A4:  not ex C be Subset of TOP-REAL 2 st
                   (C is_a_component_of (L~f)` & a in C & b in C);
A5:  a in LeftComp f \/ RightComp f by A3,GOBRD12:11;
A6:  b in LeftComp f \/ RightComp f by A3,GOBRD12:11;
  per cases by A5,XBOOLE_0:def 2;
  suppose A7: a in LeftComp f;
      now per cases by A6,XBOOLE_0:def 2;
      suppose b in LeftComp f;
      hence (a in LeftComp f & b in RightComp f) or
               (a in RightComp f & b in LeftComp f) by A1,A4,A7;
      suppose b in RightComp f;
      hence (a in LeftComp f & b in RightComp f) or
               (a in RightComp f & b in LeftComp f) by A7;
    end;
  hence (a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f);
  suppose A8: a in RightComp f;
      now per cases by A6,XBOOLE_0:def 2;
      suppose b in RightComp f;
      hence (a in LeftComp f & b in RightComp f) or
               (a in RightComp f & b in LeftComp f) by A2,A4,A8;
      suppose b in LeftComp f;
      hence (a in LeftComp f & b in RightComp f) or
               (a in RightComp f & b in LeftComp f) by A8;
    end;
  hence (a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f);
end;
  thus ((a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f)) implies
   a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
                           (C is_a_component_of (L~f)` & a in C & b in C))
   proof
     assume that A9: (a in LeftComp f & b in RightComp f) or
           (a in RightComp f & b in LeftComp f);
     thus a in (L~f)` & b in (L~f)`
     proof
A10:  RightComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
       LeftComp f c= LeftComp f \/ RightComp f by XBOOLE_1:7;
then A11:       LeftComp f c= (L~f)` by GOBRD12:11;
A12:       RightComp f c= (L~f)` by A10,GOBRD12:11;
       per cases by A9;
       suppose a in LeftComp f & b in RightComp f;
       hence thesis by A11,A12;
       suppose a in RightComp f & b in LeftComp f;
       hence thesis by A11,A12;
     end;
     thus (not ex C be Subset of TOP-REAL 2 st
                           (C is_a_component_of (L~f)` & a in C & b in C))
     proof
         now
         assume ex C be Subset of TOP-REAL 2 st
   (C is_a_component_of (L~f)` & a in C & b in C);
   then consider C be Subset of TOP-REAL 2 such that
A13:   (C is_a_component_of (L~f)` & a in C & b in C);
  now per cases by A9;
suppose A14: a in LeftComp f & b in RightComp f;
  now per cases by A1,A13,GOBOARD9:3;
suppose C = LeftComp f;
then not LeftComp f misses RightComp f by A13,A14,XBOOLE_0:3;
hence contradiction by GOBRD14:24;
suppose C misses LeftComp f;
hence contradiction by A13,A14,XBOOLE_0:3;
end;
hence contradiction;
suppose A15: a in RightComp f & b in LeftComp f;
  now per cases by A1,A13,GOBOARD9:3;
suppose C = LeftComp f;
then not LeftComp f misses RightComp f by A13,A15,XBOOLE_0:3;
hence contradiction by GOBRD14:24;
suppose C misses LeftComp f;
hence contradiction by A13,A15,XBOOLE_0:3;
end;
hence contradiction;
end;
hence contradiction;
  end;
    hence thesis;
  end;
 end;
end;

theorem Th17:
for f,a,b,c st
      ((ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) &
       (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C))) holds
       ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C)
proof
  let f be non constant standard special_circular_sequence,
      a,b,c such that
A1:      (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) and
A2:       (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C));
   per cases by A1,Th15;
   suppose A3: (a in RightComp f & b in RightComp f);
     now per cases by A2,Th15;
   suppose A4: (b in RightComp f & c in RightComp f);
     RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by A3,A4;
   suppose b in LeftComp f & c in LeftComp f;
   then LeftComp f meets RightComp f by A3,XBOOLE_0:3;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by GOBRD14:24;
   end;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C);
   suppose A5: a in LeftComp f & b in LeftComp f;
     now per cases by A2,Th15;
   suppose A6: b in LeftComp f & c in LeftComp f;
     LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by A5,A6;
   suppose b in RightComp f & c in RightComp f;
   then LeftComp f meets RightComp f by A5,XBOOLE_0:3;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by GOBRD14:24;
   end;
   hence thesis;
end;

theorem Th18:
for f,a,b,c st
   a in (L~f)` & b in (L~f)` & c in (L~f)` &
      ((not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) &
       (not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C))) holds
       ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C)
proof
  let f,a,b,c such that
A1:    a in (L~f)` & b in (L~f)` & c in (L~f)` and
A2:      (not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & b in C)) and
A3:       (not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & b in C & c in C));
A4:  LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A5:  RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
  per cases by A1,A2,Th16;
  suppose A6: a in LeftComp f & b in RightComp f;
    now per cases by A1,A3,Th16;
    suppose b in LeftComp f & c in RightComp f;
    then LeftComp f meets RightComp f by A6,XBOOLE_0:3;
    hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by GOBRD14:24;
    suppose b in RightComp f & c in LeftComp f;
    hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by A4,A6;
  end;
  hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C);
  suppose A7: a in RightComp f & b in LeftComp f;
    now per cases by A1,A3,Th16;
    suppose b in RightComp f & c in LeftComp f;
    then LeftComp f meets RightComp f by A7,XBOOLE_0:3;
    hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by GOBRD14:24;
    suppose b in LeftComp f & c in RightComp f;
    hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C) by A5,A7;
  end;
  hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & a in C & c in C);
end;

begin

reserve G for Go-board;

Lm4:now
  let G,i such that A1: i <= len G;
  let w1,w2 be Point of TOP-REAL 2 such that
A2:   w1 in v_strip(G,i) & w2 in v_strip(G,i) and
A3: w1`1 <= w2`1;
thus LSeg(w1,w2) c= v_strip(G,i)
proof
  let x such that
A4:  x in LSeg(w1,w2);
  reconsider p = x as Point of TOP-REAL 2 by A4;
A5: p = |[p`1, p`2]| by EUCLID:57;
A6:  w1`1 <= p`1 & p`1 <= w2`1 by A3,A4,TOPREAL1:9;
 per cases by A1,AXIOMS:21,RLVECT_1:99;
 suppose i = 0;
then A7: v_strip(G,i) = { |[r,s]| : r <= G*(1,1)`1 } by GOBRD11:18;
 then consider r1,s1 be Real such that
A8: w2 = |[r1,s1]| & r1 <= G*(1,1)`1 by A2;
    w2`1 <= G*(1,1)`1 by A8,EUCLID:56;
  then p`1 <= G*(1,1)`1 by A6,AXIOMS:22;
  hence x in v_strip(G,i) by A5,A7;
 suppose i = len G;
then A9: v_strip(G,i) = { |[r,s]| : G*(len G,1)`1 <= r } by GOBRD11:19;
 then consider r1,s1 be Real such that
A10: w1 = |[r1,s1]| & G*(len G,1)`1 <= r1 by A2;
    G*(len G,1)`1 <= w1`1 by A10,EUCLID:56;
  then G*(len G,1)`1 <= p`1 by A6,AXIOMS:22;
 hence x in v_strip(G,i) by A5,A9;
 suppose 1 <= i & i < len G;
then A11:v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
          by GOBRD11:20;
 then consider r1,s1 be Real such that
A12: w1 = |[r1,s1]| & G*(i,1)`1 <= r1 & r1 <= G*(i+1,1)`1 by A2;
   G*(i,1)`1 <= w1`1 & w1`1 <= G*(i+1,1)`1 by A12,EUCLID:56;
then A13:  G*(i,1)`1 <= p`1 by A6,AXIOMS:22;
 consider r2,s2 be Real such that
A14: w2 = |[r2,s2]| & G*(i,1)`1 <= r2 & r2 <= G*(i+1,1)`1 by A2,A11;
   G*(i,1)`1 <= w2`1 & w2`1 <= G*(i+1,1)`1 by A14,EUCLID:56;
 then p`1 <= G*(i+1,1)`1 by A6,AXIOMS:22;
 hence x in v_strip(G,i) by A5,A11,A13;
end;
end;

theorem Th19:
  i <= len G implies v_strip(G,i) is convex
proof
  assume A1: i<= len G;
  set P = v_strip(G,i);
  let w1,w2 be Point of TOP-REAL 2; assume
A2: w1 in P & w2 in P;
    w1`1 <= w2`1 or w2`1 <= w1`1;
  hence LSeg(w1,w2) c= P by A1,A2,Lm4;
end;

Lm5:now
  let G,j such that A1: j <= width G;
  let w1,w2 be Point of TOP-REAL 2 such that
A2:   w1 in h_strip(G,j) & w2 in h_strip(G,j) and
A3: w1`2 <= w2`2;
thus LSeg(w1,w2) c= h_strip(G,j)
proof
  let x; assume
A4:  x in LSeg(w1,w2);
  then reconsider p = x as Point of TOP-REAL 2;
A5: p = |[p`1, p`2]| by EUCLID:57;
A6:  w1`2 <= p`2 & p`2 <= w2`2 by A3,A4,TOPREAL1:10;
 per cases by A1,AXIOMS:21,RLVECT_1:99;
 suppose j = 0;
then A7: h_strip(G,j) = { |[r,s]| : s <= G*(1,1)`2 } by GOBRD11:21;
 then consider r1,s1 be Real such that
A8: w2 = |[r1,s1]| & s1 <= G*(1,1)`2 by A2;
    w2`2 <= G*(1,1)`2 by A8,EUCLID:56;
  then p`2 <= G*(1,1)`2 by A6,AXIOMS:22;
  hence x in h_strip(G,j) by A5,A7;
 suppose j = width G;
then A9: h_strip(G,j) = { |[r,s]| : G*(1,width G)`2 <= s } by GOBRD11:22;
 then consider r1,s1 be Real such that
A10: w1 = |[r1,s1]| & G*(1,width G)`2 <= s1 by A2;
    G*(1,width G)`2 <= w1`2 by A10,EUCLID:56;
  then G*(1,width G)`2 <= p`2 by A6,AXIOMS:22;
 hence x in h_strip(G,j) by A5,A9;
 suppose 1 <= j & j < width G;
then A11:h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
          by GOBRD11:23;
 then consider r1,s1 be Real such that
A12: w1 = |[r1,s1]| & G*(1,j)`2 <= s1 & s1 <= G*(1,j+1)`2 by A2;
   G*(1,j)`2 <= w1`2 & w1`2 <= G*(1,j+1)`2 by A12,EUCLID:56;
then A13:  G*(1,j)`2 <= p`2 by A6,AXIOMS:22;
 consider r2,s2 be Real such that
A14: w2 = |[r2,s2]| & G*(1,j)`2 <= s2 & s2 <= G*(1,j+1)`2 by A2,A11;
   G*(1,j)`2 <= w2`2 & w2`2 <= G*(1,j+1)`2 by A14,EUCLID:56;
 then p`2 <= G*(1,j+1)`2 by A6,AXIOMS:22;
 hence x in h_strip(G,j) by A5,A11,A13;
end;
end;

theorem Th20:
  j <= width G implies h_strip(G,j) is convex
proof
  assume A1: j<= width G;
  set P = h_strip(G,j);
  let w1,w2 be Point of TOP-REAL 2 such that
A2:   w1 in P & w2 in P;
    w1`2 <= w2`2 or w2`2 <= w1`2;
  hence LSeg(w1,w2) c= P by A1,A2,Lm5;
end;

theorem Th21:
 i <= len G & j <= width G implies cell(G,i,j) is convex
proof assume
A1: i <= len G & j <= width G;
A2:  cell(G,i,j) = v_strip(G,i) /\ h_strip(G,j) by GOBOARD5:def 3;
    v_strip(G,i) is convex & h_strip(G,j) is convex by A1,Th19,Th20;
 hence cell(G,i,j) is convex by A2,GOBOARD9:9;
end;

theorem Th22:
for f,k st 1<=k & k+1<=len f holds left_cell(f,k) is convex
proof
let f,k such that
A1: 1<=k & k+1<=len f;
 consider i,j such that
A2: i <= len GoB f & j <= width GoB f &
 cell(GoB f,i,j) = left_cell(f,k) by A1,GOBOARD9:14;
 thus left_cell(f,k) is convex by A2,Th21;
end;

theorem Th23:
for f,k st 1<=k & k+1<=len f holds
left_cell(f,k,GoB f) is convex & right_cell(f,k,GoB f) is convex
proof
let f,k such that
A1: 1<=k & k+1<=len f;
  left_cell(f,k) = left_cell(f,k,GoB f) by A1,JORDAN1H:27;
hence left_cell(f,k,GoB f) is convex by A1,Th22;
A2: len f = len Rev f by FINSEQ_5:def 3;
      k <= len f by A1,NAT_1:38;
then A3: len f-'k+k = len f by AMI_5:4;
then A4: len f-'k+1 <= len f by A1,AXIOMS:24;
A5: len f-'k >= 1 by A1,A3,REAL_1:53;
then A6: left_cell(Rev f,len f-'k) is convex by A2,A4,Th22;
   right_cell(f,k) = left_cell(Rev f,len f-'k) by A1,A3,A5,GOBOARD9:13;
 hence right_cell(f,k,GoB f) is convex by A1,A6,JORDAN1H:29;
end;

begin

theorem Th24:
for p1,p2,f
for r be Point of TOP-REAL 2 st
 (r in LSeg(p1,p2) &
 (ex x st (L~f) /\ LSeg(p1,p2) = {x}) &
 not r in L~f)
holds L~f misses LSeg(p1,r) or L~f misses LSeg(r,p2)
proof
let p1,p2,f;
let r be Point of TOP-REAL 2 such that
A1: r in LSeg(p1,p2) and
A2: (ex x st (L~f) /\ LSeg(p1,p2) = {x}) and
A3: not r in L~f;
consider p be set such that
A4: (L~f) /\ LSeg(p1,p2) = {p} by A2;
A5: p in {p} by TARSKI:def 1;
then A6: p in LSeg(p1,p2) by A4,XBOOLE_0:def 3;
 reconsider p as Point of TOP-REAL 2 by A4,A5;
   p1 in LSeg(p1,p2) by TOPREAL1:6;
then A7: LSeg(p1,r) c= LSeg(p1,p2) by A1,TOPREAL1:12;
  p2 in LSeg(p1,p2) by TOPREAL1:6;
then A8: LSeg(p2,r) c= LSeg(p1,p2) by A1,TOPREAL1:12;
A9: now
  A10: LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2) by A6,TOPREAL1:11;
  per cases by A1,A10,XBOOLE_0:def 2;
  suppose r in LSeg(p1,p);
  hence LSeg(p1,r) /\ LSeg(r,p) = {r} or
    LSeg(p,r) /\ LSeg(r,p2) = {r} by TOPREAL1:14;
  suppose r in LSeg(p,p2);
  hence LSeg(p1,r) /\ LSeg(r,p) = {r} or
    LSeg(p,r) /\ LSeg(r,p2) = {r} by TOPREAL1:14;
end;
  now
  assume A11: L~f meets LSeg(p1,r) & L~f meets LSeg(r,p2);
  per cases by A9;
  suppose A12: LSeg(p1,r) /\ LSeg(r,p) = {r};
  consider x such that
A13:  x in L~f & x in LSeg(p1,r) by A11,XBOOLE_0:3;
    x in L~f /\ LSeg(p1,p2) by A7,A13,XBOOLE_0:def 3;
  then x = p by A4,TARSKI:def 1;
  then x in LSeg(r,p) by TOPREAL1:6;
  then x in LSeg(p1,r) /\ LSeg(r,p) by A13,XBOOLE_0:def 3;
  hence contradiction by A3,A12,A13,TARSKI:def 1;
  suppose A14: LSeg(p,r) /\ LSeg(r,p2) = {r};
  consider x such that
A15:  x in L~f & x in LSeg(r,p2) by A11,XBOOLE_0:3;
    x in L~f /\ LSeg(p1,p2) by A8,A15,XBOOLE_0:def 3;
  then x = p by A4,TARSKI:def 1;
  then x in LSeg(p,r) by TOPREAL1:6;
  then x in LSeg(p,r) /\ LSeg(r,p2) by A15,XBOOLE_0:def 3;
  hence contradiction by A3,A14,A15,TARSKI:def 1;
end;
hence L~f misses LSeg(p1,r) or L~f misses LSeg(r,p2);
end;

Lm6:now
let p1,p2,f;
let r be Point of TOP-REAL 2 such that
A1: r in LSeg(p1,p2);
assume that
A2: ex x st (L~f) /\ LSeg(p1,p2) = {x} and
A3: not r in L~f;
per cases by A1,A2,A3,Th24;
  suppose L~f misses LSeg(p1,r);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by Th14;
  suppose L~f misses LSeg(r,p2);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by Th14;
end;

theorem Th25:
 for p,q,r,s being Point of TOP-REAL 2
  st LSeg(p,q) is vertical & LSeg(r,s) is vertical &
   LSeg(p,q) meets LSeg(r,s)
 holds p`1 = r`1
proof
 let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is vertical and
A2: LSeg(r,s) is vertical;
 assume LSeg(p,q) meets LSeg(r,s);
  then LSeg(p,q) /\ LSeg(r,s) <> {} by XBOOLE_0:def 7;
  then consider x being Point of TOP-REAL 2 such that
A3: x in LSeg(p,q) /\ LSeg(r,s) by SUBSET_1:10;
A4: x in LSeg(r,s) by A3,XBOOLE_0:def 3;
     x in LSeg(p,q) by A3,XBOOLE_0:def 3;
   hence p`1 = x`1 by A1,SPRECT_3:20
        .= r`1 by A2,A4,SPRECT_3:20;
end;

theorem Th26:
for p,p1,p2 st not p in LSeg(p1,p2) & p1`2 = p2`2 & p2`2 = p`2
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1)
proof
let p,p1,p2 such that
A1: not p in LSeg(p1,p2) and
A2: p1`2 = p2`2 & p2`2 = p`2;
per cases;
suppose A3: p1`1 <= p2`1;
  now per cases by A1,A2,GOBOARD7:9;
suppose p`1<p1`1;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A3,GOBOARD7:9;
suppose p2`1<p`1;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A3,GOBOARD7:9;
end;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
suppose A4: p2`1 <= p1`1;
  now per cases by A1,A2,GOBOARD7:9;
suppose p`1<p2`1;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A4,GOBOARD7:9;
suppose p1`1<p`1;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A4,GOBOARD7:9;
end;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
end;

theorem Th27:
for p,p1,p2 st not p in LSeg(p1,p2) & p1`1 = p2`1 & p2`1 = p`1
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1)
proof
let p,p1,p2 such that
A1: not p in LSeg(p1,p2) and
A2: p1`1 = p2`1 & p2`1 = p`1;
per cases;
suppose A3: p1`2 <= p2`2;
  now per cases by A1,A2,GOBOARD7:8;
suppose p`2<p1`2;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A3,GOBOARD7:8;
suppose p2`2<p`2;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A3,GOBOARD7:8;
end;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
suppose A4: p2`2 <= p1`2;
  now per cases by A1,A2,GOBOARD7:8;
suppose p`2<p2`2;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A4,GOBOARD7:8;
suppose p1`2<p`2;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1) by A2,A4,GOBOARD7:8;
end;
hence p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
end;

theorem Th28:
p <> p1 & p <> p2 & p in LSeg(p1,p2) implies not p1 in LSeg(p,p2)
proof
assume
A1: p <> p1 & p <> p2 & p in LSeg(p1,p2);
    then LSeg(p1,p) \/ LSeg(p,p2) = LSeg(p1,p2) by TOPREAL1:11;
then A2: LSeg(p,p1) c= LSeg(p1,p2) by XBOOLE_1:7;
  now
  assume p1 in LSeg(p,p2);
then A3:   LSeg(p,p1) \/ LSeg(p1,p2) = LSeg(p,p2) by TOPREAL1:11;
    LSeg(p,p1) \/ LSeg(p1,p2) = LSeg(p1,p2) by A2,XBOOLE_1:12;
  hence contradiction by A1,A3,SPPOL_1:25;
end;
hence not p1 in LSeg(p,p2);
end;

theorem Th29:
for p,p1,p2,q st not q in LSeg(p1,p2) &
               p in LSeg(p1,p2) & p <> p1 & p <> p2 &
     (p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2)
holds p1 in LSeg(q,p) or p2 in LSeg(q,p)
proof
let p,p1,p2,q such that
A1: not q in LSeg(p1,p2) and
A2: p in LSeg(p1,p2) and
A3: p <> p1 & p <> p2 and
A4: (p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2);
A5: not p1 in LSeg(p,p2) by A2,A3,Th28;
A6: not p2 in LSeg(p,p1) by A2,A3,Th28;
  per cases by A1,A4,Th26,Th27;
  suppose A7: p1 in LSeg(q,p2);
then A8: LSeg(q,p1) \/ LSeg(p1,p2) = LSeg(q,p2) by TOPREAL1:11;
      p in LSeg(q,p1) \/ LSeg(p1,p2) by A2,XBOOLE_0:def 2;
    then LSeg(q,p) \/ LSeg(p,p2) = LSeg(q,p2) by A8,TOPREAL1:11;
    hence p1 in LSeg(q,p) or p2 in LSeg(q,p) by A5,A7,XBOOLE_0:def 2;
    suppose A9: p2 in LSeg(q,p1);
then A10: LSeg(q,p2) \/ LSeg(p1,p2) = LSeg(q,p1) by TOPREAL1:11;
      p in LSeg(q,p2) \/ LSeg(p1,p2) by A2,XBOOLE_0:def 2;
    then LSeg(q,p) \/ LSeg(p,p1) = LSeg(q,p1) by A10,TOPREAL1:11;
    hence p1 in LSeg(q,p) or p2 in LSeg(q,p) by A6,A9,XBOOLE_0:def 2;
end;

theorem Th30:
for p1,p2,p3,p4,p be Point of TOP-REAL 2 st
(p1`1 = p2`1 & p3`1 = p4`1 or p1`2 = p2`2 & p3`2 = p4`2)
 & LSeg(p1,p2) /\ LSeg(p3,p4) = {p}
holds p=p1 or p=p2 or p=p3
proof
  let p1,p2,p3,p4,p be Point of TOP-REAL 2 such that
A1: (p1`1 = p2`1 & p3`1 = p4`1 or p1`2 = p2`2 & p3`2 = p4`2) and
A2: LSeg(p1,p2) /\ LSeg(p3,p4) = {p};
A3: p in LSeg(p1,p2) /\ LSeg(p3,p4) by A2,TARSKI:def 1;
then A4:LSeg(p1,p2) meets LSeg(p3,p4) by XBOOLE_0:4;
      p in LSeg(p3,p4) by A3,XBOOLE_0:def 3;
then LSeg(p3,p) \/ LSeg(p,p4) = LSeg(p3,p4) by TOPREAL1:11;
then A5: LSeg(p3,p) c= LSeg(p3,p4) by XBOOLE_1:7;
A6: p1 in LSeg(p1,p2) by TOPREAL1:6;
A7:p2 in LSeg(p1,p2) by TOPREAL1:6;
A8: p3 in LSeg(p3,p4) by TOPREAL1:6;
A9: now assume p1`1 = p2`1 & p3`1 = p4`1;
      then LSeg(p1,p2) is vertical & LSeg(p3,p4) is vertical by SPPOL_1:37;
      hence p2`1 = p3`1 by A4,Th25;
    end;
A10: now
      assume p1`2 = p2`2 & p3`2 = p4`2;
      then LSeg(p1,p2) is horizontal & LSeg(p3,p4) is horizontal by SPPOL_1:36
;
      hence p2`2 = p3`2 by A4,SPRECT_3:21;
    end;
  now
  assume A11: p<>p1 & p<>p2 & p<>p3;
A12:  p in LSeg(p1,p2) by A3,XBOOLE_0:def 3;
A13:now
    assume p3 in LSeg(p1,p2);
    then p3 in LSeg(p1,p2) /\ LSeg(p3,p4) by A8,XBOOLE_0:def 3;
    hence contradiction by A2,A11,TARSKI:def 1;
  end;
    now per cases by A1,A9,A10,A11,A12,A13,Th29;
  suppose p1 in LSeg(p3,p);
  then p1 in LSeg(p1,p2) /\ LSeg(p3,p4) by A5,A6,XBOOLE_0:def 3;
  hence contradiction by A2,A11,TARSKI:def 1;
  suppose p2 in LSeg(p3,p);
  then p2 in LSeg(p1,p2) /\ LSeg(p3,p4) by A5,A7,XBOOLE_0:def 3;
  hence contradiction by A2,A11,TARSKI:def 1;
  end;
  hence contradiction;
end;
hence p=p1 or p=p2 or p=p3;
end;

begin

theorem Th31:
for p,p1,p2,f st (L~f) /\ LSeg(p1,p2) = {p}
for r be Point of TOP-REAL 2 st not r in LSeg(p1,p2) &
          not p1 in L~f & not p2 in L~f &
 ((p1`1 = p2`1 & p1`1 = r`1) or (p1`2 = p2`2 & p1`2 = r`2)) &
 (ex i st (1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or
               r in left_cell(f,i,GoB f)) & p in LSeg(f,i))) &
 not r in L~f holds
    (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C))
proof
let p,p1,p2,f such that A1: (L~f) /\ LSeg(p1,p2) = {p};
let r be Point of TOP-REAL 2 such that
A2:not r in LSeg(p1,p2) and
A3: not p1 in L~f & not p2 in L~f and
A4: ((p1`1 = p2`1 & p1`1 = r`1) or (p1`2 = p2`2 & p1`2 = r`2)) and
A5: ex i st (1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or
               r in left_cell(f,i,GoB f)) & p in LSeg(f,i)) and
A6: not r in L~f;
A7: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i such that
A8:  1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or
             r in left_cell(f,i,GoB f)) & p in LSeg(f,i) by A5;
A9:LSeg(f,i) c= left_cell(f,i,GoB f) by A7,A8,JORDAN1H:26;
A10: LSeg(f,i) c= right_cell(f,i,GoB f) by A7,A8,JORDAN1H:28;
A11: p in L~f /\ LSeg(p1,p2) by A1,TARSKI:def 1;
then A12: p <> p2 & p <> p1 by A3,XBOOLE_0:def 3;
A13: p in LSeg(p1,p2) by A11,XBOOLE_0:def 3;
A14: right_cell(f,i,GoB f) is convex by A8,Th23;
A15: left_cell(f,i,GoB f) is convex by A8,Th23;
A16: right_cell(f,i,GoB f)\L~f c= RightComp f by A7,A8,JORDAN9:29;
A17: left_cell(f,i,GoB f)\L~f c= LeftComp f by A7,A8,JORDAN9:29;
A18: now
  assume r in right_cell(f,i,GoB f);
  then r in right_cell(f,i,GoB f)\L~f by A6,XBOOLE_0:def 4;
  hence r in RightComp f by A16;
end;
A19:now
  assume r in left_cell(f,i,GoB f);
  then r in left_cell(f,i,GoB f)\L~f by A6,XBOOLE_0:def 4;
  hence r in LeftComp f by A17;
end;
A20: now
  assume A21: p1 in LSeg(r,p) & r in right_cell(f,i,GoB f);
  then LSeg(r,p) c= right_cell(f,i,GoB f) by A8,A10,A14,JORDAN1:def 1;
  then p1 in right_cell(f,i,GoB f)\L~f by A3,A21,XBOOLE_0:def 4;
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) by A16,A18,A21,Th15;
end;
A22: now
  assume A23: p1 in LSeg(r,p) & r in left_cell(f,i,GoB f);
  then LSeg(r,p) c= left_cell(f,i,GoB f) by A8,A9,A15,JORDAN1:def 1;
  then p1 in left_cell(f,i,GoB f)\L~f by A3,A23,XBOOLE_0:def 4;
hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) by A17,A19,A23,Th15;
end;
A24: now
  assume A25: p2 in LSeg(r,p) & r in right_cell(f,i,GoB f);
  then LSeg(r,p) c= right_cell(f,i,GoB f) by A8,A10,A14,JORDAN1:def 1;
  then p2 in right_cell(f,i,GoB f)\L~f by A3,A25,XBOOLE_0:def 4;
  hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C) by A16,A18,A25,Th15;
end;
A26: now
  assume A27: p2 in LSeg(r,p) & r in left_cell(f,i,GoB f);
  then LSeg(r,p) c= left_cell(f,i,GoB f) by A8,A9,A15,JORDAN1:def 1;
  then p2 in left_cell(f,i,GoB f)\L~f by A3,A27,XBOOLE_0:def 4;
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by A17,A19,A27,Th15;
end;
  per cases by A2,A4,A12,A13,Th29;
  suppose A28: p1 in LSeg(r,p);
    now per cases by A8;
  suppose r in right_cell(f,i,GoB f);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by A20,A28;
  suppose r in left_cell(f,i,GoB f);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by A22,A28;
  end;
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C));
  suppose A29: p2 in LSeg(r,p);
    now per cases by A8;
  suppose r in right_cell(f,i,GoB f);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by A24,A29;
  suppose r in left_cell(f,i,GoB f);
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C)) by A26,A29;
  end;
  hence (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p1 in C)) or
     (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & r in C & p2 in C));
end;

theorem Th32:
for f,p1,p2,p st (L~f) /\ LSeg(p1,p2) = {p}
for rl,rp be Point of TOP-REAL 2 st
       not p1 in L~f & not p2 in L~f &
       ((p1`1 = p2`1 & p1`1 = rl`1 & rl`1 = rp`1) or
           (p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2)) &
      (ex i st (1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) &
          rp in right_cell(f,i,GoB f) & p in LSeg(f,i))) &
      not rl in L~f &
      not rp in L~f holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)
proof
let f,p1,p2,p such that A1:(L~f) /\ LSeg(p1,p2) = {p};
let rl,rp be Point of TOP-REAL 2;
assume that
A2: not p1 in L~f & not p2 in L~f and
A3: ((p1`1 = p2`1 & p1`1 = rl`1 & rl`1 = rp`1) or
    (p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2)) and
A4: ex i st (1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) &
       rp in right_cell(f,i,GoB f) & p in LSeg(f,i)) and
A5:not rl in L~f and
A6:not rp in L~f;
A7: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i such that
A8: 1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) &
          rp in right_cell(f,i,GoB f) by A4;
A9: rl in left_cell(f,i,GoB f)\L~f by A5,A8,XBOOLE_0:def 4;
A10: left_cell(f,i,GoB f)\L~f c= LeftComp f by A7,A8,JORDAN9:29;
A11: rp in right_cell(f,i,GoB f)\L~f by A6,A8,XBOOLE_0:def 4;
A12: right_cell(f,i,GoB f)\L~f c= RightComp f by A7,A8,JORDAN9:29;
A13:  not rl in RightComp f by A9,A10,GOBRD14:27;
A14: not rp in LeftComp f by A11,A12,GOBRD14:28;
A15: now
   assume A16: rl in LSeg(p1,p2);
per cases by A1,A5,A16,Lm6;
suppose (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rl in C & p1 in C));
hence p1 in LeftComp f or p2 in LeftComp f by A13,Th15;
suppose (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rl in C & p2 in C));
hence p1 in LeftComp f or p2 in LeftComp f by A13,Th15;
end;
A17:now
assume A18: rp in LSeg(p1,p2);
per cases by A1,A6,A18,Lm6;
suppose ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rp in C & p1 in C);
hence p1 in RightComp f or p2 in RightComp f by A14,Th15;
suppose ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rp in C & p2 in C);
hence p1 in RightComp f or p2 in RightComp f by A14,Th15;
end;
A19: now
assume A20: not rl in LSeg(p1,p2);
per cases by A1,A2,A3,A4,A5,A20,Th31;
suppose (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rl in C & p1 in C));
hence p1 in LeftComp f or p2 in LeftComp f by A13,Th15;
suppose (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rl in C & p2 in C));
hence p1 in LeftComp f or p2 in LeftComp f by A13,Th15;
end;
A21: now
assume A22: not rp in LSeg(p1,p2);
per cases by A1,A2,A3,A4,A6,A22,Th31;
suppose ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rp in C & p1 in C);
hence p1 in RightComp f or p2 in RightComp f by A14,Th15;
suppose (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & rp in C & p2 in C));
hence p1 in RightComp f or p2 in RightComp f by A14,Th15;
end;
A23: now
  assume A24: not rl in LSeg(p1,p2) & not rp in LSeg(p1,p2);
  per cases by A19,A24;
  suppose A25: p1 in LeftComp f;
    now per cases by A21,A24;
  suppose p1 in RightComp f;
  then LeftComp f meets RightComp f by A25,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  suppose p2 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A25,Th16;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
  suppose A26: p2 in LeftComp f;
    now per cases by A21,A24;
  suppose p1 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A26,Th16;
  suppose p2 in RightComp f;
  then LeftComp f meets RightComp f by A26,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;
A27:now
assume A28: rl in LSeg(p1,p2) & rp in LSeg(p1,p2);
  per cases by A15,A28;
  suppose A29: p1 in LeftComp f;
    now per cases by A17,A28;
  suppose p1 in RightComp f;
  then LeftComp f meets RightComp f by A29,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  suppose p2 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A29,Th16;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
  suppose A30: p2 in LeftComp f;
    now per cases by A17,A28;
  suppose p1 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A30,Th16;
  suppose p2 in RightComp f;
  then LeftComp f meets RightComp f by A30,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;
A31:now
  assume A32: rl in LSeg(p1,p2) & not rp in LSeg(p1,p2);
  per cases by A15,A32;
  suppose A33: p1 in LeftComp f;
    now per cases by A21,A32;
  suppose p1 in RightComp f;
  then LeftComp f meets RightComp f by A33,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  suppose p2 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A33,Th16;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
  suppose A34: p2 in LeftComp f;
    now per cases by A21,A32;
  suppose p1 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A34,Th16;
  suppose p2 in RightComp f;
  then LeftComp f meets RightComp f by A34,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;
A35:now
  assume A36: not rl in LSeg(p1,p2) & rp in LSeg(p1,p2);
  per cases by A19,A36;
  suppose A37: p1 in LeftComp f;
    now per cases by A17,A36;
  suppose p1 in RightComp f;
  then LeftComp f meets RightComp f by A37,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  suppose p2 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A37,Th16;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
  suppose A38: p2 in LeftComp f;
    now per cases by A17,A36;
  suppose p1 in RightComp f;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A38,Th16;
  suppose p2 in RightComp f;
  then LeftComp f meets RightComp f by A38,XBOOLE_0:3;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by GOBRD14:24;
  end;
  hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;
per cases;
suppose A39: rl in LSeg(p1,p2);
  now per cases;
suppose rp in LSeg(p1,p2);
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A27,A39;
suppose not rp in LSeg(p1,p2);
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A31,A39;
end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
suppose A40: not rl in LSeg(p1,p2);
  now per cases;
suppose rp in LSeg(p1,p2);
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A35,A40;
suppose not rp in LSeg(p1,p2);
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C) by A23,A40;
end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;

theorem Th33:
for p,f,p1,p2 st L~f /\ LSeg(p1,p2) = {p} &
                 (p1`1=p2`1 or p1`2=p2`2) &
                 not p1 in L~f & not p2 in L~f &
                 rng f misses LSeg(p1,p2) holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)
proof
  let p,f,p1,p2 such that A1:L~f /\ LSeg(p1,p2) = {p} and
A2:(p1`1=p2`1 or p1`2=p2`2);
  assume that
A3: not p1 in L~f & not p2 in L~f and
A4: rng f misses LSeg(p1,p2);
A5:p in {p} by TARSKI:def 1;
then A6: p in LSeg(p1,p2) by A1,XBOOLE_0:def 3;
A7: p in LSeg(p2,p1) by A1,A5,XBOOLE_0:def 3;
A8: f is_sequence_on GoB(f) by GOBOARD5:def 5;
      p in L~f by A1,A5,XBOOLE_0:def 3;
then p in union { LSeg(f,i) : 1 <= i & i+1 <= len f } by TOPREAL1:def 6;
    then consider LS be set such that
A9:    p in LS & LS in { LSeg(f,i) : 1 <= i & i+1 <= len f }
          by TARSKI:def 4;
   consider k such that
A10: LS = LSeg(f,k) & 1 <= k & k+1 <= len f by A9;
   set G = GoB f;
A11:now
  let r be Point of TOP-REAL 2;
  assume A12: r in Int right_cell(f,k,G);
    Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:44;
  hence r in right_cell(f,k,G) by A12;
    Int right_cell(f,k,G) misses L~f by A8,A10,JORDAN9:17;
  hence not r in L~f by A12,XBOOLE_0:3;
end;
A13:now
  let r be Point of TOP-REAL 2;
  assume A14: r in Int left_cell(f,k,G);
    Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:44;
  hence r in left_cell(f,k,G) by A14;
    Int left_cell(f,k,G) misses L~f by A8,A10,JORDAN9:17;
  hence not r in L~f by A14,XBOOLE_0:3;
end;
consider i1,j1,i2,j2 being Nat such that
A15:     [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A16:     [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A17:     (i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
       i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1) by A8,A10,JORDAN8:6;
       k < len f by A10,NAT_1:38;
then A18:  k in dom f by A10,FINSEQ_3:27;
     then f.k in rng f by FUNCT_1:12;
then A19:  f/.k in rng f by A18,FINSEQ_4:def 4;
  1<=k+1 by A10,NAT_1:38;
then A20: k+1 in dom f by A10,FINSEQ_3:27;
     then f.(k+1) in rng f by FUNCT_1:12;
then A21: f/.(k+1) in rng f by A20,FINSEQ_4:def 4;
     LSeg(f,k) c= L~f by TOPREAL3:26;
then A22:LSeg(p1,p2) /\ LSeg(f,k) = {p} by A1,A9,A10,SPRECT_2:2;
     LSeg(f,k) is vertical or LSeg(f,k) is horizontal by SPPOL_1:41;
   then LSeg(f/.k,f/.(k+1)) is vertical or LSeg(f/.k,f/.(k+1)) is horizontal
          by A10,TOPREAL1:def 5;
then A23: (f/.k)`1 =(f/.(k+1))`1 or (f/.k)`2 = (f/.(k+1))`2
           by SPPOL_1:36,37;
A24: LSeg(p1,p2) /\ LSeg(f/.k,f/.(k+1)) = {p} by A10,A22,TOPREAL1:def 5;
A25: p <> p1 & p <> p2 & p <> f/.k by A1,A3,A4,A5,A6,A19,XBOOLE_0:3,def 3;
then A26:  p1`2 = p2`2 implies i1 = i2 by A15,A16,A23,A24,Th30,JORDAN1G:7;
A27:  p1`1 = p2`1 implies j1 = j2 by A15,A16,A23,A24,A25,Th30,JORDAN1G:6;
A28: i2 <= len G by A16,GOBOARD5:1;
A29: 1 <= i2 by A16,GOBOARD5:1;
A30: i1 <= len G by A15,GOBOARD5:1;
A31: 1 <= i1 by A15,GOBOARD5:1;
A32: 1<=j1 by A15,GOBOARD5:1;
A33: j1 <= width G by A15,GOBOARD5:1;
A34:  j2 <= width G by A16,GOBOARD5:1;
A35: 1 <= j2 by A16,GOBOARD5:1;
A36: j1 -'1 < j1 by A32,JORDAN5B:1;
A37: i1 -'1 < i1 by A31,JORDAN5B:1;
A38: i2 -'1 < i2 by A29,JORDAN5B:1;
A39:p in LSeg(f/.(k+1),f/.k) by A9,A10,TOPREAL1:def 5;
A40:p <> f/.(k+1) by A4,A6,A21,XBOOLE_0:3;
A41: now
  assume A42: i1 = i2 & j1 = j2+1;
then A43:  1 <= j2+1 & j2+1<=width G by A15,GOBOARD5:1;
    j2 < j1 by A42,NAT_1:38;
then (f/.(k+1))`2 < (f/.k)`2 by A15,A16,A30,A31,A33,A35,A42,GOBOARD5:5;
  then (f/.(k+1))`2 < p`2 & p`2 < (f/.k)`2 by A25,A39,A40,TOPREAL6:38;
  hence G*(1,j2)`2 < p`2 & p`2 < G*(1,j2+1)`2
        by A15,A16,A30,A31,A34,A35,A42,A43,GOBOARD5:2;
end;
A44: now
  assume A45: i1 = i2 & j2 = j1+1;
  then j1 < j2 by NAT_1:38;
then (f/.k)`2 < (f/.(k+1))`2 by A15,A16,A30,A31,A32,A34,A45,GOBOARD5:5;
  then (f/.k)`2 < p`2 & p`2 < (f/.(k+1))`2 by A25,A39,A40,TOPREAL6:38;
  hence G*(1,j1)`2 < p`2 & p`2 < G*(1,j1+1)`2
        by A15,A16,A29,A30,A32,A33,A34,A35,A45,GOBOARD5:2;
end;
A46:now
  assume A47: j1 = j2 & i1 = i2+1;
  then i2 < i1 by NAT_1:38;
  then G*(i2,j1)`1 < G*(i1,j1)`1 by A29,A30,A32,A33,GOBOARD5:4;
    then (f/.(k+1))`1 < p`1 & p`1 < (f/.k)`1 by A15,A16,A25,A39,A40,A47,
TOPREAL6:37;
  hence G*(i2,1)`1 < p`1 & p`1 < G*(i2+1,1)`1
        by A15,A16,A28,A29,A30,A31,A34,A35,A47,GOBOARD5:3;
end;
A48:now
  assume A49: j1 = j2 & i2 = i1+1;
  then i1 < i2 by NAT_1:38;
then (f/.k)`1 < (f/.(k+1))`1 by A15,A16,A28,A31,A34,A35,A49,GOBOARD5:4;
  then (f/.k)`1 < p`1 & p`1 < (f/.(k+1))`1 by A25,A39,A40,TOPREAL6:37;
  hence G*(i1,1)`1 < p`1 & p`1 < G*(i1+1,1)`1
        by A15,A16,A28,A29,A30,A31,A33,A35,A49,GOBOARD5:3;
end;
A50: now
  assume A51:j1 = j2 & i2 = i1+1;
  hence Int left_cell(f,k,G)= Int cell(G,i1,j1)
           by A8,A10,A15,A16,GOBRD13:24;
  thus Int right_cell(f,k,G)= Int cell(G,i1,j1-'1)
           by A8,A10,A15,A16,A51,GOBRD13:25;
end;
A52: i2=i1+1 implies i1 < len G by A28,NAT_1:38;
A53: now
  assume 1 < j1 & i2 = i1+1;
  then 1 <= i1 & i1 < len G & 1 <= j1-'1 & j1-'1 < width G
           by A15,A28,A33,A36,AXIOMS:22,GOBOARD5:1,JORDAN3:12,NAT_1:38;
  hence Int cell(G,i1,j1-'1) =
    { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
                G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 } by GOBOARD6:29;
end;
A54: now
  assume A55: 1 = j1 & i2 = i1+1;
  then Int cell(G,i1,0) = Int cell(G,i1,j1-'1) by NAT_2:10;
  hence Int cell(G,i1,j1-'1) =
   { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & s < G*(1,1)`2 }
              by A31,A52,A55,GOBOARD6:27;
end;
A56: j1 < width G & i2 = i1+1 implies
  Int cell(G,i1,j1) =
    { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A31,A32,A52,GOBOARD6:29;
A57: j1 = width G & i2 = i1+1 implies
  Int cell(G,i1,j1) =
  { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & G*(1,width G)`2 < s }
     by A31,A52,GOBOARD6:28;
A58: i1=i2+1 implies i2 < len G by A30,NAT_1:38;
A59: now
  assume A60: j1 = j2 & i1 = i2+1;
  hence Int left_cell(f,k,G)= Int cell(G,i2,j1-'1)
        by A8,A10,A15,A16,GOBRD13:26;
  thus Int right_cell(f,k,G)= Int cell(G,i2,j1)
        by A8,A10,A15,A16,A60,GOBRD13:27;
end;
A61: now assume 1 < j1 & i1 = i2+1;
  then 1 <= i2 & i2 < len G & 1 <= j1-'1 & j1-'1 < width G
            by A16,A30,A33,A36,AXIOMS:22,GOBOARD5:1,JORDAN3:12,NAT_1:38;
  hence Int cell(G,i2,j1-'1) =
    { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
                G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 } by GOBOARD6:29;
end;
A62: now assume A63: 1 = j1 & i1 = i2+1;
  then Int cell(G,i2,0) = Int cell(G,i2,j1-'1) by NAT_2:10;
  hence Int cell(G,i2,j1-'1) =
     { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & s < G*(1,1)`2 }
        by A29,A58,A63,GOBOARD6:27;
end;
A64: j1 < width G & i1 = i2+1 implies Int cell(G,i2,j1) =
    { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A29,A32,A58,GOBOARD6:29;
A65: j1 = width G & i1 = i2+1 implies Int cell(G,i2,j1) =
  { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & G*(1,width G)`2 < s }
       by A29,A58,GOBOARD6:28;
A66: j2=j1+1 implies j1 < width G by A34,NAT_1:38;
A67: now
  assume A68: i1 = i2 & j2 = j1+1;
  hence Int left_cell(f,k,G)= Int cell(G,i1-'1,j1)
           by A8,A10,A15,A16,GOBRD13:22;
  thus Int right_cell(f,k,G)= Int cell(G,i1,j1) by A8,A10,A15,A16,A68,GOBRD13:
23;
end;
A69: now
  assume 1 < i1 & j2 = j1+1;
  then 1 <= i1-'1 & i1-'1 < len G & 1 <= j1 & j1 < width G
             by A15,A30,A34,A37,AXIOMS:22,GOBOARD5:1,JORDAN3:12,NAT_1:38;
  hence Int cell(G,i1-'1,j1) =
    { |[r,s]| : G*(i1-'1,1)`1 < r & r < G*(i1-'1+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by GOBOARD6:29;
end;
A70: now
  assume A71: 1 = i1 & j2 = j1+1;
  then Int cell(G,i1-'1,j1) = Int cell(G,0,j1) by NAT_2:10;
  hence Int cell(G,i1-'1,j1) =
     { |[r,s]| : r < G*(1,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 }
        by A32,A66,A71,GOBOARD6:23;
end;
A72: i1 < len G & j2 = j1+1 implies Int cell(G,i1,j1) =
    { |[r,s]| : G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 } by A31,A32,A66,GOBOARD6:29;
A73: i1 = len G & j2 = j1+1 implies Int cell(G,i1,j1) =
   { |[r,s]| : G*(len G,1)`1 < r & G*(1,j1)`2 < s & s < G*(1,j1+1)`2 }
        by A32,A66,GOBOARD6:26;
A74: j1=j2+1 implies j2 < width G by A33,NAT_1:38;
A75: now
  assume A76: i1 = i2 & j1 = j2+1;
  hence Int right_cell(f,k,G)= Int cell(G,i2-'1,j2)
           by A8,A10,A15,A16,GOBRD13:29;
  thus Int left_cell(f,k,G)= Int cell(G,i2,j2) by A8,A10,A15,A16,A76,GOBRD13:28
;
end;
A77: now
  assume 1 < i2 & j1 = j2+1;
  then 1 <= i2-'1 & i2-'1 < len G & 1 <= j2 & j2 < width G
             by A16,A28,A33,A38,AXIOMS:22,GOBOARD5:1,JORDAN3:12,NAT_1:38;
  hence Int cell(G,i2-'1,j2) =
    { |[r,s]| : G*(i2-'1,1)`1 < r & r < G*(i2-'1+1,1)`1 &
                G*(1,j2)`2 < s & s < G*(1,j2+1)`2 } by GOBOARD6:29;
end;
A78: now
  assume A79: 1 = i2 & j1 = j2+1;
  then Int cell(G,i2-'1,j2) = Int cell(G,0,j2) by NAT_2:10;
  hence Int cell(G,i2-'1,j2) =
     { |[r,s]| : r < G*(1,1)`1 & G*(1,j2)`2 < s & s < G*(1,j2+1)`2 }
       by A35,A74,A79,GOBOARD6:23;
end;
A80: i2 < len G & j1 = j2+1 implies Int cell(G,i2,j2) =
    { |[r,s]| : G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
                G*(1,j2)`2 < s & s < G*(1,j2+1)`2 } by A29,A35,A74,GOBOARD6:29;
A81: i2 = len G & j1 = j2+1 implies
  Int cell(G,i2,j2) =
   { |[r,s]| : G*(len G,1)`1 < r & G*(1,j2)`2 < s & s < G*(1,j2+1)`2 }
            by A35,A74,GOBOARD6:26;
per cases by A2;
suppose A82:p1`2=p2`2;
then A83: p`2 = p1`2 by A7,GOBOARD7:6;
  Int left_cell(f,k,G) <> {} by A8,A10,JORDAN9:11;
then consider rl' be set such that
A84:   rl' in Int left_cell(f,k,G) by XBOOLE_0:def 1;
  reconsider rl' as Point of TOP-REAL 2 by A84;
  reconsider rl = |[rl'`1,p`2]| as Point of TOP-REAL 2;
A85: rl`2=p`2 & rl`1=rl'`1 by EUCLID:56;
  Int right_cell(f,k,G) <> {} by A8,A10,JORDAN9:11;
then consider rp' be set such that
A86:   rp' in Int right_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rp' as Point of TOP-REAL 2 by A86;
reconsider rp = |[rp'`1,p`2]| as Point of TOP-REAL 2;
A87: rp`2=p`2 & rp`1=rp'`1 by EUCLID:56;
A88: now
  assume A89: j1=j2+1 & i2 < len G;
  then ex r,s st rl' = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
                G*(1,j2)`2 < s & s < G*(1,j2+1)`2 by A15,A16,A23,A24,A25,A75,
A80,A82,A84,Th30,JORDAN1G:7;
  then G*(i2,1)`1 < rl`1 & rl`1 < G*(i2+1,1)`1
     & G*(1,j2)`2 < p`2 & p`2 < G*(1,j2+1)`2 by A15,A16,A23,A24,A25,A41,A82,A85
,A89,Th30,EUCLID:56,JORDAN1G:7;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A75,A80,A82,A85,A89,
Th30,JORDAN1G:7;
end;
A90: now
  assume A91: j1=j2+1 & i2 = len G;
 then ex r,s st rl' = |[r,s]| & G*(len G,1)`1 < r & G*(1,j2)`2 < s &
                   s < G*(1,j2+1)`2 by A15,A16,A23,A24,A25,A75,A81,A82,A84,Th30
,JORDAN1G:7;
  then G*(len G,1)`1 < rl`1
     & G*(1,j2)`2 < p`2 & p`2 < G*(1,j2+1)`2 by A15,A16,A23,A24,A25,A41,A82,A85
,A91,Th30,EUCLID:56,JORDAN1G:7;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A75,A81,A82,A85,A91,
Th30,JORDAN1G:7;
end;
A92: now
  assume A93: j1=j2+1 & 1 = i2;
  then ex r,s st rp' = |[r,s]| & r < G*(1,1)`1 & G*(1,j2)`2 < s & s < G*(1,j2+
1)`2
           by A15,A16,A23,A24,A25,A75,A78,A82,A86,Th30,JORDAN1G:7;
  then rp'`1 < G*(1,1)`1 by EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A41,A75,A78,A82,A93,
Th30,JORDAN1G:7;
end;
A94: now
  assume A95: j1=j2+1 & 1 < i2;
  then ex r,s st rp' = |[r,s]| & G*(i2-'1,1)`1 < r & r < G*(i2-'1+1,1)`1 &
                G*(1,j2)`2 < s & s < G*(1,j2+1)`2 by A15,A16,A23,A24,A25,A75,
A77,A82,A86,Th30,JORDAN1G:7;
  then G*(i2-'1,1)`1 < rp'`1 & rp'`1 < G*(i2-'1+1,1)`1 by EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A41,A75,A77,A82,A95,
Th30,JORDAN1G:7;
end;
A96: now
  assume A97: j2=j1+1 & i1 < len G;
  then ex r,s st rp' = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 by A15,A16,A23,A24,A25,A67,
A72,A82,A86,Th30,JORDAN1G:7;
  then G*(i1,1)`1 < rp'`1 & rp'`1 < G*(i1+1,1)`1 by EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A44,A67,A72,A82,A97,
Th30,JORDAN1G:7;
end;
A98: now
  assume A99: j2=j1+1 & i1 = len G;
  then ex r,s st rp' = |[r,s]| & G*(len G,1)`1 < r & G*(1,j1)`2 < s &
                   s < G*(1,j1+1)`2 by A15,A16,A23,A24,A25,A67,A73,A82,A86,Th30
,JORDAN1G:7;
  then G*(len G,1)`1 < rp'`1 by EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A44,A67,A73,A82,A99,
Th30,JORDAN1G:7;
end;
A100: now
  assume A101: j2=j1+1 & 1 = i1;
  then ex r,s st rl' = |[r,s]| & r < G*(1,1)`1 & G*(1,j1)`2 < s & s < G*(1,j1+
1)`2
           by A15,A16,A23,A24,A25,A67,A70,A82,A84,Th30,JORDAN1G:7;
  then rl'`1 < G*(1,1)`1 by EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A44,A67,A70,A82,A101,
Th30,JORDAN1G:7;
end;
A102: now
  assume A103: j2=j1+1 & 1 < i1;
  then ex r,s st rl' = |[r,s]| & G*(i1-'1,1)`1 < r & r < G*(i1-'1+1,1)`1 &
                G*(1,j1)`2 < s & s < G*(1,j1+1)`2 by A15,A16,A23,A24,A25,A67,
A69,A82,A84,Th30,JORDAN1G:7;
  then G*(i1-'1,1)`1 < rl'`1 & rl'`1 < G*(i1-'1+1,1)`1 by EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A44,A67,A69,A82,A103,
Th30,JORDAN1G:7;
end;
  now per cases by A17,A26,A82,NAT_1:38;
suppose A104: j1=j2+1;
A105: rl in Int left_cell(f,k,G)
proof
  per cases by A28,REAL_1:def 5;
  suppose i2 < len G;
  hence thesis by A88,A104;
  suppose i2 = len G;
  hence thesis by A90,A104;
end;
A106: rp in Int right_cell(f,k,GoB f)
proof
  per cases by A29,REAL_1:def 5;
  suppose 1 < i2;
  hence thesis by A94,A104;
  suppose 1 = i2;
  hence thesis by A92,A104;
end;
A107: rl in left_cell(f,k,GoB f) by A13,A105;
A108: rp in right_cell(f,k,GoB f) by A11,A106;
A109: not rl in L~f by A13,A105;
  not rp in L~f by A11,A106;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)
       by A1,A3,A9,A10,A82,A83,A85,A87,A107,A108,A109,Th32;
suppose A110: j2=j1+1;
A111: rl in Int left_cell(f,k,G)
proof
  per cases by A31,REAL_1:def 5;
  suppose 1 < i1;
  hence thesis by A102,A110;
  suppose 1 = i1;
  hence thesis by A100,A110;
end;
A112: rp in Int right_cell(f,k,GoB f)
proof
  per cases by A30,REAL_1:def 5;
  suppose i1 < len G;
  hence thesis by A96,A110;
  suppose i1 = len G;
  hence thesis by A98,A110;
end;
A113: rl in left_cell(f,k,GoB f) by A13,A111;
A114: rp in right_cell(f,k,GoB f) by A11,A112;
A115: not rl in L~f by A13,A111;
       not rp in L~f by A11,A112;
   hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
        & p1 in C & p2 in C) by A1,A3,A9,A10,A82,A83,A85,A87,A113,A114,A115,
Th32;
end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
suppose A116: p1`1=p2`1;
then A117: p`1 = p1`1 by A7,GOBOARD7:5;
  Int left_cell(f,k,G) <> {} by A8,A10,JORDAN9:11;
then consider rl' be set such that
A118:   rl' in Int left_cell(f,k,G) by XBOOLE_0:def 1;
reconsider rl' as Point of TOP-REAL 2 by A118;
reconsider rl = |[p`1,rl'`2]| as Point of TOP-REAL 2;
A119: rl`1=p`1 & rl`2=rl'`2 by EUCLID:56;
  Int right_cell(f,k,G) <> {} by A8,A10,JORDAN9:11;
then consider rp' be set such that
A120:   rp' in Int right_cell(f,k,G) by XBOOLE_0:def 1;
  reconsider rp' as Point of TOP-REAL 2 by A120;
  reconsider rp = |[p`1,rp'`2]| as Point of TOP-REAL 2;
A121: rp`1=p`1 & rp`2=rp'`2 by EUCLID:56;
A122: now
  assume A123: i1=i2+1 & j1 < width G;
  then ex r,s st rp' = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
        G*(1,j1)`2 < s & s < G*(1,j1+1)`2 by A15,A16,A23,A24,A25,A59,A64,A116,
A120,Th30,JORDAN1G:6;
  then G*(1,j1)`2 < rp`2 & rp`2 < G*(1,j1+1)`2 by A121,EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A46,A59,A64,A116,
A121,A123,Th30,JORDAN1G:6;
end;
A124: now
  assume A125: i1=i2+1 & j1 = width G;
 then ex r,s st rp' = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
         G*(1,width G)`2 < s by A15,A16,A23,A24,A25,A59,A65,A116,A120,Th30,
JORDAN1G:6;
  then G*(i2,1)`1 < p`1 & p`1 < G*(i2+1,1)`1 & G*(1,width G)`2 < rp`2
          by A15,A16,A23,A24,A25,A46,A116,A121,A125,Th30,EUCLID:56,JORDAN1G:6;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A59,A65,A116,A121,
A125,Th30,JORDAN1G:6;
end;
A126: now
  assume A127: i1=i2+1 & 1 = j1;
 then ex r,s st rl' = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 & s < G*(1,
1)`2
              by A15,A16,A23,A24,A25,A59,A62,A116,A118,Th30,JORDAN1G:6;
  then rl`2 < G*(1,1)`2 by A119,EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A46,A59,A62,A116,A119
,A127,Th30,JORDAN1G:6;
end;
A128: now
  assume A129: i1=i2+1 & 1 < j1;
  then ex r,s st rl' = |[r,s]| & G*(i2,1)`1 < r & r < G*(i2+1,1)`1 &
    G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 by A15,A16,A23,A24,A25,A59,A61,A116
,A118,Th30,JORDAN1G:6;
  then G*(1,j1-'1)`2 < rl'`2 & rl'`2 < G*(1,j1-'1+1)`2 by EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A46,A59,A61,A116,A129
,Th30,JORDAN1G:6;
end;
A130: now
  assume A131: i2=i1+1 & j1 < width G;
  then ex r,s st rl' = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
     G*(1,j1)`2 < s & s < G*(1,j1+1)`2 by A15,A16,A23,A24,A25,A50,A56,A116,A118
,Th30,JORDAN1G:6;
  then G*(1,j1)`2 < rl`2 & rl`2 < G*(1,j1+1)`2 by A119,EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A48,A50,A56,A116,A119
,A131,Th30,JORDAN1G:6;
end;
A132: now
  assume A133: i2=i1+1 & j1 = width G;
 then ex r,s st rl' = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
         G*(1,width G)`2 < s by A15,A16,A23,A24,A25,A50,A57,A116,A118,Th30,
JORDAN1G:6;
  then G*(1,width G)`2 < rl'`2 by EUCLID:56;
  hence rl in Int left_cell(f,k,G) by A15,A16,A23,A24,A25,A48,A50,A57,A116,A133
,Th30,JORDAN1G:6;
end;
A134: now
  assume A135: i2=i1+1 & 1 = j1;
 then ex r,s st rp' = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 & s < G*(1,
1)`2
              by A15,A16,A23,A24,A25,A50,A54,A116,A120,Th30,JORDAN1G:6;
  then rp'`2 < G*(1,1)`2 by EUCLID:56;
hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A48,A50,A54,A116,A135,
Th30,JORDAN1G:6;
end;
A136: now
  assume A137: i2=i1+1 & 1 < j1;
  then ex r,s st rp' = |[r,s]| & G*(i1,1)`1 < r & r < G*(i1+1,1)`1 &
   G*(1,j1-'1)`2 < s & s < G*(1,j1-'1+1)`2 by A15,A16,A23,A24,A25,A50,A53,A116,
A120,Th30,JORDAN1G:6;
  then G*(1,j1-'1)`2 < rp'`2 & rp'`2 < G*(1,j1-'1+1)`2 by EUCLID:56;
  hence rp in Int right_cell(f,k,G) by A15,A16,A23,A24,A25,A48,A50,A53,A116,
A137,Th30,JORDAN1G:6;
end;
  now per cases by A17,A27,A116,NAT_1:38;
suppose A138: i1=i2+1;
A139: rl in Int left_cell(f,k,G)
proof
  per cases by A32,REAL_1:def 5;
  suppose 1 < j1;
  hence thesis by A128,A138;
  suppose 1 = j1;
  hence thesis by A126,A138;
end;
A140: rp in Int right_cell(f,k,GoB f)
proof
  per cases by A33,REAL_1:def 5;
  suppose j1 < width G;
  hence thesis by A122,A138;
  suppose j1 = width G;
  hence thesis by A124,A138;
end;
A141: rl in left_cell(f,k,GoB f) by A13,A139;
A142: rp in right_cell(f,k,GoB f) by A11,A140;
A143: not rl in L~f by A13,A139;
   not rp in L~f by A11,A140;
 hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)
       by A1,A3,A9,A10,A116,A117,A119,A121,A141,A142,A143,Th32;
suppose A144: i2=i1+1;
A145: rp in Int right_cell(f,k,G)
proof
  per cases by A32,REAL_1:def 5;
  suppose 1 < j1;
  hence thesis by A136,A144;
  suppose 1 = j1;
  hence thesis by A134,A144;
end;
A146: rl in Int left_cell(f,k,GoB f)
proof
  per cases by A33,REAL_1:def 5;
  suppose j1 < width G;
  hence thesis by A130,A144;
  suppose j1 = width G;
  hence thesis by A132,A144;
end;
then A147: rl in left_cell(f,k,GoB f) by A13;
A148: rp in right_cell(f,k,GoB f) by A11,A145;
A149: not rl in L~f by A13,A146;
     not rp in L~f by A11,A145;
   hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C)
       by A1,A3,A9,A10,A116,A117,A119,A121,A147,A148,A149,Th32;
end;
hence not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & p1 in C & p2 in C);
end;

theorem Th34:
for f being non constant standard special_circular_sequence,
    g being special FinSequence of TOP-REAL 2 st f,g are_in_general_position
for k st 1<=k & k+1<= len g holds
      Card (L~f /\ LSeg(g,k)) is even Nat iff
          ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & g.k in C & g.(k+1) in C)
proof
  let f be non constant standard special_circular_sequence,
      g being special FinSequence of TOP-REAL 2 such that
A1:     f,g are_in_general_position;
  let k such that
A2:  1<=k & k+1<= len g;
A3: k < len g by A2,NAT_1:38;
A4:f is_in_general_position_wrt g by A1,Def2;
then A5: L~f misses rng g by Def1;
A6:g is_in_general_position_wrt f by A1,Def2;
A7: 1<=k+1 by A2,NAT_1:38;
A8: k in dom g by A2,A3,FINSEQ_3:27;
A9:k+1 in dom g by A2,A7,FINSEQ_3:27;
   set m = L~f /\ LSeg(g,k);
A10: g/.k = g.k by A8,FINSEQ_4:def 4;
A11: g.k in rng g by A8,FUNCT_1:12;
A12: rng g c= the carrier of TOP-REAL 2 by FINSEQ_1:def 4;
   then reconsider gk = g.k as Point of TOP-REAL 2 by A11;
     g.(k+1) in rng g by A9,FUNCT_1:12;
   then reconsider gk1 = g.(k+1) as Point of TOP-REAL 2 by A12;
A13: g/.(k+1) = g.(k+1) by A9,FINSEQ_4:def 4;
then LSeg(gk,gk1) = LSeg(g,k) by A2,A10,TOPREAL1:def 5;
then A14:  LSeg(g,k) is connected Subset of TOP-REAL 2 by GOBOARD9:8;
A15:  g.k in LSeg(g,k) by A2,A10,TOPREAL1:27;
A16:  g.(k+1) in LSeg(g,k) by A2,A13,TOPREAL1:27;
A17: g.k in (L~f)` by A1,A2,Th9;
then A18: not g.k in (L~f) by SUBSET_1:54;
A19:g.(k+1) in (L~f)` by A1,A2,Th9;
then A20: not g.(k+1) in (L~f) by SUBSET_1:54;
     set p1 = g/.k, p2 = g/.(k+1);
A21:  LSeg(g,k) = LSeg(p1,p2) by A2,TOPREAL1:def 5;
    LSeg(g,k) is vertical or LSeg(g,k) is horizontal by SPPOL_1:41;
then A22:(p1`1=p2`1 or p1`2=p2`2) by A21,SPPOL_1:36,37;
   per cases;
   suppose A23: not m = {};
   m is trivial by A2,A3,A4,Def1;
   then consider x such that
A24:  m = {x} by A23,REALSET1:def 12;
  x in m by A24,TARSKI:def 1;
   then reconsider p = x as Point of TOP-REAL 2;
A25: p1 = g.k & p2 = g.(k+1) by A8,A9,FINSEQ_4:def 4;
A26: L~f /\ LSeg(p1,p2) = {p} by A2,A24,TOPREAL1:def 5;
A27: p1 in rng g & p2 in rng g by A8,A9,A25,FUNCT_1:12;
A28: now
  assume A29: not (not p1 in L~f & not p2 in L~f);
  per cases by A29;
  suppose p1 in L~f;
  hence contradiction by A5,A27,XBOOLE_0:3;
  suppose p2 in L~f;
  hence contradiction by A5,A27,XBOOLE_0:3;
end;
A30: rng f misses L~g by A6,Def1;
     LSeg(g,k) c= L~g by TOPREAL3:26;
   then rng f misses LSeg(p1,p2) by A21,A30,XBOOLE_1:63;
   hence Card (L~f /\ LSeg(g,k)) is even Nat iff
          ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & g.k in C & g.(k+1) in C)
                  by A22,A24,A25,A26,A28,Th3,Th33,CARD_1:79;
   suppose A31: m = {};
then A32:Card m = 2*0 by CARD_1:47;
A33: LSeg(g,k) misses L~f by A31,XBOOLE_0:def 7;
then A34: not (g.(k+1) in RightComp f & g.k in LeftComp f)
          by A14,A15,A16,JORDAN1J:36;
     now per cases by A14,A15,A16,A33,JORDAN1J:36;
   suppose A35: not gk in RightComp f;
then A36:   gk in LeftComp f by A18,GOBRD14:27;
A37:   g.(k+1) in LeftComp f by A18,A19,A20,A34,A35,GOBRD14:27;
     LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & g.k in C & g.(k+1) in C) by A36,A37;
   suppose A38: not g.(k+1) in LeftComp f;
then A39:  g.(k+1) in RightComp f by A19,A20,GOBRD14:28;
A40:   g.k in RightComp f by A17,A18,A19,A20,A34,A38,GOBRD14:28;
     RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
   hence ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
              & g.k in C & g.(k+1) in C) by A39,A40;
   end;
   hence thesis by A32;
end;

theorem Th35:
for f1,f2,g1 being special FinSequence of TOP-REAL 2
  st f1 ^' f2 is non constant standard special_circular_sequence &
     f1 ^' f2, g1 are_in_general_position & len g1 >= 2 &
     g1 is unfolded s.n.c. holds
     Card (L~(f1 ^' f2) /\ L~g1) is even Nat iff
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
        & g1.1 in C & g1.len g1 in C
proof
  let f1,f2,g1 being special FinSequence of TOP-REAL 2
    such that
A1:     f1 ^' f2 is non constant standard special_circular_sequence &
            f1 ^' f2, g1 are_in_general_position and
A2:len g1 >= 2 and
A3: g1 is unfolded s.n.c.;
  reconsider g1 as special unfolded s.n.c. FinSequence of TOP-REAL 2 by A3;
  set Lf = L~(f1 ^' f2);
    (f1 ^' f2) is_in_general_position_wrt g1 by A1,Def2;
then A4: Lf misses rng g1 by Def1;
  defpred P[Nat] means
   $1 <= len g1 implies for a being FinSequence of TOP-REAL 2 st
    a = g1|(Seg $1) holds
     ( (Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2 st
       C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)) );
A5: 1+1<=len g1 by A2;
A6: dom g1 = Seg len g1 by FINSEQ_1:def 3;
A7: 1 <= len g1 by A2,AXIOMS:22;
then A8: 1 in dom g1 by FINSEQ_3:27;
A9: 2 in dom g1 by A2,FINSEQ_3:27;
  now
  let a being FinSequence of TOP-REAL 2 such that
A10:    a = g1|(Seg 2);
      g1|1 = g1|(Seg 1) by TOPREAL1:def 1;
then A11: len (g1|1) = 1 by A7,FINSEQ_1:21;
A12:L~a = L~(g1|2) by A10,TOPREAL1:def 1
       .= L~(g1|1) \/ LSeg(g1/.1,g1/.(1+1)) by A8,A9,TOPREAL3:45
       .= L~(g1|1) \/ LSeg(g1,1) by A2,TOPREAL1:def 5
       .= {} \/ LSeg(g1,1) by A11,TOPREAL1:28
       .= LSeg(g1,1);
A13:2 in Seg 2 by FINSEQ_1:4,TARSKI:def 2;
      1 in Seg 2 by FINSEQ_1:4,TARSKI:def 2;
then A14:a.1 = g1.1 by A10,FUNCT_1:72;
      a.(len a) = a.2 by A2,A10,FINSEQ_1:21
              .= g1.(1+1) by A10,A13,FUNCT_1:72;
    hence ((Card (Lf /\ L~a) is even Nat iff
        (ex C be Subset of TOP-REAL 2 st
           C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)) )
             by A1,A2,A12,A14,Th34;
end;
then A15: P[2];
A16: now
let k such that
A17: k>=2 and
A18: P[k];
A19:1<=k by A17,AXIOMS:22;
then A20: 1<=k+1 by NAT_1:38;
  now
  assume that
A21: k+1 <= len g1;
  let a being FinSequence of TOP-REAL 2 such that
A22:  a = g1|(Seg (k+1));
A23:  k < len g1 by A21,NAT_1:38;
A24: k+1 in Seg len g1 by A20,A21,FINSEQ_1:3;
A25: k in dom g1 & k+1 in dom g1 by A6,A19,A20,A21,A23,FINSEQ_1:3;
A26:k+1 in Seg (k+1) by A20,FINSEQ_1:3;
      1 in Seg (k+1) by A20,FINSEQ_1:3;
then A27:g1.1 = a.1 by A22,FUNCT_1:72;
A28: g1.1 in Lf` by A1,A5,Th9;
A29: g1.(k+1) in Lf` by A1,A19,A21,Th9;
A30: g1.k in Lf` by A1,A19,A21,Th9;
A31:len a = k+1 by A21,A22,FINSEQ_1:21;
A32:g1.(k+1) = a.(k+1) by A22,A26,FUNCT_1:72
             .= a.(len a) by A21,A22,FINSEQ_1:21;
A33: (f1 ^' f2),a are_in_general_position by A1,A22,Th7;
     reconsider b = g1|Seg k as FinSequence of TOP-REAL 2 by FINSEQ_1:23;
A34:  (f1 ^' f2),b are_in_general_position by A1,Th7;
A35:k in Seg k by A19,FINSEQ_1:3;
       1 in Seg k by A19,FINSEQ_1:3;
then A36: b.1 = g1.1 by FUNCT_1:72;
A37: b.(len b) = b.k by A23,FINSEQ_1:21
               .= g1.k by A35,FUNCT_1:72;
   set c = LSeg(g1,k);
   reconsider s1 = Lf /\ L~b as finite set by A34,Th12;
   reconsider s2 = Lf /\ c as finite set by A1,Th13;
   reconsider s = Lf /\ L~a as finite set by A33,Th12;
     a = g1|(k+1) by A22,TOPREAL1:def 1;
then L~a = L~(g1|k) \/ LSeg(g1/.k,g1/.(k+1)) by A25,TOPREAL3:45
     .= L~b \/ LSeg(g1/.k,g1/.(k+1)) by TOPREAL1:def 1
     .= L~b \/ c by A19,A21,TOPREAL1:def 5;
then A38: s = s1 \/ s2 by XBOOLE_1:23;
A39: g1|(k+1) = a by A22,TOPREAL1:def 1;
A40: dom a = dom g1 /\ Seg(k+1) by A22,FUNCT_1:68;
A41: k <=k+1 by NAT_1:38;
  then k in Seg (k+1) by A19,FINSEQ_1:3;
then A42: k in dom a by A25,A40,XBOOLE_0:def 3;
A43: Seg k c= Seg (k+1) by A41,FINSEQ_1:7;
A44: a|k = (g1|(Seg (k+1)))|(Seg k) by A22,TOPREAL1:def 1
       .= g1|(Seg k) by A43,FUNCT_1:82
       .= g1|k by TOPREAL1:def 1;
A45: k+1 in dom a by A6,A24,A26,A40,XBOOLE_0:def 3;
    k>=1+1 by A17;
then A46: 1<k by NAT_1:38;
A47: a/.k = a.k by A42,FINSEQ_4:def 4
        .= g1.k by A22,A42,FUNCT_1:68
        .= g1/.k by A25,FINSEQ_4:def 4;
A48: a/.(k+1) = a.(k+1) by A45,FINSEQ_4:def 4
            .= g1.(k+1) by A22,A45,FUNCT_1:68
            .= g1/.(k+1) by A6,A24,FINSEQ_4:def 4;
    L~(a|k) /\ LSeg(a,k) = {a/.k} by A31,A39,A46,GOBOARD2:9;
  then L~(a|k) /\ LSeg(a/.k,a/.(k+1)) = {a/.k} by A19,A31,TOPREAL1:def 5;
  then L~b /\ LSeg(g1/.k,g1/.(k+1)) = {g1/.k} by A44,A47,A48,TOPREAL1:def 1;
  then L~b /\ LSeg(g1,k) = {g1/.k} by A19,A21,TOPREAL1:def 5;
then A49: L~b /\ c = {g1.k} by A25,FINSEQ_4:def 4;
A50: s1 misses s2
proof
  assume
   s1 meets s2;
  then consider x such that
A51:  x in s1 & x in s2 by XBOOLE_0:3;
A52:  x in Lf & x in L~b & x in c by A51,XBOOLE_0:def 3;
  then x in (L~b /\ c) by XBOOLE_0:def 3;
  then x = g1.k by A49,TARSKI:def 1;
  then x in rng g1 by A25,FUNCT_1:12;
  hence contradiction by A4,A52,XBOOLE_0:3;
end;
  per cases;
  suppose A53: Card s1 is even Nat;
   then reconsider c1 = Card (Lf /\ L~b) as even Integer;
      now per cases;
      suppose A54: Card s2 is even Nat;
then reconsider c2 = Card (Lf /\ c) as even Integer;
reconsider c = Card s as Integer;
A55: c = c1 + c2 by A38,A50,CARD_2:53;
A56: ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & g1.k in C & g1.(k+1) in C) by A1,A19,A21,A54,Th34;
     ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & b.1 in C & b.(len b) in C) by A18,A21,A53,NAT_1:38;
  hence ((Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2
   st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)))
        by A1,A27,A32,A36,A37,A55,A56,Th17;
     suppose A57: not Card s2 is even Nat;
   then reconsider c2 = Card (Lf /\ c) as odd Integer;
   reconsider c = Card s as Integer;
A58:c = c1 + c2 by A38,A50,CARD_2:53;
A59: not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & g1.k in C & g1.(k+1) in C) by A1,A19,A21,A57,Th34;
      ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & b.1 in C & b.(len b) in C) by A18,A21,A53,NAT_1:38;
    hence ((Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2
   st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)))
           by A1,A27,A32,A36,A37,A58,A59,Th17;
    end;
  hence ((Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2
   st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)));
  suppose A60: not Card s1 is even Nat;
   then reconsider c1 = Card (Lf /\ L~b) as odd Integer;
    now per cases;
      suppose A61: Card s2 is even Nat;
  then reconsider c2 = Card (Lf /\ c) as even Integer;
  reconsider c = Card s as Integer;
A62: c = c1 + c2 by A38,A50,CARD_2:53;
A63: ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & g1.k in C & g1.(k+1) in C) by A1,A19,A21,A61,Th34;
     not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & b.1 in C & b.(len b) in C) by A18,A21,A60,NAT_1:38;
  hence ((Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2
  st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)))
        by A1,A27,A32,A36,A37,A62,A63,Th17;
  suppose A64: not Card s2 is even Nat;
  then reconsider c2 = Card (Lf /\ c) as odd Integer;
  reconsider c = Card s as Integer;
A65: c = c1 + c2 by A38,A50,CARD_2:53;
A66: not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & g1.k in C & g1.(k+1) in C) by A1,A19,A21,A64,Th34;
     not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (Lf)`
              & b.1 in C & b.(len b) in C) by A18,A21,A60,NAT_1:38;
  hence ((Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2
   st C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)))
     by A1,A27,A28,A29,A30,A32,A36,A37,A65,A66,Th18;
  end;
  hence (Card (Lf /\ L~a) is even Nat iff (ex C be Subset of TOP-REAL 2 st
     (C is_a_component_of (Lf)` & a.1 in C & a.(len a) in C)));
end;
hence P[k+1];
end;
A67: for k st k>=2 holds P[k] from Ind1(A15,A16);
      dom g1 = Seg len g1 by FINSEQ_1:def 3;
    then g1|(Seg len g1) = g1 by RELAT_1:98;
    hence thesis by A2,A67;
end;

theorem
  for f1,f2,g1,g2 being special FinSequence of TOP-REAL 2
  st f1 ^' f2 is non constant standard special_circular_sequence &
     g1 ^' g2 is non constant standard special_circular_sequence &
     L~f1 misses L~g2 & L~f2 misses L~g1 &
     f1 ^' f2 , g1 ^' g2 are_in_general_position
for p1,p2,q1,q2 being Point of TOP-REAL 2
  st f1.1 = p1 & f1.len f1 = p2 & g1.1 = q1 & g1.len g1 = q2 &
     f1/.len f1 = f2/.1 & g1/.len g1 = g2/.1 &
     p1 in L~f1 /\ L~f2 & q1 in L~g1 /\ L~g2 &
     ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
        & q1 in C & q2 in C
     ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(g1 ^' g2))`
        & p1 in C & p2 in C
proof
  let f1,f2,g1,g2 be special FinSequence of TOP-REAL 2 such that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: g1 ^' g2 is non constant standard special_circular_sequence and
A3: L~f1 misses L~g2 and
A4:L~f2 misses L~g1 and
A5: f1 ^' f2 , g1 ^' g2 are_in_general_position;
  let p1,p2,q1,q2 be Point of TOP-REAL 2 such that
A6: f1.1 = p1 and
A7:f1.len f1 = p2 and
A8:g1.1 = q1 and
A9:g1.len g1 = q2 and
A10: f1/.len f1 = f2/.1 and
A11:g1/.len g1 = g2/.1 and
A12: p1 in L~f1 /\ L~f2 and
A13: q1 in L~g1 /\ L~g2 and
A14: ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
        & q1 in C & q2 in C;
A15:now
    assume A16: len g1 = 0 or len g1 =1 or len g2 = 0 or len g2 =1;
    per cases by A16;
    suppose len g1 = 0 or len g1 = 1;
    then L~g1 = {} by TOPREAL1:28;
    hence contradiction by A13;
    suppose len g2 = 0 or len g2 = 1;
    then L~g2 = {} by TOPREAL1:28;
    hence contradiction by A13;
  end;
then A17: len g1 is non trivial by NAT_2:def 1;
then A18: len g1 >= 2 by NAT_2:31;
       g1 is non trivial by A17,Lm3;
     then A19: g1 is non empty by REALSET1:def 12;
A20:len g2 is non trivial by A15,NAT_2:def 1;
then A21: len g2 >= 1+1 by NAT_2:31;
A22:g2 is non trivial by A20,Lm3;
A23:now
  assume A24: len f1 = 0 or len f1 =1 or len f2 = 0 or len f2 = 1;
  per cases by A24;
  suppose len f1 = 0 or len f1 = 1;
  then L~f1 = {} by TOPREAL1:28;
  hence contradiction by A12;
  suppose len f2 = 0 or len f2 = 1;
  then L~f2 = {} by TOPREAL1:28;
  hence contradiction by A12;
end;
then A25:len f1 is non trivial by NAT_2:def 1;
then A26: len f1 >= 2 by NAT_2:31;
      f1 is non trivial by A25,Lm3;
    then A27: f1 is non empty by REALSET1:def 12;
A28: len f2 is non trivial by A23,NAT_2:def 1;
then A29: len f2 >= 1+1 by NAT_2:31;
       f2 is non trivial by A28,Lm3;
     then A30: L~(f1 ^' f2) /\ L~g1 = (L~f1 \/ L~f2) /\ L~g1 by A10,A27,
TOPREAL8:35
                    .= L~f1 /\ L~g1 \/ L~f2 /\ L~g1 by XBOOLE_1:23
                    .= L~f1 /\ L~g1 \/ {} by A4,XBOOLE_0:def 7
                    .= L~f1 /\ L~g1 \/ L~f1 /\ L~g2 by A3,XBOOLE_0:def 7
                    .= (L~g1 \/ L~g2) /\ L~f1 by XBOOLE_1:23
                    .= L~f1 /\ L~(g1 ^' g2) by A11,A19,A22,TOPREAL8:35;
A31:f1 ^' f2, g1 are_in_general_position &
                      g1 is unfolded s.n.c. by A2,A5,A21,Th5,Th8;
A32:g1 ^' g2, f1 are_in_general_position &
               f1 is unfolded s.n.c. by A1,A5,A29,Th5,Th8;
     Card (L~(f1 ^' f2) /\ L~g1) is even Nat by A1,A8,A9,A14,A18,A31,Th35;
   hence thesis by A2,A6,A7,A26,A30,A32,Th35;
end;

Back to top