jordan12.miz



    begin

    reserve i,j,k,n for Nat,

X,Y,a,b,c,x for set,

r,s for Real;

    

     Lm1: for f be FinSequence st ( dom f) is trivial holds ( len f) is trivial

    proof

      let f be FinSequence;

      

       A1: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      assume

       A2: ( dom f) is trivial;

      per cases by A2, ZFMISC_1: 131;

        suppose ( dom f) is empty;

        then f = {} ;

        hence thesis by CARD_1: 27;

      end;

        suppose ex x be object st ( dom f) = {x};

        hence thesis by A1, CARD_1: 49, FINSEQ_3: 20;

      end;

    end;

    

     Lm2: 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;

      hence thesis by Lm1;

    end;

    theorem :: JORDAN12:1

    1 < i implies 0 < (i -' 1)

    proof

      assume 1 < i;

      then (1 - 1) = 0 & (1 -' 1) < (i -' 1) by NAT_D: 56;

      hence thesis by XREAL_0:def 2;

    end;

    theorem :: JORDAN12:2

    

     Th2: 1 is odd

    proof

      1 = ((2 * 0 ) + 1);

      hence thesis;

    end;

    theorem :: JORDAN12:3

    

     Th3: for f be FinSequence of ( TOP-REAL n) holds 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 in ( dom f) by SEQ_4: 134;

      then (f . i) in ( rng f) by FUNCT_1: 3;

      hence (f /. i) in ( rng f) by A2, PARTFUN1:def 6;

      

       A3: (i + 1) in ( dom f) by A1, SEQ_4: 134;

      then (f . (i + 1)) in ( rng f) by FUNCT_1: 3;

      hence thesis by A3, PARTFUN1:def 6;

    end;

    registration

      cluster s.n.c. -> s.c.c. for FinSequence of ( TOP-REAL 2);

      coherence ;

    end

    theorem :: JORDAN12:4

    

     Th4: 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;

      

       A3: g <> 0 by A2, CARD_1: 27;

       A4:

      now

        1 = (2 - 1);

        then (( len g) - 1) >= 1 by A2, XREAL_1: 9;

        then

         A5: (( len g) - 1) > 0 by XXREAL_0: 2;

        assume not f is s.n.c.;

        then

        consider i,j be Nat such that

         A6: (i + 1) < j and

         A7: not ( LSeg (f,i)) misses ( LSeg (f,j));

         A8:

        now

          assume not (1 <= j & (j + 1) <= ( len f));

          then ( LSeg (f,j)) = {} by TOPREAL1:def 3;

          hence contradiction by A7;

        end;

        then j < ( len f) by NAT_1: 13;

        then

         A9: ( LSeg ((f ^' g),j)) = ( LSeg (f,j)) by TOPREAL8: 28;

        (( len (f ^' g)) + 1) = (( len f) + ( len g)) by A3, FINSEQ_6: 139;

        then ((( len (f ^' g)) + 1) - 1) = (( len f) + (( len g) - 1));

        then ( len f) < ( len (f ^' g)) by A5, XREAL_1: 29;

        then

         A10: (j + 1) < ( len (f ^' g)) by A8, XXREAL_0: 2;

        now

          assume not (1 <= i & (i + 1) <= ( len f));

          then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

          hence contradiction by A7;

        end;

        then i < ( len f) by NAT_1: 13;

        then ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by TOPREAL8: 28;

        hence contradiction by A1, A6, A7, A10, A9;

      end;

      now

        assume not f is unfolded;

        then

        consider i be Nat such that

         A11: 1 <= i and

         A12: (i + 2) <= ( len f) and

         A13: (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) <> {(f /. (i + 1))};

        

         A14: 1 <= (i + 1) by A11, NAT_1: 13;

        (i + 1) < ((i + 1) + 1) by NAT_1: 13;

        then

         A15: (i + 1) < ( len f) by A12, NAT_1: 13;

        then

         A16: ( LSeg ((f ^' g),(i + 1))) = ( LSeg (f,(i + 1))) by TOPREAL8: 28;

        

         A17: ( len f) <= ( len (f ^' g)) by TOPREAL8: 7;

        then (i + 1) <= ( len (f ^' g)) by A15, XXREAL_0: 2;

        then

         A18: (i + 1) in ( dom (f ^' g)) by A14, FINSEQ_3: 25;

        i in NAT & i < ( len f) by A15, NAT_1: 13, ORDINAL1:def 12;

        then

         A19: ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by TOPREAL8: 28;

        (i + 1) in ( dom f) by A14, A15, FINSEQ_3: 25;

        

        then

         A20: (f /. (i + 1)) = (f . (i + 1)) by PARTFUN1:def 6

        .= ((f ^' g) . (i + 1)) by A14, A15, FINSEQ_6: 140

        .= ((f ^' g) /. (i + 1)) by A18, PARTFUN1:def 6;

        (i + 2) <= ( len (f ^' g)) by A12, A17, XXREAL_0: 2;

        hence contradiction by A1, A11, A13, A20, A19, A16;

      end;

      hence thesis by A4;

    end;

    theorem :: JORDAN12:5

    

     Th5: 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 be object;

      assume x in ( L~ g1);

      then

      consider a such that

       A1: x in a & a in { ( LSeg (g1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len g1) } by TARSKI:def 4;

      consider j be Nat such that

       A2: a = ( LSeg (g1,j)) and

       A3: 1 <= j and

       A4: (j + 1) <= ( len g1) by A1;

      j < ( len g1) by A4, NAT_1: 13;

      then

       A5: a = ( LSeg ((g1 ^' g2),j)) by A2, TOPREAL8: 28;

      ( len g1) <= ( len (g1 ^' g2)) by TOPREAL8: 7;

      then (j + 1) <= ( len (g1 ^' g2)) by A4, XXREAL_0: 2;

      then a in { ( LSeg ((g1 ^' g2),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (g1 ^' g2)) } by A3, A5;

      hence thesis by A1, TARSKI:def 4;

    end;

    begin

    definition

      let n;

      let f1,f2 be FinSequence of ( TOP-REAL n);

      :: JORDAN12:def1

      pred f1 is_in_general_position_wrt f2 means ( 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);

      :: JORDAN12:def2

      pred f1,f2 are_in_general_position means f1 is_in_general_position_wrt f2 & f2 is_in_general_position_wrt f1;

      symmetry ;

    end

    theorem :: JORDAN12:6

    

     Th6: for f1,f2 be FinSequence of ( TOP-REAL 2) st (f1,f2) are_in_general_position holds for f be 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

       A1: (f1,f2) are_in_general_position ;

      then

       A2: f1 is_in_general_position_wrt f2;

      let f be FinSequence of ( TOP-REAL 2) such that

       A3: f = (f2 | ( Seg k));

      

       A4: f = (f2 | k) by A3, FINSEQ_1:def 15;

      then

       A5: ( len f) <= ( len f2) by FINSEQ_5: 16;

       A6:

      now

        let i such that

         A7: 1 <= i and

         A8: i < ( len f);

        i in ( dom (f2 | k)) by A4, A7, A8, FINSEQ_3: 25;

        then

         A9: (f /. i) = (f2 /. i) by A4, FINSEQ_4: 70;

        

         A10: (i + 1) <= ( len f) by A8, NAT_1: 13;

        then

         A11: (i + 1) <= ( len f2) by A5, XXREAL_0: 2;

        then

         A12: i < ( len f2) by NAT_1: 13;

        1 <= (i + 1) by A7, NAT_1: 13;

        then (i + 1) in ( dom (f2 | k)) by A4, A10, FINSEQ_3: 25;

        then

         A13: (f /. (i + 1)) = (f2 /. (i + 1)) by A4, FINSEQ_4: 70;

        ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A7, A10, TOPREAL1:def 3

        .= ( LSeg (f2,i)) by A7, A11, A9, A13, TOPREAL1:def 3;

        hence (( L~ f1) /\ ( LSeg (f,i))) is trivial by A2, A7, A12;

      end;

      

       A14: f2 is_in_general_position_wrt f1 by A1;

       A15:

      now

        let i;

        assume 1 <= i & i < ( len f1);

        then

         A16: (( L~ f2) /\ ( LSeg (f1,i))) is trivial by A14;

        (( L~ f) /\ ( LSeg (f1,i))) c= (( L~ f2) /\ ( LSeg (f1,i))) by A4, TOPREAL3: 20, XBOOLE_1: 26;

        hence (( L~ f) /\ ( LSeg (f1,i))) is trivial by A16;

      end;

      ( L~ f2) misses ( rng f1) by A14;

      then ( L~ f) misses ( rng f1) by A4, TOPREAL3: 20, XBOOLE_1: 63;

      then

       A17: f is_in_general_position_wrt f1 by A15;

      ( L~ f1) misses ( rng f2) by A2;

      then ( rng f) misses ( L~ f1) by A3, RELAT_1: 70, XBOOLE_1: 63;

      then f1 is_in_general_position_wrt f by A6;

      hence thesis by A17;

    end;

    theorem :: JORDAN12:7

    

     Th7: 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: (g1 ^' g2) is_in_general_position_wrt (f1 ^' f2) by A1;

       A3:

      now

        let i;

        assume 1 <= i & i < ( len (f1 ^' f2));

        then

         A4: (( L~ (g1 ^' g2)) /\ ( LSeg ((f1 ^' f2),i))) is trivial by A2;

        (( L~ g1) /\ ( LSeg ((f1 ^' f2),i))) c= (( L~ (g1 ^' g2)) /\ ( LSeg ((f1 ^' f2),i))) by Th5, XBOOLE_1: 26;

        hence (( L~ g1) /\ ( LSeg ((f1 ^' f2),i))) is trivial by A4;

      end;

      

       A5: (f1 ^' f2) is_in_general_position_wrt (g1 ^' g2) by A1;

       A6:

      now

        let i such that

         A7: 1 <= i and

         A8: i < ( len g1);

        ( len g1) <= ( len (g1 ^' g2)) by TOPREAL8: 7;

        then i < ( len (g1 ^' g2)) by A8, XXREAL_0: 2;

        then (( L~ (f1 ^' f2)) /\ ( LSeg ((g1 ^' g2),i))) is trivial by A5, A7;

        hence (( L~ (f1 ^' f2)) /\ ( LSeg (g1,i))) is trivial by A8, TOPREAL8: 28;

      end;

      ( L~ (g1 ^' g2)) misses ( rng (f1 ^' f2)) by A2;

      then ( L~ g1) misses ( rng (f1 ^' f2)) by Th5, XBOOLE_1: 63;

      then

       A9: g1 is_in_general_position_wrt (f1 ^' f2) by A3;

      ( L~ (f1 ^' f2)) misses ( rng (g1 ^' g2)) by A5;

      then ( L~ (f1 ^' f2)) misses ( rng g1) by TOPREAL8: 10, XBOOLE_1: 63;

      then (f1 ^' f2) is_in_general_position_wrt g1 by A6;

      hence thesis by A9;

    end;

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

    theorem :: JORDAN12:8

    

     Th8: 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 and

       A2: (k + 1) <= ( len g) and

       A3: (f,g) are_in_general_position ;

      f is_in_general_position_wrt g by A3;

      then

       A4: ( L~ f) misses ( rng g);

      

       A5: ( rng g) c= the carrier of ( TOP-REAL 2) by FINSEQ_1:def 4;

      k < ( len g) by A2, NAT_1: 13;

      then k in ( dom g) by A1, FINSEQ_3: 25;

      then

       A6: (g . k) in ( rng g) by FUNCT_1: 3;

      now

        assume not (g . k) in (( L~ f) ` );

        then (g . k) in ((( L~ f) ` ) ` ) by A6, A5, XBOOLE_0:def 5;

        hence contradiction by A4, A6, XBOOLE_0: 3;

      end;

      hence (g . k) in (( L~ f) ` );

      1 <= (k + 1) by A1, NAT_1: 13;

      then (k + 1) in ( dom g) by A2, FINSEQ_3: 25;

      then

       A7: (g . (k + 1)) in ( rng g) by FUNCT_1: 3;

      now

        assume not (g . (k + 1)) in (( L~ f) ` );

        then (g . (k + 1)) in ((( L~ f) ` ) ` ) by A5, A7, XBOOLE_0:def 5;

        hence contradiction by A4, A7, XBOOLE_0: 3;

      end;

      hence thesis;

    end;

    theorem :: JORDAN12:9

    

     Th9: for f1,f2 be FinSequence of ( TOP-REAL 2) st (f1,f2) are_in_general_position holds 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 ;

      f1 is_in_general_position_wrt f2 by A1;

      then

       A2: ( L~ f1) misses ( rng f2);

      let i, j such that

       A3: 1 <= i & (i + 1) <= ( len f1) and

       A4: 1 <= j & (j + 1) <= ( len f2);

      f2 is_in_general_position_wrt f1 by A1;

      then

       A5: ( L~ f2) misses ( rng f1);

      now

        set B1 = ( LSeg ((f1 /. i),(f1 /. (i + 1)))), B2 = ( LSeg ((f2 /. j),(f2 /. (j + 1))));

        set A1 = ( LSeg (f1,i)), A2 = ( LSeg (f2,j));

        set A = (( LSeg (f1,i)) /\ ( LSeg (f2,j)));

        assume (( LSeg (f1,i)) /\ ( LSeg (f2,j))) is non trivial;

        then

        consider a1,a2 be object such that

         A6: a1 in A and

         A7: a2 in A and

         A8: a1 <> a2 by ZFMISC_1:def 10;

        

         A9: a1 in A1 & a2 in A1 by A6, A7, XBOOLE_0:def 4;

        

         A10: a2 in A2 by A7, XBOOLE_0:def 4;

        

         A11: a1 in A2 by A6, XBOOLE_0:def 4;

        reconsider a1, a2 as Point of ( TOP-REAL 2) by A6, A7;

        

         A12: a2 in B2 by A4, A10, TOPREAL1:def 3;

        

         A13: A1 = B1 by A3, TOPREAL1:def 3;

        then

         A14: a2 in B1 by A7, XBOOLE_0:def 4;

        a1 in B2 by A4, A11, TOPREAL1:def 3;

        then

         A15: a1 in (( LSeg ((f2 /. j),a2)) \/ ( LSeg (a2,(f2 /. (j + 1))))) by A12, TOPREAL1: 5;

        (f1 /. i) in B1 by RLTOPSP1: 68;

        then

         A16: ( LSeg (a2,(f1 /. i))) c= B1 by A14, TOPREAL1: 6;

        

         A17: a1 in (( LSeg ((f1 /. i),a2)) \/ ( LSeg (a2,(f1 /. (i + 1))))) by A9, A13, TOPREAL1: 5;

        (f2 /. j) in B2 by RLTOPSP1: 68;

        then

         A18: ( LSeg (a2,(f2 /. j))) c= B2 by A12, TOPREAL1: 6;

        

         A19: (f2 /. j) in ( rng f2) by A4, Th3;

        

         A20: (f1 /. i) in ( rng f1) by A3, Th3;

        (f2 /. (j + 1)) in B2 by RLTOPSP1: 68;

        then

         A21: ( LSeg (a2,(f2 /. (j + 1)))) c= B2 by A12, TOPREAL1: 6;

        (f1 /. (i + 1)) in B1 by RLTOPSP1: 68;

        then

         A22: ( LSeg (a2,(f1 /. (i + 1)))) c= B1 by A14, TOPREAL1: 6;

        

         A23: (f2 /. (j + 1)) in ( rng f2) by A4, Th3;

        

         A24: (f1 /. (i + 1)) in ( rng f1) by A3, Th3;

        per cases by A17, XBOOLE_0:def 3;

          suppose

           A25: a1 in ( LSeg ((f1 /. i),a2));

          now

            per cases by A15, XBOOLE_0:def 3;

              suppose a1 in ( LSeg ((f2 /. j),a2));

              then (f1 /. i) in ( LSeg (a2,(f2 /. j))) or (f2 /. j) in ( LSeg (a2,(f1 /. i))) by A8, A25, JORDAN4: 41;

              then

               A26: (f1 /. i) in B2 or (f2 /. j) in B1 by A18, A16;

              now

                per cases by A3, A4, A26, TOPREAL1:def 3;

                  suppose (f1 /. i) in A2;

                  then (f1 /. i) in ( L~ f2) by SPPOL_2: 17;

                  hence contradiction by A5, A20, XBOOLE_0: 3;

                end;

                  suppose (f2 /. j) in A1;

                  then (f2 /. j) in ( L~ f1) by SPPOL_2: 17;

                  hence contradiction by A2, A19, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

              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 A8, A25, JORDAN4: 41;

              then

               A27: (f1 /. i) in B2 or (f2 /. (j + 1)) in B1 by A16, A21;

              now

                per cases by A3, A4, A27, TOPREAL1:def 3;

                  suppose (f1 /. i) in A2;

                  then (f1 /. i) in ( L~ f2) by SPPOL_2: 17;

                  hence contradiction by A5, A20, XBOOLE_0: 3;

                end;

                  suppose (f2 /. (j + 1)) in A1;

                  then (f2 /. (j + 1)) in ( L~ f1) by SPPOL_2: 17;

                  hence contradiction by A2, A23, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

          suppose

           A28: a1 in ( LSeg (a2,(f1 /. (i + 1))));

          now

            per cases by A15, XBOOLE_0:def 3;

              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 A8, A28, JORDAN4: 41;

              then

               A29: (f1 /. (i + 1)) in B2 or (f2 /. j) in B1 by A18, A22;

              now

                per cases by A3, A4, A29, TOPREAL1:def 3;

                  suppose (f1 /. (i + 1)) in A2;

                  then (f1 /. (i + 1)) in ( L~ f2) by SPPOL_2: 17;

                  hence contradiction by A5, A24, XBOOLE_0: 3;

                end;

                  suppose (f2 /. j) in A1;

                  then (f2 /. j) in ( L~ f1) by SPPOL_2: 17;

                  hence contradiction by A2, A19, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

              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 A8, A28, JORDAN4: 41;

              then

               A30: (f1 /. (i + 1)) in B2 or (f2 /. (j + 1)) in B1 by A22, A21;

              now

                per cases by A3, A4, A30, TOPREAL1:def 3;

                  suppose (f1 /. (i + 1)) in A2;

                  then (f1 /. (i + 1)) in ( L~ f2) by SPPOL_2: 17;

                  hence contradiction by A5, A24, XBOOLE_0: 3;

                end;

                  suppose (f2 /. (j + 1)) in A1;

                  then (f2 /. (j + 1)) in ( L~ f1) by SPPOL_2: 17;

                  hence contradiction by A2, A23, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN12:10

    

     Th10: for f, g holds ( INTERSECTION ({ ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) },{ ( LSeg (g,j)) where j be Nat : 1 <= j & (j + 1) <= ( len g) })) is finite

    proof

      deffunc F( set, set) = ($1 /\ $2);

      let f, g;

      set AL = { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) };

      set BL = { ( LSeg (g,j)) where j be Nat : 1 <= j & (j + 1) <= ( len g) };

      set IN = { F(X,Y) where X be Subset of ( TOP-REAL 2), Y be Subset of ( TOP-REAL 2) : X in AL & Y in BL };

      

       A1: BL is finite by SPPOL_1: 23;

      set C = ( INTERSECTION (AL,BL));

      

       A2: C c= IN

      proof

        let a be object;

        assume a in C;

        then

        consider X, Y such that

         A3: X in AL & Y in BL and

         A4: a = (X /\ Y) by SETFAM_1:def 5;

        (ex i st X = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f)) & ex j st Y = ( LSeg (g,j)) & 1 <= j & (j + 1) <= ( len g) by A3;

        then

        reconsider X, Y as Subset of ( TOP-REAL 2);

        (X /\ Y) in IN by A3;

        hence thesis by A4;

      end;

      

       A5: AL is finite by SPPOL_1: 23;

      IN is finite from FRAENKEL:sch 22( A5, A1);

      hence thesis by A2;

    end;

    theorem :: JORDAN12:11

    

     Th11: 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 BL = { ( LSeg (g,j)) : 1 <= j & (j + 1) <= ( len g) };

      set AL = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

       A2:

      now

        let Z be set;

        assume Z in ( INTERSECTION (AL,BL));

        then

        consider X,Y be set such that

         A3: X in AL & Y in BL and

         A4: Z = (X /\ Y) by SETFAM_1:def 5;

        (ex i be Nat st X = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f)) & ex j be Nat st Y = ( LSeg (g,j)) & 1 <= j & (j + 1) <= ( len g) by A3;

        hence Z is finite by A1, A4, Th9;

      end;

      (( L~ f) /\ ( L~ g)) = ( union ( INTERSECTION (AL,BL))) & ( INTERSECTION (AL,BL)) is finite by Th10, SETFAM_1: 28;

      hence thesis by A2, FINSET_1: 7;

    end;

    theorem :: JORDAN12:12

    

     Th12: for f, g st (f,g) are_in_general_position holds for k holds (( L~ f) /\ ( LSeg (g,k))) is finite

    proof

      let f, g;

      assume (f,g) are_in_general_position ;

      then

       A1: (( L~ f) /\ ( L~ g)) is finite by Th11;

      let k;

      ((( L~ f) /\ ( L~ g)) /\ ( LSeg (g,k))) = (( L~ f) /\ (( L~ g) /\ ( LSeg (g,k)))) by XBOOLE_1: 16

      .= (( L~ f) /\ ( LSeg (g,k))) by TOPREAL3: 19, XBOOLE_1: 28;

      hence thesis by A1;

    end;

    begin

    reserve f for non constant standard special_circular_sequence,

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

    theorem :: JORDAN12:13

    

     Th13: 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: ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      

       A3: p1 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      then

       A4: not p1 in ( L~ f) by A1, XBOOLE_0: 3;

      

       A5: p2 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      then

       A6: not p2 in ( L~ f) by A1, XBOOLE_0: 3;

      

       A7: not (p2 in ( RightComp f) & p1 in ( LeftComp f)) by A1, A3, A5, JORDAN1J: 36;

      

       A8: ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      now

        per cases by A1, A3, A5, JORDAN1J: 36;

          suppose not p1 in ( RightComp f);

          then p1 in ( LeftComp f) & p2 in ( LeftComp f) by A7, A4, A6, GOBRD14: 17;

          hence thesis by A8;

        end;

          suppose not p2 in ( LeftComp f);

          then p2 in ( RightComp f) & p1 in ( RightComp f) by A7, A4, A6, GOBRD14: 18;

          hence thesis by A2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN12:14

    

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

    theorem :: JORDAN12:15

    

     Th15: 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) ` ) and

         A4: b in (( L~ f) ` ) and

         A5: not ex C be Subset of ( TOP-REAL 2) st (C is_a_component_of (( L~ f) ` ) & a in C & b in C);

        

         A6: a in (( LeftComp f) \/ ( RightComp f)) by A3, GOBRD12: 10;

        

         A7: b in (( LeftComp f) \/ ( RightComp f)) by A4, GOBRD12: 10;

        per cases by A6, XBOOLE_0:def 3;

          suppose

           A8: a in ( LeftComp f);

          now

            per cases by A7, XBOOLE_0:def 3;

              suppose b in ( LeftComp f);

              hence thesis by A1, A5, A8;

            end;

              suppose b in ( RightComp f);

              hence thesis by A8;

            end;

          end;

          hence thesis;

        end;

          suppose

           A9: a in ( RightComp f);

          now

            per cases by A7, XBOOLE_0:def 3;

              suppose b in ( RightComp f);

              hence thesis by A2, A5, A9;

            end;

              suppose b in ( LeftComp f);

              hence thesis by A9;

            end;

          end;

          hence thesis;

        end;

      end;

      thus (a in ( LeftComp f) & b in ( RightComp f) or a in ( RightComp f) & b in ( LeftComp f)) implies a in (( L~ f) ` ) & b in (( L~ f) ` ) & 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

         A10: 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

          ( LeftComp f) c= (( LeftComp f) \/ ( RightComp f)) by XBOOLE_1: 7;

          then

           A11: ( LeftComp f) c= (( L~ f) ` ) by GOBRD12: 10;

          ( RightComp f) c= (( LeftComp f) \/ ( RightComp f)) by XBOOLE_1: 7;

          then

           A12: ( RightComp f) c= (( L~ f) ` ) by GOBRD12: 10;

          per cases by A10;

            suppose a in ( LeftComp f) & b in ( RightComp f);

            hence thesis by A11, A12;

          end;

            suppose a in ( RightComp f) & b in ( LeftComp f);

            hence thesis by A11, A12;

          end;

        end;

        now

          given C be Subset of ( TOP-REAL 2) such that

           A13: C is_a_component_of (( L~ f) ` ) and

           A14: a in C and

           A15: b in C;

          now

            per cases by A10;

              suppose

               A16: a in ( LeftComp f) & b in ( RightComp f);

              now

                per cases by A1, A13, GOBOARD9: 1;

                  suppose C = ( LeftComp f);

                  then not ( LeftComp f) misses ( RightComp f) by A15, A16, XBOOLE_0: 3;

                  hence contradiction by GOBRD14: 14;

                end;

                  suppose C misses ( LeftComp f);

                  hence contradiction by A14, A16, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A17: a in ( RightComp f) & b in ( LeftComp f);

              now

                per cases by A1, A13, GOBOARD9: 1;

                  suppose C = ( LeftComp f);

                  then not ( LeftComp f) misses ( RightComp f) by A14, A17, XBOOLE_0: 3;

                  hence contradiction by GOBRD14: 14;

                end;

                  suppose C misses ( LeftComp f);

                  hence contradiction by A15, A17, XBOOLE_0: 3;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

        hence not ex C be Subset of ( TOP-REAL 2) st (C is_a_component_of (( L~ f) ` ) & a in C & b in C);

      end;

    end;

    theorem :: JORDAN12:16

    

     Th16: 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, Th14;

        suppose

         A3: a in ( RightComp f) & b in ( RightComp f);

        now

          per cases by A2, Th14;

            suppose

             A4: b in ( RightComp f) & c in ( RightComp f);

            ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

            hence thesis by A3, A4;

          end;

            suppose b in ( LeftComp f) & c in ( LeftComp f);

            then ( LeftComp f) meets ( RightComp f) by A3, XBOOLE_0: 3;

            hence thesis by GOBRD14: 14;

          end;

        end;

        hence thesis;

      end;

        suppose

         A5: a in ( LeftComp f) & b in ( LeftComp f);

        now

          per cases by A2, Th14;

            suppose

             A6: b in ( LeftComp f) & c in ( LeftComp f);

            ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

            hence thesis by A5, A6;

          end;

            suppose b in ( RightComp f) & c in ( RightComp f);

            then ( LeftComp f) meets ( RightComp f) by A5, XBOOLE_0: 3;

            hence thesis by GOBRD14: 14;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:17

    

     Th17: 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) ` ) and

       A2: b in (( L~ f) ` ) and

       A3: c 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) and

       A5: not ex C be Subset of ( TOP-REAL 2) st (C is_a_component_of (( L~ f) ` ) & b in C & c in C);

      

       A6: ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      

       A7: ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      per cases by A1, A2, A4, Th15;

        suppose

         A8: a in ( LeftComp f) & b in ( RightComp f);

        now

          per cases by A2, A3, A5, Th15;

            suppose b in ( LeftComp f) & c in ( RightComp f);

            then ( LeftComp f) meets ( RightComp f) by A8, XBOOLE_0: 3;

            hence thesis by GOBRD14: 14;

          end;

            suppose b in ( RightComp f) & c in ( LeftComp f);

            hence thesis by A6, A8;

          end;

        end;

        hence thesis;

      end;

        suppose

         A9: a in ( RightComp f) & b in ( LeftComp f);

        now

          per cases by A2, A3, A5, Th15;

            suppose b in ( RightComp f) & c in ( LeftComp f);

            then ( LeftComp f) meets ( RightComp f) by A9, XBOOLE_0: 3;

            hence thesis by GOBRD14: 14;

          end;

            suppose b in ( LeftComp f) & c in ( RightComp f);

            hence thesis by A7, A9;

          end;

        end;

        hence thesis;

      end;

    end;

    begin

    reserve G for Go-board;

     Lm3:

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

       A3: w2 in ( v_strip (G,i)) and

       A4: (w1 `1 ) <= (w2 `1 );

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

      proof

        let x be object such that

         A5: x in ( LSeg (w1,w2));

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

        

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

        

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

        

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

        per cases by A1, NAT_1: 14, XXREAL_0: 1;

          suppose i = 0 ;

          then

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

          then ex r1,s1 be 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 thesis by A8, A9;

        end;

          suppose i = ( len G);

          then

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

          then ex r1,s1 be 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 thesis by A8, A10;

        end;

          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 ex r2,s2 be 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 be 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 thesis by A8, A11, A12;

        end;

      end;

    end;

    theorem :: JORDAN12:18

    

     Th18: i <= ( len G) implies ( v_strip (G,i)) is convex

    proof

      assume

       A1: i <= ( len G);

      let w1,w2 be Point of ( TOP-REAL 2);

      set P = ( v_strip (G,i));

      

       A2: (w1 `1 ) <= (w2 `1 ) or (w2 `1 ) <= (w1 `1 );

      assume w1 in P & w2 in P;

      hence thesis by A1, A2, Lm3;

    end;

     Lm4:

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

       A3: w2 in ( h_strip (G,j)) and

       A4: (w1 `2 ) <= (w2 `2 );

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

      proof

        let x be object;

        assume

         A5: x in ( LSeg (w1,w2));

        then

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

        

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

        

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

        

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

        per cases by A1, NAT_1: 14, XXREAL_0: 1;

          suppose j = 0 ;

          then

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

          then ex r1,s1 be 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 thesis by A8, A9;

        end;

          suppose j = ( width G);

          then

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

          then ex r1,s1 be 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 thesis by A8, A10;

        end;

          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 ex r2,s2 be 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 be 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 thesis by A8, A11, A12;

        end;

      end;

    end;

    theorem :: JORDAN12:19

    

     Th19: 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 thesis by A1, A2, Lm4;

    end;

    theorem :: JORDAN12:20

    

     Th20: i <= ( len G) & j <= ( width G) implies ( cell (G,i,j)) is convex

    proof

      assume i <= ( len G) & j <= ( width G);

      then ( v_strip (G,i)) is convex & ( h_strip (G,j)) is convex by Th18, Th19;

      hence thesis by GOBOARD9: 6;

    end;

    theorem :: JORDAN12:21

    

     Th21: for f, k st 1 <= k & (k + 1) <= ( len f) holds ( left_cell (f,k)) is convex

    proof

      let f, k;

      assume 1 <= k & (k + 1) <= ( len f);

      then ex i, j st i <= ( len ( GoB f)) & j <= ( width ( GoB f)) & ( cell (( GoB f),i,j)) = ( left_cell (f,k)) by GOBOARD9: 11;

      hence thesis by Th20;

    end;

    theorem :: JORDAN12:22

    

     Th22: 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 and

       A2: (k + 1) <= ( len f);

      ( left_cell (f,k)) = ( left_cell (f,k,( GoB f))) by A1, A2, JORDAN1H: 21;

      hence ( left_cell (f,k,( GoB f))) is convex by A1, A2, Th21;

      k <= ( len f) by A2, NAT_1: 13;

      then

       A3: ((( len f) -' k) + k) = ( len f) by XREAL_1: 235;

      then

       A4: (( len f) -' k) >= 1 by A2, XREAL_1: 6;

      then

       A5: ( right_cell (f,k)) = ( left_cell (( Rev f),(( len f) -' k))) by A1, A3, GOBOARD9: 10;

      ( len f) = ( len ( Rev f)) & ((( len f) -' k) + 1) <= ( len f) by A1, A3, FINSEQ_5:def 3, XREAL_1: 6;

      then ( left_cell (( Rev f),(( len f) -' k))) is convex by A4, Th21;

      hence thesis by A1, A2, A5, JORDAN1H: 23;

    end;

    begin

    theorem :: JORDAN12:23

    

     Th23: for p1, p2, f holds 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 4;

      reconsider p as Point of ( TOP-REAL 2) by A4, A5;

       A7:

      now

        

         A8: ( LSeg (p1,p2)) = (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by A6, TOPREAL1: 5;

        per cases by A1, A8, XBOOLE_0:def 3;

          suppose r in ( LSeg (p1,p));

          hence (( LSeg (p1,r)) /\ ( LSeg (r,p))) = {r} or (( LSeg (p,r)) /\ ( LSeg (r,p2))) = {r} by TOPREAL1: 8;

        end;

          suppose r in ( LSeg (p,p2));

          hence (( LSeg (p1,r)) /\ ( LSeg (r,p))) = {r} or (( LSeg (p,r)) /\ ( LSeg (r,p2))) = {r} by TOPREAL1: 8;

        end;

      end;

      p2 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      then

       A9: ( LSeg (p2,r)) c= ( LSeg (p1,p2)) by A1, TOPREAL1: 6;

      p1 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      then

       A10: ( LSeg (p1,r)) c= ( LSeg (p1,p2)) by A1, TOPREAL1: 6;

      now

        assume that

         A11: ( L~ f) meets ( LSeg (p1,r)) and

         A12: ( L~ f) meets ( LSeg (r,p2));

        per cases by A7;

          suppose

           A13: (( LSeg (p1,r)) /\ ( LSeg (r,p))) = {r};

          consider x be object such that

           A14: x in ( L~ f) and

           A15: x in ( LSeg (p1,r)) by A11, XBOOLE_0: 3;

          x in (( L~ f) /\ ( LSeg (p1,p2))) by A10, A14, A15, XBOOLE_0:def 4;

          then x = p by A4, TARSKI:def 1;

          then x in ( LSeg (r,p)) by RLTOPSP1: 68;

          then x in (( LSeg (p1,r)) /\ ( LSeg (r,p))) by A15, XBOOLE_0:def 4;

          hence contradiction by A3, A13, A14, TARSKI:def 1;

        end;

          suppose

           A16: (( LSeg (p,r)) /\ ( LSeg (r,p2))) = {r};

          consider x be object such that

           A17: x in ( L~ f) and

           A18: x in ( LSeg (r,p2)) by A12, XBOOLE_0: 3;

          x in (( L~ f) /\ ( LSeg (p1,p2))) by A9, A17, A18, XBOOLE_0:def 4;

          then x = p by A4, TARSKI:def 1;

          then x in ( LSeg (p,r)) by RLTOPSP1: 68;

          then x in (( LSeg (p,r)) /\ ( LSeg (r,p2))) by A18, XBOOLE_0:def 4;

          hence contradiction by A3, A16, A17, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

     Lm5:

    now

      let p1, p2, f;

      let r be Point of ( TOP-REAL 2) such that

       A1: r in ( LSeg (p1,p2));

      assume

       A2: (ex x st (( L~ f) /\ ( LSeg (p1,p2))) = {x}) & not r in ( L~ f);

      per cases by A1, A2, Th23;

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

      end;

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

      end;

    end;

    theorem :: JORDAN12:24

    

     Th24: for p,q,r,s be 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))) <> {} ;

      then

      consider x be Point of ( TOP-REAL 2) such that

       A3: x in (( LSeg (p,q)) /\ ( LSeg (r,s))) by SUBSET_1: 4;

      

       A4: x in ( LSeg (r,s)) by A3, XBOOLE_0:def 4;

      x in ( LSeg (p,q)) by A3, XBOOLE_0:def 4;

      

      hence (p `1 ) = (x `1 ) by A1, SPPOL_1: 41

      .= (r `1 ) by A2, A4, SPPOL_1: 41;

    end;

    theorem :: JORDAN12:25

    

     Th25: 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: 8;

            suppose (p `1 ) < (p1 `1 );

            hence thesis by A2, A3, GOBOARD7: 8;

          end;

            suppose (p2 `1 ) < (p `1 );

            hence thesis by A2, A3, GOBOARD7: 8;

          end;

        end;

        hence thesis;

      end;

        suppose

         A4: (p2 `1 ) <= (p1 `1 );

        now

          per cases by A1, A2, GOBOARD7: 8;

            suppose (p `1 ) < (p2 `1 );

            hence thesis by A2, A4, GOBOARD7: 8;

          end;

            suppose (p1 `1 ) < (p `1 );

            hence thesis by A2, A4, GOBOARD7: 8;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:26

    

     Th26: 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: 7;

            suppose (p `2 ) < (p1 `2 );

            hence thesis by A2, A3, GOBOARD7: 7;

          end;

            suppose (p2 `2 ) < (p `2 );

            hence thesis by A2, A3, GOBOARD7: 7;

          end;

        end;

        hence thesis;

      end;

        suppose

         A4: (p2 `2 ) <= (p1 `2 );

        now

          per cases by A1, A2, GOBOARD7: 7;

            suppose (p `2 ) < (p2 `2 );

            hence thesis by A2, A4, GOBOARD7: 7;

          end;

            suppose (p1 `2 ) < (p `2 );

            hence thesis by A2, A4, GOBOARD7: 7;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:27

    

     Th27: p <> p1 & p <> p2 & p in ( LSeg (p1,p2)) implies not p1 in ( LSeg (p,p2))

    proof

      assume that

       A1: p <> p1 & p <> p2 and

       A2: p in ( LSeg (p1,p2));

      

       A3: (( LSeg (p1,p)) \/ ( LSeg (p,p2))) = ( LSeg (p1,p2)) by A2, TOPREAL1: 5;

      now

        assume p1 in ( LSeg (p,p2));

        then

         A4: (( LSeg (p,p1)) \/ ( LSeg (p1,p2))) = ( LSeg (p,p2)) by TOPREAL1: 5;

        (( LSeg (p,p1)) \/ ( LSeg (p1,p2))) = ( LSeg (p1,p2)) by A3, XBOOLE_1: 7, XBOOLE_1: 12;

        hence contradiction by A1, A4, SPPOL_1: 8;

      end;

      hence thesis;

    end;

    theorem :: JORDAN12:28

    

     Th28: 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, Th27;

      

       A6: not p2 in ( LSeg (p,p1)) by A2, A3, Th27;

      per cases by A1, A4, Th25, Th26;

        suppose

         A7: p1 in ( LSeg (q,p2));

        

         A8: p in (( LSeg (q,p1)) \/ ( LSeg (p1,p2))) by A2, XBOOLE_0:def 3;

        (( LSeg (q,p1)) \/ ( LSeg (p1,p2))) = ( LSeg (q,p2)) by A7, TOPREAL1: 5;

        then (( LSeg (q,p)) \/ ( LSeg (p,p2))) = ( LSeg (q,p2)) by A8, TOPREAL1: 5;

        hence thesis by A5, A7, XBOOLE_0:def 3;

      end;

        suppose

         A9: p2 in ( LSeg (q,p1));

        

         A10: p in (( LSeg (q,p2)) \/ ( LSeg (p1,p2))) by A2, XBOOLE_0:def 3;

        (( LSeg (q,p2)) \/ ( LSeg (p1,p2))) = ( LSeg (q,p1)) by A9, TOPREAL1: 5;

        then (( LSeg (q,p)) \/ ( LSeg (p,p1))) = ( LSeg (q,p1)) by A10, TOPREAL1: 5;

        hence thesis by A6, A9, XBOOLE_0:def 3;

      end;

    end;

    theorem :: JORDAN12:29

    

     Th29: 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 p in ( LSeg (p3,p4)) by XBOOLE_0:def 4;

      then (( LSeg (p3,p)) \/ ( LSeg (p,p4))) = ( LSeg (p3,p4)) by TOPREAL1: 5;

      then

       A4: ( LSeg (p3,p)) c= ( LSeg (p3,p4)) by XBOOLE_1: 7;

      

       A5: ( LSeg (p1,p2)) meets ( LSeg (p3,p4)) by A3;

       A6:

      now

        assume (p1 `2 ) = (p2 `2 ) & (p3 `2 ) = (p4 `2 );

        then ( LSeg (p1,p2)) is horizontal & ( LSeg (p3,p4)) is horizontal by SPPOL_1: 15;

        hence (p2 `2 ) = (p3 `2 ) by A5, SPRECT_3: 9;

      end;

       A7:

      now

        assume (p1 `1 ) = (p2 `1 ) & (p3 `1 ) = (p4 `1 );

        then ( LSeg (p1,p2)) is vertical & ( LSeg (p3,p4)) is vertical by SPPOL_1: 16;

        hence (p2 `1 ) = (p3 `1 ) by A5, Th24;

      end;

      

       A8: p3 in ( LSeg (p3,p4)) by RLTOPSP1: 68;

      

       A9: p2 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      

       A10: p1 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      now

        

         A11: p in ( LSeg (p1,p2)) by A3, XBOOLE_0:def 4;

        assume that

         A12: p <> p1 and

         A13: p <> p2 and

         A14: p <> p3;

         A15:

        now

          assume p3 in ( LSeg (p1,p2));

          then p3 in (( LSeg (p1,p2)) /\ ( LSeg (p3,p4))) by A8, XBOOLE_0:def 4;

          hence contradiction by A2, A14, TARSKI:def 1;

        end;

        now

          per cases by A1, A7, A6, A12, A13, A11, A15, Th28;

            suppose p1 in ( LSeg (p3,p));

            then p1 in (( LSeg (p1,p2)) /\ ( LSeg (p3,p4))) by A4, A10, XBOOLE_0:def 4;

            hence contradiction by A2, A12, TARSKI:def 1;

          end;

            suppose p2 in ( LSeg (p3,p));

            then p2 in (( LSeg (p1,p2)) /\ ( LSeg (p3,p4))) by A4, A9, XBOOLE_0:def 4;

            hence contradiction by A2, A13, TARSKI:def 1;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    begin

    theorem :: JORDAN12:30

    

     Th30: for p, p1, p2, f st (( L~ f) /\ ( LSeg (p1,p2))) = {p} holds 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;

      assume (( L~ f) /\ ( LSeg (p1,p2))) = {p};

      then

       A1: p in (( L~ f) /\ ( LSeg (p1,p2))) by TARSKI:def 1;

      then

       A2: p in ( LSeg (p1,p2)) by XBOOLE_0:def 4;

      let r be Point of ( TOP-REAL 2) such that

       A3: not r in ( LSeg (p1,p2)) and

       A4: not p1 in ( L~ f) and

       A5: not p2 in ( L~ f) and

       A6: (p1 `1 ) = (p2 `1 ) & (p1 `1 ) = (r `1 ) or (p1 `2 ) = (p2 `2 ) & (p1 `2 ) = (r `2 ) and

       A7: ex i st 1 <= i & (i + 1) <= ( len f) & (r in ( right_cell (f,i,( GoB f))) or r in ( left_cell (f,i,( GoB f)))) & p in ( LSeg (f,i)) and

       A8: not r in ( L~ f);

      consider i such that

       A9: 1 <= i & (i + 1) <= ( len f) and

       A10: r in ( right_cell (f,i,( GoB f))) or r in ( left_cell (f,i,( GoB f))) and

       A11: p in ( LSeg (f,i)) by A7;

      

       A12: ( right_cell (f,i,( GoB f))) is convex by A9, Th22;

      

       A13: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      then

       A14: (( right_cell (f,i,( GoB f))) \ ( L~ f)) c= ( RightComp f) by A9, JORDAN9: 27;

       A15:

      now

        assume r in ( right_cell (f,i,( GoB f)));

        then r in (( right_cell (f,i,( GoB f))) \ ( L~ f)) by A8, XBOOLE_0:def 5;

        hence r in ( RightComp f) by A14;

      end;

      

       A16: ( LSeg (f,i)) c= ( right_cell (f,i,( GoB f))) by A13, A9, JORDAN1H: 22;

       A17:

      now

        assume that

         A18: p1 in ( LSeg (r,p)) and

         A19: r in ( right_cell (f,i,( GoB f)));

        ( LSeg (r,p)) c= ( right_cell (f,i,( GoB f))) by A11, A16, A12, A19;

        then p1 in (( right_cell (f,i,( GoB f))) \ ( L~ f)) by A4, A18, XBOOLE_0:def 5;

        hence ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ f) ` ) & r in C & p1 in C by A14, A15, A19, Th14;

      end;

      

       A20: ( left_cell (f,i,( GoB f))) is convex by A9, Th22;

      

       A21: (( left_cell (f,i,( GoB f))) \ ( L~ f)) c= ( LeftComp f) by A13, A9, JORDAN9: 27;

       A22:

      now

        assume r in ( left_cell (f,i,( GoB f)));

        then r in (( left_cell (f,i,( GoB f))) \ ( L~ f)) by A8, XBOOLE_0:def 5;

        hence r in ( LeftComp f) by A21;

      end;

      

       A23: ( LSeg (f,i)) c= ( left_cell (f,i,( GoB f))) by A13, A9, JORDAN1H: 20;

       A24:

      now

        assume that

         A25: p1 in ( LSeg (r,p)) and

         A26: r in ( left_cell (f,i,( GoB f)));

        ( LSeg (r,p)) c= ( left_cell (f,i,( GoB f))) by A11, A23, A20, A26;

        then p1 in (( left_cell (f,i,( GoB f))) \ ( L~ f)) by A4, A25, XBOOLE_0:def 5;

        hence ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ f) ` ) & r in C & p1 in C by A21, A22, A26, Th14;

      end;

       A27:

      now

        assume that

         A28: p2 in ( LSeg (r,p)) and

         A29: r in ( left_cell (f,i,( GoB f)));

        ( LSeg (r,p)) c= ( left_cell (f,i,( GoB f))) by A11, A23, A20, A29;

        then p2 in (( left_cell (f,i,( GoB f))) \ ( L~ f)) by A5, A28, XBOOLE_0:def 5;

        hence ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ f) ` ) & r in C & p2 in C by A21, A22, A29, Th14;

      end;

       A30:

      now

        assume that

         A31: p2 in ( LSeg (r,p)) and

         A32: r in ( right_cell (f,i,( GoB f)));

        ( LSeg (r,p)) c= ( right_cell (f,i,( GoB f))) by A11, A16, A12, A32;

        then p2 in (( right_cell (f,i,( GoB f))) \ ( L~ f)) by A5, A31, XBOOLE_0:def 5;

        hence ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ f) ` ) & r in C & p2 in C by A14, A15, A32, Th14;

      end;

      

       A33: p <> p2 & p <> p1 by A4, A5, A1, XBOOLE_0:def 4;

      per cases by A3, A6, A33, A2, Th28;

        suppose

         A34: p1 in ( LSeg (r,p));

        now

          per cases by A10;

            suppose r in ( right_cell (f,i,( GoB f)));

            hence thesis by A17, A34;

          end;

            suppose r in ( left_cell (f,i,( GoB f)));

            hence thesis by A24, A34;

          end;

        end;

        hence thesis;

      end;

        suppose

         A35: p2 in ( LSeg (r,p));

        now

          per cases by A10;

            suppose r in ( right_cell (f,i,( GoB f)));

            hence thesis by A30, A35;

          end;

            suppose r in ( left_cell (f,i,( GoB f)));

            hence thesis by A27, A35;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:31

    

     Th31: for f, p1, p2, p st (( L~ f) /\ ( LSeg (p1,p2))) = {p} holds 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) & ((p1 `1 ) = (p2 `1 ) & (p1 `1 ) = (rl `1 ) & (rl `1 ) = (rp `1 ) or (p1 `2 ) = (p2 `2 ) & (p1 `2 ) = (rl `2 ) & (rl `2 ) = (rp `2 )) and

       A3: ex i st 1 <= i & (i + 1) <= ( len f) & rl in ( left_cell (f,i,( GoB f))) & rp in ( right_cell (f,i,( GoB f))) & p in ( LSeg (f,i)) and

       A4: not rl in ( L~ f) and

       A5: not rp in ( L~ f);

      consider i such that

       A6: 1 <= i & (i + 1) <= ( len f) and

       A7: rl in ( left_cell (f,i,( GoB f))) and

       A8: rp in ( right_cell (f,i,( GoB f))) by A3;

      

       A9: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      then

       A10: (( left_cell (f,i,( GoB f))) \ ( L~ f)) c= ( LeftComp f) by A6, JORDAN9: 27;

      

       A11: (( right_cell (f,i,( GoB f))) \ ( L~ f)) c= ( RightComp f) by A9, A6, JORDAN9: 27;

      rp in (( right_cell (f,i,( GoB f))) \ ( L~ f)) by A5, A8, XBOOLE_0:def 5;

      then

       A12: not rp in ( LeftComp f) by A11, GOBRD14: 18;

       A13:

      now

        assume

         A14: not rp in ( LSeg (p1,p2));

        per cases by A1, A2, A3, A5, A14, Th30;

          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 A12, Th14;

        end;

          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 A12, Th14;

        end;

      end;

      rl in (( left_cell (f,i,( GoB f))) \ ( L~ f)) by A4, A7, XBOOLE_0:def 5;

      then

       A15: not rl in ( RightComp f) by A10, GOBRD14: 17;

       A16:

      now

        assume

         A17: not rl in ( LSeg (p1,p2));

        per cases by A1, A2, A3, A4, A17, Th30;

          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 A15, Th14;

        end;

          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 A15, Th14;

        end;

      end;

       A18:

      now

        assume that

         A19: not rl in ( LSeg (p1,p2)) and

         A20: not rp in ( LSeg (p1,p2));

        per cases by A16, A19;

          suppose

           A21: p1 in ( LeftComp f);

          now

            per cases by A13, A20;

              suppose p1 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A21, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

              suppose p2 in ( RightComp f);

              hence thesis by A21, Th15;

            end;

          end;

          hence thesis;

        end;

          suppose

           A22: p2 in ( LeftComp f);

          now

            per cases by A13, A20;

              suppose p1 in ( RightComp f);

              hence thesis by A22, Th15;

            end;

              suppose p2 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A22, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

          end;

          hence thesis;

        end;

      end;

       A23:

      now

        assume

         A24: rp in ( LSeg (p1,p2));

        per cases by A1, A5, A24, Lm5;

          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 A12, Th14;

        end;

          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 A12, Th14;

        end;

      end;

       A25:

      now

        assume that

         A26: not rl in ( LSeg (p1,p2)) and

         A27: rp in ( LSeg (p1,p2));

        per cases by A16, A26;

          suppose

           A28: p1 in ( LeftComp f);

          now

            per cases by A23, A27;

              suppose p1 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A28, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

              suppose p2 in ( RightComp f);

              hence thesis by A28, Th15;

            end;

          end;

          hence thesis;

        end;

          suppose

           A29: p2 in ( LeftComp f);

          now

            per cases by A23, A27;

              suppose p1 in ( RightComp f);

              hence thesis by A29, Th15;

            end;

              suppose p2 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A29, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

          end;

          hence thesis;

        end;

      end;

       A30:

      now

        assume

         A31: rl in ( LSeg (p1,p2));

        per cases by A1, A4, A31, Lm5;

          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 A15, Th14;

        end;

          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 A15, Th14;

        end;

      end;

       A32:

      now

        assume that

         A33: rl in ( LSeg (p1,p2)) and

         A34: rp in ( LSeg (p1,p2));

        per cases by A30, A33;

          suppose

           A35: p1 in ( LeftComp f);

          now

            per cases by A23, A34;

              suppose p1 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A35, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

              suppose p2 in ( RightComp f);

              hence thesis by A35, Th15;

            end;

          end;

          hence thesis;

        end;

          suppose

           A36: p2 in ( LeftComp f);

          now

            per cases by A23, A34;

              suppose p1 in ( RightComp f);

              hence thesis by A36, Th15;

            end;

              suppose p2 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A36, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

          end;

          hence thesis;

        end;

      end;

       A37:

      now

        assume that

         A38: rl in ( LSeg (p1,p2)) and

         A39: not rp in ( LSeg (p1,p2));

        per cases by A30, A38;

          suppose

           A40: p1 in ( LeftComp f);

          now

            per cases by A13, A39;

              suppose p1 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A40, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

              suppose p2 in ( RightComp f);

              hence thesis by A40, Th15;

            end;

          end;

          hence thesis;

        end;

          suppose

           A41: p2 in ( LeftComp f);

          now

            per cases by A13, A39;

              suppose p1 in ( RightComp f);

              hence thesis by A41, Th15;

            end;

              suppose p2 in ( RightComp f);

              then ( LeftComp f) meets ( RightComp f) by A41, XBOOLE_0: 3;

              hence thesis by GOBRD14: 14;

            end;

          end;

          hence thesis;

        end;

      end;

      per cases ;

        suppose

         A42: rl in ( LSeg (p1,p2));

        now

          per cases ;

            suppose rp in ( LSeg (p1,p2));

            hence thesis by A32, A42;

          end;

            suppose not rp in ( LSeg (p1,p2));

            hence thesis by A37, A42;

          end;

        end;

        hence thesis;

      end;

        suppose

         A43: not rl in ( LSeg (p1,p2));

        now

          per cases ;

            suppose rp in ( LSeg (p1,p2));

            hence thesis by A25, A43;

          end;

            suppose not rp in ( LSeg (p1,p2));

            hence thesis by A18, A43;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:32

    

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

      

       A3: p in {p} by TARSKI:def 1;

      then

       A4: p in ( LSeg (p1,p2)) by A1, XBOOLE_0:def 4;

      

       A5: p in ( LSeg (p2,p1)) by A1, A3, XBOOLE_0:def 4;

      p in ( L~ f) by A1, A3, XBOOLE_0:def 4;

      then

      consider LS be set such that

       A6: p in LS & LS in { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) } by TARSKI:def 4;

      set G = ( GoB f);

      assume that

       A7: ( not p1 in ( L~ f)) & not p2 in ( L~ f) and

       A8: ( rng f) misses ( LSeg (p1,p2));

      consider k such that

       A9: LS = ( LSeg (f,k)) and

       A10: 1 <= k and

       A11: (k + 1) <= ( len f) by A6;

      

       A12: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      then

      consider i1,j1,i2,j2 be Nat such that

       A13: [i1, j1] in ( Indices G) and

       A14: (f /. k) = (G * (i1,j1)) and

       A15: [i2, j2] in ( Indices G) and

       A16: (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 A10, A11, JORDAN8: 3;

      

       A18: 1 <= i1 by A13, MATRIX_0: 32;

      1 <= (k + 1) by A10, NAT_1: 13;

      then

       A19: (k + 1) in ( dom f) by A11, FINSEQ_3: 25;

      then (f . (k + 1)) in ( rng f) by FUNCT_1: 3;

      then (f /. (k + 1)) in ( rng f) by A19, PARTFUN1:def 6;

      then

       A20: p <> (f /. (k + 1)) by A8, A4, XBOOLE_0: 3;

      

       A21: i2 <= ( len G) by A15, MATRIX_0: 32;

      then

       A22: i2 = (i1 + 1) implies i1 < ( len G) by NAT_1: 13;

      then

       A23: 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 A18, GOBOARD6: 25;

      

       A24: 1 <= j1 by A13, MATRIX_0: 32;

      then

       A25: 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 A18, A22, GOBOARD6: 26;

      

       A26: j2 <= ( width G) by A15, MATRIX_0: 32;

      then

       A27: j2 = (j1 + 1) implies j1 < ( width G) by NAT_1: 13;

      then

       A28: 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 A24, GOBOARD6: 23;

      

       A29: 1 <= j2 by A15, MATRIX_0: 32;

      

       A30: j1 <= ( width G) by A13, MATRIX_0: 32;

      then

       A31: j1 = (j2 + 1) implies j2 < ( width G) by NAT_1: 13;

      then

       A32: 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 A29, GOBOARD6: 23;

      

       A33: 1 <= i2 by A15, MATRIX_0: 32;

      then

       A34: 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, A31, GOBOARD6: 26;

      

       A35: i1 <= ( len G) by A13, MATRIX_0: 32;

      then

       A36: i1 = (i2 + 1) implies i2 < ( len G) by NAT_1: 13;

      then

       A37: 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 A33, GOBOARD6: 25;

      k < ( len f) by A11, NAT_1: 13;

      then

       A38: k in ( dom f) by A10, FINSEQ_3: 25;

      then (f . k) in ( rng f) by FUNCT_1: 3;

      then (f /. k) in ( rng f) by A38, PARTFUN1:def 6;

      then

       A39: p <> (f /. k) by A8, A4, XBOOLE_0: 3;

      

       A40: (j1 -' 1) < j1 by A24, JORDAN5B: 1;

       A41:

      now

        assume 1 < j1 & i2 = (i1 + 1);

        then

         A42: i1 < ( len G) & 1 <= (j1 -' 1) by A21, NAT_1: 13, NAT_D: 49;

        1 <= i1 & (j1 -' 1) < ( width G) by A13, A30, A40, MATRIX_0: 32, XXREAL_0: 2;

        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 A42, GOBOARD6: 26;

      end;

      

       A43: 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 A33, A24, A36, GOBOARD6: 26;

       A44:

      now

        assume 1 < j1 & i1 = (i2 + 1);

        then

         A45: i2 < ( len G) & 1 <= (j1 -' 1) by A35, NAT_1: 13, NAT_D: 49;

        1 <= i2 & (j1 -' 1) < ( width G) by A15, A30, A40, MATRIX_0: 32, XXREAL_0: 2;

        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 A45, GOBOARD6: 26;

      end;

       A46:

      now

        assume that

         A47: 1 = j1 and

         A48: i1 = (i2 + 1);

        ( Int ( cell (G,i2, 0 ))) = ( Int ( cell (G,i2,(j1 -' 1)))) by A47, NAT_2: 8;

        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 A33, A36, A48, GOBOARD6: 24;

      end;

      

       A49: j1 = j2 & i2 = (i1 + 1) implies ( Int ( left_cell (f,k,G))) = ( Int ( cell (G,i1,j1))) & ( Int ( right_cell (f,k,G))) = ( Int ( cell (G,i1,(j1 -' 1)))) by A12, A10, A11, A13, A14, A15, A16, GOBRD13: 23, GOBRD13: 24;

      

       A50: p in ( LSeg ((f /. (k + 1)),(f /. k))) by A6, A9, A10, A11, TOPREAL1:def 3;

       A51:

      now

        assume that

         A52: i1 = i2 and

         A53: j1 = (j2 + 1);

        j2 < j1 by A53, NAT_1: 13;

        then ((f /. (k + 1)) `2 ) < ((f /. k) `2 ) by A14, A16, A35, A18, A30, A29, A52, GOBOARD5: 4;

        then

         A54: ((f /. (k + 1)) `2 ) < (p `2 ) & (p `2 ) < ((f /. k) `2 ) by A39, A50, A20, TOPREAL6: 30;

        1 <= (j2 + 1) & (j2 + 1) <= ( width G) by A13, A53, MATRIX_0: 32;

        hence ((G * (1,j2)) `2 ) < (p `2 ) & (p `2 ) < ((G * (1,(j2 + 1))) `2 ) by A14, A16, A35, A18, A26, A29, A52, A53, A54, GOBOARD5: 1;

      end;

       A55:

      now

        assume that

         A56: i1 = i2 and

         A57: j2 = (j1 + 1);

        j1 < j2 by A57, NAT_1: 13;

        then ((f /. k) `2 ) < ((f /. (k + 1)) `2 ) by A14, A16, A35, A18, A24, A26, A56, GOBOARD5: 4;

        then ((f /. k) `2 ) < (p `2 ) & (p `2 ) < ((f /. (k + 1)) `2 ) by A39, A50, A20, TOPREAL6: 30;

        hence ((G * (1,j1)) `2 ) < (p `2 ) & (p `2 ) < ((G * (1,(j1 + 1))) `2 ) by A14, A16, A33, A35, A24, A30, A26, A29, A56, A57, GOBOARD5: 1;

      end;

       A58:

      now

        assume that

         A59: 1 = i2 and

         A60: j1 = (j2 + 1);

        ( Int ( cell (G,(i2 -' 1),j2))) = ( Int ( cell (G, 0 ,j2))) by A59, NAT_2: 8;

        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 A29, A31, A60, GOBOARD6: 20;

      end;

      (( LSeg (p1,p2)) /\ ( LSeg (f,k))) = {p} by A1, A6, A9, TOPREAL3: 19, ZFMISC_1: 124;

      then

       A61: (( LSeg (p1,p2)) /\ ( LSeg ((f /. k),(f /. (k + 1))))) = {p} by A10, A11, TOPREAL1:def 3;

      

       A62: i1 < ( len 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 A18, A24, A27, GOBOARD6: 26;

       A63:

      now

        assume that

         A64: 1 = i1 and

         A65: j2 = (j1 + 1);

        ( Int ( cell (G,(i1 -' 1),j1))) = ( Int ( cell (G, 0 ,j1))) by A64, NAT_2: 8;

        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 A24, A27, A65, GOBOARD6: 20;

      end;

      

       A66: i1 = i2 & j1 = (j2 + 1) implies ( Int ( right_cell (f,k,G))) = ( Int ( cell (G,(i2 -' 1),j2))) & ( Int ( left_cell (f,k,G))) = ( Int ( cell (G,i2,j2))) by A12, A10, A11, A13, A14, A15, A16, GOBRD13: 27, GOBRD13: 28;

       A67:

      now

        let r be Point of ( TOP-REAL 2);

        assume

         A68: r in ( Int ( left_cell (f,k,G)));

        ( Int ( left_cell (f,k,G))) c= ( left_cell (f,k,G)) by TOPS_1: 16;

        hence r in ( left_cell (f,k,G)) by A68;

        ( Int ( left_cell (f,k,G))) misses ( L~ f) by A12, A10, A11, JORDAN9: 15;

        hence not r in ( L~ f) by A68, XBOOLE_0: 3;

      end;

       A69:

      now

        let r be Point of ( TOP-REAL 2);

        assume

         A70: r in ( Int ( right_cell (f,k,G)));

        ( Int ( right_cell (f,k,G))) c= ( right_cell (f,k,G)) by TOPS_1: 16;

        hence r in ( right_cell (f,k,G)) by A70;

        ( Int ( right_cell (f,k,G))) misses ( L~ f) by A12, A10, A11, JORDAN9: 15;

        hence not r in ( L~ f) by A70, XBOOLE_0: 3;

      end;

       A71:

      now

        assume that

         A72: 1 = j1 and

         A73: i2 = (i1 + 1);

        ( Int ( cell (G,i1, 0 ))) = ( Int ( cell (G,i1,(j1 -' 1)))) by A72, NAT_2: 8;

        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 A18, A22, A73, GOBOARD6: 24;

      end;

      ( LSeg (f,k)) is vertical or ( LSeg (f,k)) is horizontal by SPPOL_1: 19;

      then ( LSeg ((f /. k),(f /. (k + 1)))) is vertical or ( LSeg ((f /. k),(f /. (k + 1)))) is horizontal by A10, A11, TOPREAL1:def 3;

      then

       A74: ((f /. k) `1 ) = ((f /. (k + 1)) `1 ) or ((f /. k) `2 ) = ((f /. (k + 1)) `2 ) by SPPOL_1: 15, SPPOL_1: 16;

       A75:

      now

        assume that

         A76: j1 = j2 and

         A77: i2 = (i1 + 1);

        i1 < i2 by A77, NAT_1: 13;

        then ((f /. k) `1 ) < ((f /. (k + 1)) `1 ) by A14, A16, A21, A18, A26, A29, A76, GOBOARD5: 3;

        then ((f /. k) `1 ) < (p `1 ) & (p `1 ) < ((f /. (k + 1)) `1 ) by A39, A50, A20, TOPREAL6: 29;

        hence ((G * (i1,1)) `1 ) < (p `1 ) & (p `1 ) < ((G * ((i1 + 1),1)) `1 ) by A14, A16, A21, A33, A35, A18, A30, A29, A76, A77, GOBOARD5: 2;

      end;

      

       A78: (i2 -' 1) < i2 by A33, JORDAN5B: 1;

       A79:

      now

        assume 1 < i2 & j1 = (j2 + 1);

        then

         A80: 1 <= (i2 -' 1) & j2 < ( width G) by A30, NAT_1: 13, NAT_D: 49;

        (i2 -' 1) < ( len G) & 1 <= j2 by A15, A21, A78, MATRIX_0: 32, XXREAL_0: 2;

        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 A80, GOBOARD6: 26;

      end;

      

       A81: j1 = j2 & i1 = (i2 + 1) implies ( Int ( left_cell (f,k,G))) = ( Int ( cell (G,i2,(j1 -' 1)))) & ( Int ( right_cell (f,k,G))) = ( Int ( cell (G,i2,j1))) by A12, A10, A11, A13, A14, A15, A16, GOBRD13: 25, GOBRD13: 26;

       A82:

      now

        assume that

         A83: j1 = j2 and

         A84: i1 = (i2 + 1);

        i2 < i1 by A84, NAT_1: 13;

        then ((G * (i2,j1)) `1 ) < ((G * (i1,j1)) `1 ) by A33, A35, A24, A30, GOBOARD5: 3;

        then ((f /. (k + 1)) `1 ) < (p `1 ) & (p `1 ) < ((f /. k) `1 ) by A14, A16, A39, A50, A20, A83, TOPREAL6: 29;

        hence ((G * (i2,1)) `1 ) < (p `1 ) & (p `1 ) < ((G * ((i2 + 1),1)) `1 ) by A14, A16, A21, A33, A35, A18, A26, A29, A83, A84, GOBOARD5: 2;

      end;

      

       A85: (i1 -' 1) < i1 by A18, JORDAN5B: 1;

       A86:

      now

        assume 1 < i1 & j2 = (j1 + 1);

        then

         A87: 1 <= (i1 -' 1) & j1 < ( width G) by A26, NAT_1: 13, NAT_D: 49;

        (i1 -' 1) < ( len G) & 1 <= j1 by A13, A35, A85, MATRIX_0: 32, XXREAL_0: 2;

        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 A87, GOBOARD6: 26;

      end;

      

       A88: i1 = i2 & j2 = (j1 + 1) implies ( Int ( left_cell (f,k,G))) = ( Int ( cell (G,(i1 -' 1),j1))) & ( Int ( right_cell (f,k,G))) = ( Int ( cell (G,i1,j1))) by A12, A10, A11, A13, A14, A15, A16, GOBRD13: 21, GOBRD13: 22;

      

       A89: p <> p1 & p <> p2 by A1, A7, A3, XBOOLE_0:def 4;

      then

       A90: (p1 `2 ) = (p2 `2 ) implies i1 = i2 by A13, A14, A15, A16, A74, A61, A39, Th29, JORDAN1G: 7;

      

       A91: (p1 `1 ) = (p2 `1 ) implies j1 = j2 by A13, A14, A15, A16, A74, A61, A89, A39, Th29, JORDAN1G: 6;

      per cases by A2;

        suppose

         A92: (p1 `2 ) = (p2 `2 );

        ( Int ( right_cell (f,k,G))) <> {} by A12, A10, A11, JORDAN9: 9;

        then

        consider rp9 be object such that

         A93: rp9 in ( Int ( right_cell (f,k,G))) by XBOOLE_0:def 1;

        reconsider rp9 as Point of ( TOP-REAL 2) by A93;

        reconsider rp = |[(rp9 `1 ), (p `2 )]| as Point of ( TOP-REAL 2);

        

         A94: (p `2 ) = (p1 `2 ) by A5, A92, GOBOARD7: 6;

         A95:

        now

          assume

           A96: j1 = (j2 + 1) & 1 < i2;

          then ex r, s st rp9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A66, A79, A92, A93, Th29, JORDAN1G: 7;

          then ((G * ((i2 -' 1),1)) `1 ) < (rp9 `1 ) & (rp9 `1 ) < ((G * (((i2 -' 1) + 1),1)) `1 ) by EUCLID: 52;

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A79, A92, A96, Th29, JORDAN1G: 7;

        end;

         A97:

        now

          assume

           A98: j1 = (j2 + 1) & 1 = i2;

          then ex r, s st rp9 = |[r, s]| & r < ((G * (1,1)) `1 ) & ((G * (1,j2)) `2 ) < s & s < ((G * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A58, A92, A93, Th29, JORDAN1G: 7;

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

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A58, A92, A98, Th29, JORDAN1G: 7;

        end;

        ( Int ( left_cell (f,k,G))) <> {} by A12, A10, A11, JORDAN9: 9;

        then

        consider rl9 be object such that

         A99: rl9 in ( Int ( left_cell (f,k,G))) by XBOOLE_0:def 1;

        reconsider rl9 as Point of ( TOP-REAL 2) by A99;

        reconsider rl = |[(rl9 `1 ), (p `2 )]| as Point of ( TOP-REAL 2);

        

         A100: (rl `2 ) = (p `2 ) & (rp `2 ) = (p `2 ) by EUCLID: 52;

         A101:

        now

          assume

           A102: j2 = (j1 + 1) & 1 < i1;

          then ex r, s st rl9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A88, A86, A92, A99, Th29, JORDAN1G: 7;

          then ((G * ((i1 -' 1),1)) `1 ) < (rl9 `1 ) & (rl9 `1 ) < ((G * (((i1 -' 1) + 1),1)) `1 ) by EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A86, A92, A102, Th29, JORDAN1G: 7;

        end;

         A103:

        now

          assume

           A104: j2 = (j1 + 1) & 1 = i1;

          then ex r, s st rl9 = |[r, s]| & r < ((G * (1,1)) `1 ) & ((G * (1,j1)) `2 ) < s & s < ((G * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A63, A92, A99, Th29, JORDAN1G: 7;

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

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A63, A92, A104, Th29, JORDAN1G: 7;

        end;

        

         A105: (rl `1 ) = (rl9 `1 ) by EUCLID: 52;

         A106:

        now

          assume

           A107: j1 = (j2 + 1) & i2 = ( len G);

          then ex r, s st rl9 = |[r, s]| & ((G * (( len G),1)) `1 ) < r & ((G * (1,j2)) `2 ) < s & s < ((G * (1,(j2 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A66, A32, A92, A99, Th29, JORDAN1G: 7;

          then ((G * (( len G),1)) `1 ) < (rl `1 ) by A105, EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A32, A92, A105, A107, Th29, JORDAN1G: 7;

        end;

         A108:

        now

          assume

           A109: j2 = (j1 + 1) & i1 = ( len G);

          then ex r, s st rp9 = |[r, s]| & ((G * (( len G),1)) `1 ) < r & ((G * (1,j1)) `2 ) < s & s < ((G * (1,(j1 + 1))) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A88, A28, A92, A93, Th29, JORDAN1G: 7;

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

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A28, A92, A109, Th29, JORDAN1G: 7;

        end;

         A110:

        now

          assume

           A111: j2 = (j1 + 1) & i1 < ( len G);

          then ex r, s st rp9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A88, A62, A92, A93, Th29, JORDAN1G: 7;

          then ((G * (i1,1)) `1 ) < (rp9 `1 ) & (rp9 `1 ) < ((G * ((i1 + 1),1)) `1 ) by EUCLID: 52;

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A62, A92, A111, Th29, JORDAN1G: 7;

        end;

         A112:

        now

          assume

           A113: j1 = (j2 + 1) & i2 < ( len G);

          then ex r, s st rl9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A66, A34, A92, A99, Th29, JORDAN1G: 7;

          then ((G * (i2,1)) `1 ) < (rl `1 ) & (rl `1 ) < ((G * ((i2 + 1),1)) `1 ) by A105, EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A34, A92, A105, A113, Th29, JORDAN1G: 7;

        end;

        now

          per cases by A17, A90, A92;

            suppose

             A114: j1 = (j2 + 1);

            rp in ( Int ( right_cell (f,k,( GoB f))))

            proof

              per cases by A33, XXREAL_0: 1;

                suppose 1 < i2;

                hence thesis by A95, A114;

              end;

                suppose 1 = i2;

                hence thesis by A97, A114;

              end;

            end;

            then

             A115: rp in ( right_cell (f,k,( GoB f))) & not rp in ( L~ f) by A69;

            rl in ( Int ( left_cell (f,k,G)))

            proof

              per cases by A21, XXREAL_0: 1;

                suppose i2 < ( len G);

                hence thesis by A112, A114;

              end;

                suppose i2 = ( len G);

                hence thesis by A106, A114;

              end;

            end;

            then rl in ( left_cell (f,k,( GoB f))) & not rl in ( L~ f) by A67;

            hence thesis by A1, A7, A6, A9, A10, A11, A92, A94, A100, A115, Th31;

          end;

            suppose

             A116: j2 = (j1 + 1);

            rp in ( Int ( right_cell (f,k,( GoB f))))

            proof

              per cases by A35, XXREAL_0: 1;

                suppose i1 < ( len G);

                hence thesis by A110, A116;

              end;

                suppose i1 = ( len G);

                hence thesis by A108, A116;

              end;

            end;

            then

             A117: rp in ( right_cell (f,k,( GoB f))) & not rp in ( L~ f) by A69;

            rl in ( Int ( left_cell (f,k,G)))

            proof

              per cases by A18, XXREAL_0: 1;

                suppose 1 < i1;

                hence thesis by A101, A116;

              end;

                suppose 1 = i1;

                hence thesis by A103, A116;

              end;

            end;

            then rl in ( left_cell (f,k,( GoB f))) & not rl in ( L~ f) by A67;

            hence thesis by A1, A7, A6, A9, A10, A11, A92, A94, A100, A117, Th31;

          end;

        end;

        hence thesis;

      end;

        suppose

         A118: (p1 `1 ) = (p2 `1 );

        ( Int ( left_cell (f,k,G))) <> {} by A12, A10, A11, JORDAN9: 9;

        then

        consider rl9 be object such that

         A119: rl9 in ( Int ( left_cell (f,k,G))) by XBOOLE_0:def 1;

        reconsider rl9 as Point of ( TOP-REAL 2) by A119;

        reconsider rl = |[(p `1 ), (rl9 `2 )]| as Point of ( TOP-REAL 2);

        

         A120: (p `1 ) = (p1 `1 ) by A5, A118, GOBOARD7: 5;

        

         A121: (rl `2 ) = (rl9 `2 ) by EUCLID: 52;

         A122:

        now

          assume

           A123: i1 = (i2 + 1) & 1 = j1;

          then ex r, s st rl9 = |[r, s]| & ((G * (i2,1)) `1 ) < r & r < ((G * ((i2 + 1),1)) `1 ) & s < ((G * (1,1)) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A81, A46, A118, A119, Th29, JORDAN1G: 6;

          then (rl `2 ) < ((G * (1,1)) `2 ) by A121, EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A46, A118, A121, A123, Th29, JORDAN1G: 6;

        end;

         A124:

        now

          assume

           A125: i2 = (i1 + 1) & j1 < ( width G);

          then ex r, s st rl9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A49, A25, A118, A119, Th29, JORDAN1G: 6;

          then ((G * (1,j1)) `2 ) < (rl `2 ) & (rl `2 ) < ((G * (1,(j1 + 1))) `2 ) by A121, EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A25, A118, A121, A125, Th29, JORDAN1G: 6;

        end;

        ( Int ( right_cell (f,k,G))) <> {} by A12, A10, A11, JORDAN9: 9;

        then

        consider rp9 be object such that

         A126: rp9 in ( Int ( right_cell (f,k,G))) by XBOOLE_0:def 1;

        reconsider rp9 as Point of ( TOP-REAL 2) by A126;

        reconsider rp = |[(p `1 ), (rp9 `2 )]| as Point of ( TOP-REAL 2);

        

         A127: (rl `1 ) = (p `1 ) & (rp `1 ) = (p `1 ) by EUCLID: 52;

         A128:

        now

          assume

           A129: i2 = (i1 + 1) & 1 < j1;

          then ex r, s st rp9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A49, A41, A118, A126, Th29, JORDAN1G: 6;

          then ((G * (1,(j1 -' 1))) `2 ) < (rp9 `2 ) & (rp9 `2 ) < ((G * (1,((j1 -' 1) + 1))) `2 ) by EUCLID: 52;

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A41, A118, A129, Th29, JORDAN1G: 6;

        end;

         A130:

        now

          assume

           A131: i2 = (i1 + 1) & 1 = j1;

          then ex r, s st rp9 = |[r, s]| & ((G * (i1,1)) `1 ) < r & r < ((G * ((i1 + 1),1)) `1 ) & s < ((G * (1,1)) `2 ) by A13, A14, A15, A16, A74, A61, A89, A39, A49, A71, A118, A126, Th29, JORDAN1G: 6;

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

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A71, A118, A131, Th29, JORDAN1G: 6;

        end;

        

         A132: (rp `2 ) = (rp9 `2 ) by EUCLID: 52;

         A133:

        now

          assume

           A134: i1 = (i2 + 1) & j1 = ( width G);

          then ex r, s st rp9 = |[r, s]| & ((G * (i2,1)) `1 ) < r & r < ((G * ((i2 + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) < s by A13, A14, A15, A16, A74, A61, A89, A39, A81, A37, A118, A126, Th29, JORDAN1G: 6;

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

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A37, A118, A132, A134, Th29, JORDAN1G: 6;

        end;

         A135:

        now

          assume

           A136: i2 = (i1 + 1) & j1 = ( width G);

          then ex r, s st rl9 = |[r, s]| & ((G * (i1,1)) `1 ) < r & r < ((G * ((i1 + 1),1)) `1 ) & ((G * (1,( width G))) `2 ) < s by A13, A14, A15, A16, A74, A61, A89, A39, A49, A23, A118, A119, Th29, JORDAN1G: 6;

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

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A23, A118, A136, Th29, JORDAN1G: 6;

        end;

         A137:

        now

          assume

           A138: i1 = (i2 + 1) & 1 < j1;

          then ex r, s st rl9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A81, A44, A118, A119, Th29, JORDAN1G: 6;

          then ((G * (1,(j1 -' 1))) `2 ) < (rl9 `2 ) & (rl9 `2 ) < ((G * (1,((j1 -' 1) + 1))) `2 ) by EUCLID: 52;

          hence rl in ( Int ( left_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A44, A118, A138, Th29, JORDAN1G: 6;

        end;

         A139:

        now

          assume

           A140: i1 = (i2 + 1) & j1 < ( width G);

          then ex r, s st rp9 = |[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 A13, A14, A15, A16, A74, A61, A89, A39, A81, A43, A118, A126, Th29, JORDAN1G: 6;

          then ((G * (1,j1)) `2 ) < (rp `2 ) & (rp `2 ) < ((G * (1,(j1 + 1))) `2 ) by A132, EUCLID: 52;

          hence rp in ( Int ( right_cell (f,k,G))) by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A43, A118, A132, A140, Th29, JORDAN1G: 6;

        end;

        now

          per cases by A17, A91, A118;

            suppose

             A141: i1 = (i2 + 1);

            rp in ( Int ( right_cell (f,k,( GoB f))))

            proof

              per cases by A30, XXREAL_0: 1;

                suppose j1 < ( width G);

                hence thesis by A139, A141;

              end;

                suppose j1 = ( width G);

                hence thesis by A133, A141;

              end;

            end;

            then

             A142: rp in ( right_cell (f,k,( GoB f))) & not rp in ( L~ f) by A69;

            rl in ( Int ( left_cell (f,k,G)))

            proof

              per cases by A24, XXREAL_0: 1;

                suppose 1 < j1;

                hence thesis by A137, A141;

              end;

                suppose 1 = j1;

                hence thesis by A122, A141;

              end;

            end;

            then rl in ( left_cell (f,k,( GoB f))) & not rl in ( L~ f) by A67;

            hence thesis by A1, A7, A6, A9, A10, A11, A118, A120, A127, A142, Th31;

          end;

            suppose

             A143: i2 = (i1 + 1);

            rl in ( Int ( left_cell (f,k,( GoB f))))

            proof

              per cases by A30, XXREAL_0: 1;

                suppose j1 < ( width G);

                hence thesis by A124, A143;

              end;

                suppose j1 = ( width G);

                hence thesis by A135, A143;

              end;

            end;

            then

             A144: rl in ( left_cell (f,k,( GoB f))) & not rl in ( L~ f) by A67;

            rp in ( Int ( right_cell (f,k,G)))

            proof

              per cases by A24, XXREAL_0: 1;

                suppose 1 < j1;

                hence thesis by A128, A143;

              end;

                suppose 1 = j1;

                hence thesis by A130, A143;

              end;

            end;

            then rp in ( right_cell (f,k,( GoB f))) & not rp in ( L~ f) by A69;

            hence thesis by A1, A7, A6, A9, A10, A11, A118, A120, A127, A144, Th31;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN12:33

    

     Th33: for f be non constant standard special_circular_sequence, g be special FinSequence of ( TOP-REAL 2) st (f,g) are_in_general_position holds for k st 1 <= k & (k + 1) <= ( len g) holds ( card (( L~ f) /\ ( LSeg (g,k)))) is even Element of 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 be special FinSequence of ( TOP-REAL 2) such that

       A1: (f,g) are_in_general_position ;

      

       A2: g is_in_general_position_wrt f by A1;

      let k such that

       A3: 1 <= k and

       A4: (k + 1) <= ( len g);

      

       A5: (g . k) in (( L~ f) ` ) by A1, A3, A4, Th8;

      then

       A6: not (g . k) in ( L~ f) by XBOOLE_0:def 5;

      

       A7: (g . (k + 1)) in (( L~ f) ` ) by A1, A3, A4, Th8;

      then

       A8: not (g . (k + 1)) in ( L~ f) by XBOOLE_0:def 5;

      

       A9: k < ( len g) by A4, NAT_1: 13;

      then

       A10: k in ( dom g) by A3, FINSEQ_3: 25;

      then

       A11: (g /. k) = (g . k) by PARTFUN1:def 6;

      then

       A12: (g . k) in ( LSeg (g,k)) by A3, A4, TOPREAL1: 21;

      set m = (( L~ f) /\ ( LSeg (g,k)));

      set p1 = (g /. k), p2 = (g /. (k + 1));

      

       A13: ( LSeg (g,k)) = ( LSeg (p1,p2)) by A3, A4, TOPREAL1:def 3;

      ( LSeg (g,k)) is vertical or ( LSeg (g,k)) is horizontal by SPPOL_1: 19;

      then

       A14: (p1 `1 ) = (p2 `1 ) or (p1 `2 ) = (p2 `2 ) by A13, SPPOL_1: 15, SPPOL_1: 16;

      

       A15: ( rng g) c= the carrier of ( TOP-REAL 2) by FINSEQ_1:def 4;

      1 <= (k + 1) by A3, NAT_1: 13;

      then

       A16: (k + 1) in ( dom g) by A4, FINSEQ_3: 25;

      then

       A17: (g /. (k + 1)) = (g . (k + 1)) by PARTFUN1:def 6;

      then

       A18: (g . (k + 1)) in ( LSeg (g,k)) by A3, A4, TOPREAL1: 21;

      (g . (k + 1)) in ( rng g) by A16, FUNCT_1: 3;

      then

      reconsider gk1 = (g . (k + 1)) as Point of ( TOP-REAL 2) by A15;

      (g . k) in ( rng g) by A10, FUNCT_1: 3;

      then

      reconsider gk = (g . k) as Point of ( TOP-REAL 2) by A15;

      ( LSeg (gk,gk1)) = ( LSeg (g,k)) by A3, A4, A11, A17, TOPREAL1:def 3;

      then

       A19: ( LSeg (g,k)) is convex;

      

       A20: f is_in_general_position_wrt g by A1;

      then

       A21: ( L~ f) misses ( rng g);

      per cases ;

        suppose

         A22: not m = {} ;

        m is trivial by A3, A9, A20;

        then

        consider x be object such that

         A23: m = {x} by A22, ZFMISC_1: 131;

        x in m by A23, TARSKI:def 1;

        then

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

        

         A24: p2 = (g . (k + 1)) by A16, PARTFUN1:def 6;

        then

         A25: p2 in ( rng g) by A16, FUNCT_1: 3;

        

         A26: p1 = (g . k) by A10, PARTFUN1:def 6;

        then

         A27: p1 in ( rng g) by A10, FUNCT_1: 3;

         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 A21, A27, XBOOLE_0: 3;

          end;

            suppose p2 in ( L~ f);

            hence contradiction by A21, A25, XBOOLE_0: 3;

          end;

        end;

        ( rng f) misses ( L~ g) by A2;

        then

         A30: ( rng f) misses ( LSeg (p1,p2)) by A13, TOPREAL3: 19, XBOOLE_1: 63;

        (( L~ f) /\ ( LSeg (p1,p2))) = {p} by A3, A4, A23, TOPREAL1:def 3;

        hence thesis by A14, A23, A26, A24, A28, A30, Th2, Th32, CARD_1: 30;

      end;

        suppose

         A31: m = {} ;

        then

         A32: ( LSeg (g,k)) misses ( L~ f);

        then

         A33: not ((g . (k + 1)) in ( RightComp f) & (g . k) in ( LeftComp f)) by A19, A12, A18, JORDAN1J: 36;

         A34:

        now

          per cases by A19, A12, A18, A32, JORDAN1J: 36;

            suppose

             A35: not gk in ( RightComp f);

            

             A36: ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

            gk in ( LeftComp f) & (g . (k + 1)) in ( LeftComp f) by A6, A7, A8, A33, A35, GOBRD14: 17;

            hence ex C 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;

          end;

            suppose

             A37: not (g . (k + 1)) in ( LeftComp f);

            

             A38: ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

            (g . (k + 1)) in ( RightComp f) & (g . k) in ( RightComp f) by A5, A6, A7, A8, A33, A37, GOBRD14: 18;

            hence ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ f) ` ) & (g . k) in C & (g . (k + 1)) in C by A38;

          end;

        end;

        ( card m) = (2 * 0 ) by A31, CARD_1: 27;

        hence thesis by A34;

      end;

    end;

    theorem :: JORDAN12:34

    

     Th34: for f1,f2,g1 be 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 Element of 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 be special FinSequence of ( TOP-REAL 2) such that

       A1: (f1 ^' f2) is non constant standard special_circular_sequence and

       A2: ((f1 ^' f2),g1) are_in_general_position and

       A3: ( len g1) >= 2 and

       A4: g1 is unfolded s.n.c.;

      reconsider g1 as special unfolded s.n.c. FinSequence of ( TOP-REAL 2) by A4;

      set Lf = ( L~ (f1 ^' f2));

      (f1 ^' f2) is_in_general_position_wrt g1 by A2;

      then

       A5: Lf misses ( rng g1);

      defpred P[ Nat] means $1 <= ( len g1) implies for a be FinSequence of ( TOP-REAL 2) st a = (g1 | ( Seg $1)) holds (( card (Lf /\ ( L~ a))) is even Element of 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));

      

       A6: ( dom g1) = ( Seg ( len g1)) by FINSEQ_1:def 3;

      

       A7: (1 + 1) <= ( len g1) by A3;

       A8:

      now

        let k be Nat such that

         A9: k >= 2 and

         A10: P[k];

        

         A11: 1 <= k by A9, XXREAL_0: 2;

        then

         A12: 1 <= (k + 1) by NAT_1: 13;

        now

          reconsider b = (g1 | ( Seg k)) as FinSequence of ( TOP-REAL 2) by FINSEQ_1: 18;

          1 in ( Seg k) by A11, FINSEQ_1: 1;

          then

           A13: (b . 1) = (g1 . 1) by FUNCT_1: 49;

          reconsider s1 = (Lf /\ ( L~ b)) as finite set by A2, Th6, Th11;

          set c = ( LSeg (g1,k));

          

           A14: k in ( Seg k) by A11, FINSEQ_1: 1;

          reconsider s2 = (Lf /\ c) as finite set by A2, Th12;

          

           A15: k <= (k + 1) by NAT_1: 13;

          then

           A16: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

          k >= (1 + 1) by A9;

          then

           A17: 1 < k by NAT_1: 13;

          

           A18: (g1 . 1) in (Lf ` ) by A2, A7, Th8;

          assume

           A19: (k + 1) <= ( len g1);

          then

           A20: (g1 . (k + 1)) in (Lf ` ) & (g1 . k) in (Lf ` ) by A2, A11, Th8;

          let a be FinSequence of ( TOP-REAL 2) such that

           A21: a = (g1 | ( Seg (k + 1)));

          

           A22: ( dom a) = (( dom g1) /\ ( Seg (k + 1))) by A21, RELAT_1: 61;

          

           A23: (k + 1) in ( Seg (k + 1)) by A12, FINSEQ_1: 1;

          

          then

           A24: (g1 . (k + 1)) = (a . (k + 1)) by A21, FUNCT_1: 49

          .= (a . ( len a)) by A19, A21, FINSEQ_1: 17;

          

           A25: (k + 1) in ( Seg ( len g1)) by A12, A19, FINSEQ_1: 1;

          then

           A26: (k + 1) in ( dom a) by A6, A23, A22, XBOOLE_0:def 4;

          

          then

           A27: (a /. (k + 1)) = (a . (k + 1)) by PARTFUN1:def 6

          .= (g1 . (k + 1)) by A21, A26, FUNCT_1: 47

          .= (g1 /. (k + 1)) by A6, A25, PARTFUN1:def 6;

          

           A28: ( len a) = (k + 1) by A19, A21, FINSEQ_1: 17;

          (g1 | (k + 1)) = a by A21, FINSEQ_1:def 15;

          then (( L~ (a | k)) /\ ( LSeg (a,k))) = {(a /. k)} by A28, A17, GOBOARD2: 4;

          then

           A29: (( L~ (a | k)) /\ ( LSeg ((a /. k),(a /. (k + 1))))) = {(a /. k)} by A11, A28, TOPREAL1:def 3;

          1 in ( Seg (k + 1)) by A12, FINSEQ_1: 1;

          then

           A30: (g1 . 1) = (a . 1) by A21, FUNCT_1: 49;

          reconsider s = (Lf /\ ( L~ a)) as finite set by A2, A21, Th6, Th11;

          

           A31: a = (g1 | (k + 1)) by A21, FINSEQ_1:def 15;

          

           A32: k < ( len g1) by A19, NAT_1: 13;

          then

           A33: k in ( dom g1) by A6, A11, FINSEQ_1: 1;

          

           A34: (a | k) = ((g1 | ( Seg (k + 1))) | ( Seg k)) by A21, FINSEQ_1:def 15

          .= (g1 | ( Seg k)) by A16, FUNCT_1: 51

          .= (g1 | k) by FINSEQ_1:def 15;

          

           A35: (b . ( len b)) = (b . k) by A32, FINSEQ_1: 17

          .= (g1 . k) by A14, FUNCT_1: 49;

          k in ( Seg (k + 1)) by A11, A15, FINSEQ_1: 1;

          then

           A36: k in ( dom a) by A33, A22, XBOOLE_0:def 4;

          

          then (a /. k) = (a . k) by PARTFUN1:def 6

          .= (g1 . k) by A21, A36, FUNCT_1: 47

          .= (g1 /. k) by A33, PARTFUN1:def 6;

          then (( L~ b) /\ ( LSeg ((g1 /. k),(g1 /. (k + 1))))) = {(g1 /. k)} by A34, A27, A29, FINSEQ_1:def 15;

          then (( L~ b) /\ ( LSeg (g1,k))) = {(g1 /. k)} by A11, A19, TOPREAL1:def 3;

          then

           A37: (( L~ b) /\ c) = {(g1 . k)} by A33, PARTFUN1:def 6;

          

           A38: s1 misses s2

          proof

            assume s1 meets s2;

            then

            consider x be object such that

             A39: x in s1 and

             A40: x in s2 by XBOOLE_0: 3;

            x in ( L~ b) & x in c by A39, A40, XBOOLE_0:def 4;

            then x in (( L~ b) /\ c) by XBOOLE_0:def 4;

            then x = (g1 . k) by A37, TARSKI:def 1;

            then

             A41: x in ( rng g1) by A33, FUNCT_1: 3;

            x in Lf by A39, XBOOLE_0:def 4;

            hence contradiction by A5, A41, XBOOLE_0: 3;

          end;

          (k + 1) in ( dom g1) by A6, A12, A19, FINSEQ_1: 1;

          

          then ( L~ a) = (( L~ (g1 | k)) \/ ( LSeg ((g1 /. k),(g1 /. (k + 1))))) by A33, A31, TOPREAL3: 38

          .= (( L~ b) \/ ( LSeg ((g1 /. k),(g1 /. (k + 1))))) by FINSEQ_1:def 15

          .= (( L~ b) \/ c) by A11, A19, TOPREAL1:def 3;

          then

           A42: s = (s1 \/ s2) by XBOOLE_1: 23;

          per cases ;

            suppose

             A43: ( card s1) is even Element of NAT ;

            then

            reconsider c1 = ( card (Lf /\ ( L~ b))) as even Integer;

            now

              per cases ;

                suppose

                 A44: ( card s2) is even Element of NAT ;

                then

                reconsider c2 = ( card (Lf /\ c)) as even Integer;

                reconsider c = ( card s) as Integer;

                

                 A45: c = (c1 + c2) & 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 A10, A19, A42, A38, A43, CARD_2: 40, NAT_1: 13;

                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, A2, A11, A19, A44, Th33;

                hence ( card (Lf /\ ( L~ a))) is even Element of 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, A30, A24, A13, A35, A45, Th16;

              end;

                suppose

                 A46: not ( card s2) is even Element of NAT ;

                then

                reconsider c2 = ( card (Lf /\ c)) as odd Integer;

                reconsider c = ( card s) as Integer;

                

                 A47: c = (c1 + c2) & 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 A10, A19, A42, A38, A43, CARD_2: 40, NAT_1: 13;

                 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, A2, A11, A19, A46, Th33;

                hence ( card (Lf /\ ( L~ a))) is even Element of 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, A30, A24, A13, A35, A47, Th16;

              end;

            end;

            hence ( card (Lf /\ ( L~ a))) is even Element of 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;

            suppose

             A48: not ( card s1) is even Element of NAT ;

            then

            reconsider c1 = ( card (Lf /\ ( L~ b))) as odd Integer;

            now

              per cases ;

                suppose

                 A49: ( card s2) is even Element of NAT ;

                then

                reconsider c2 = ( card (Lf /\ c)) as even Integer;

                reconsider c = ( card s) as Integer;

                

                 A50: c = (c1 + c2) & 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 A10, A19, A42, A38, A48, CARD_2: 40, NAT_1: 13;

                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, A2, A11, A19, A49, Th33;

                hence ( card (Lf /\ ( L~ a))) is even Element of 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, A30, A24, A13, A35, A50, Th16;

              end;

                suppose

                 A51: not ( card s2) is even Element of NAT ;

                then

                reconsider c2 = ( card (Lf /\ c)) as odd Integer;

                reconsider c = ( card s) as Integer;

                

                 A52: c = (c1 + c2) & 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 A10, A19, A42, A38, A48, CARD_2: 40, NAT_1: 13;

                 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, A2, A11, A19, A51, Th33;

                hence ( card (Lf /\ ( L~ a))) is even Element of 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, A30, A18, A20, A24, A13, A35, A52, Th17;

              end;

            end;

            hence ( card (Lf /\ ( L~ a))) is even Element of 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;

        end;

        hence P[(k + 1)];

      end;

      ( dom g1) = ( Seg ( len g1)) by FINSEQ_1:def 3;

      then

       A53: (g1 | ( Seg ( len g1))) = g1;

      

       A54: 2 in ( dom g1) by A3, FINSEQ_3: 25;

      

       A55: 1 <= ( len g1) by A3, XXREAL_0: 2;

      then

       A56: 1 in ( dom g1) by FINSEQ_3: 25;

      now

        (g1 | 1) = (g1 | ( Seg 1)) by FINSEQ_1:def 15;

        then

         A57: ( len (g1 | 1)) = 1 by A55, FINSEQ_1: 17;

        

         A58: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

        let a be FinSequence of ( TOP-REAL 2) such that

         A59: a = (g1 | ( Seg 2));

        

         A60: (a . ( len a)) = (a . 2) by A3, A59, FINSEQ_1: 17

        .= (g1 . (1 + 1)) by A59, A58, FUNCT_1: 49;

        1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

        then

         A61: (a . 1) = (g1 . 1) by A59, FUNCT_1: 49;

        ( L~ a) = ( L~ (g1 | 2)) by A59, FINSEQ_1:def 15

        .= (( L~ (g1 | 1)) \/ ( LSeg ((g1 /. 1),(g1 /. (1 + 1))))) by A56, A54, TOPREAL3: 38

        .= (( L~ (g1 | 1)) \/ ( LSeg (g1,1))) by A3, TOPREAL1:def 3

        .= ( {} \/ ( LSeg (g1,1))) by A57, TOPREAL1: 22

        .= ( LSeg (g1,1));

        hence ( card (Lf /\ ( L~ a))) is even Element of 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, A3, A61, A60, Th33;

      end;

      then

       A62: P[2];

      for k be Nat st k >= 2 holds P[k] from NAT_1:sch 8( A62, A8);

      hence thesis by A3, A53;

    end;

    theorem :: JORDAN12:35

    for f1,f2,g1,g2 be 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 be 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 holds 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 & (f1 . ( len f1)) = p2 and

       A7: (g1 . 1) = q1 & (g1 . ( len g1)) = q2 and

       A8: (f1 /. ( len f1)) = (f2 /. 1) and

       A9: (g1 /. ( len g1)) = (g2 /. 1) and

       A10: p1 in (( L~ f1) /\ ( L~ f2)) and

       A11: q1 in (( L~ g1) /\ ( L~ g2)) and

       A12: ex C be Subset of ( TOP-REAL 2) st C is_a_component_of (( L~ (f1 ^' f2)) ` ) & q1 in C & q2 in C;

      

       A13: ((f1 ^' f2),g1) are_in_general_position by A5, Th7;

       A14:

      now

        assume

         A15: ( len f1) = 0 or ( len f1) = 1 or ( len f2) = 0 or ( len f2) = 1;

        per cases by A15;

          suppose ( len f1) = 0 or ( len f1) = 1;

          then ( L~ f1) = {} by TOPREAL1: 22;

          hence contradiction by A10;

        end;

          suppose ( len f2) = 0 or ( len f2) = 1;

          then ( L~ f2) = {} by TOPREAL1: 22;

          hence contradiction by A10;

        end;

      end;

      then

       A16: ( len f2) is non trivial by NAT_2:def 1;

      then

       A17: f2 is non trivial by Lm2;

       A18:

      now

        assume

         A19: ( len g1) = 0 or ( len g1) = 1 or ( len g2) = 0 or ( len g2) = 1;

        per cases by A19;

          suppose ( len g1) = 0 or ( len g1) = 1;

          then ( L~ g1) = {} by TOPREAL1: 22;

          hence contradiction by A11;

        end;

          suppose ( len g2) = 0 or ( len g2) = 1;

          then ( L~ g2) = {} by TOPREAL1: 22;

          hence contradiction by A11;

        end;

      end;

      then

       A20: ( len g2) is non trivial by NAT_2:def 1;

      then

       A21: g2 is non trivial by Lm2;

      

       A22: ( len g1) is non trivial by A18, NAT_2:def 1;

      then

       A23: g1 is non empty by Lm2;

      ( len g2) >= (1 + 1) by A20, NAT_2: 29;

      then

       A24: g1 is unfolded s.n.c. by A2, Th4;

      ( len g1) >= 2 by A22, NAT_2: 29;

      then

       A25: ( card (( L~ (f1 ^' f2)) /\ ( L~ g1))) is even Element of NAT by A1, A7, A12, A13, A24, Th34;

      ( len f2) >= (1 + 1) by A16, NAT_2: 29;

      then

       A26: f1 is unfolded s.n.c. by A1, Th4;

      

       A27: ((g1 ^' g2),f1) are_in_general_position by A5, Th7;

      

       A28: ( len f1) is non trivial by A14, NAT_2:def 1;

      then f1 is non empty by Lm2;

      

      then

       A29: (( L~ (f1 ^' f2)) /\ ( L~ g1)) = ((( L~ f1) \/ ( L~ f2)) /\ ( L~ g1)) by A8, A17, TOPREAL8: 35

      .= ((( L~ f1) /\ ( L~ g1)) \/ (( L~ f2) /\ ( L~ g1))) by XBOOLE_1: 23

      .= ((( L~ f1) /\ ( L~ g1)) \/ {} ) by A4

      .= ((( L~ f1) /\ ( L~ g1)) \/ (( L~ f1) /\ ( L~ g2))) by A3

      .= ((( L~ g1) \/ ( L~ g2)) /\ ( L~ f1)) by XBOOLE_1: 23

      .= (( L~ f1) /\ ( L~ (g1 ^' g2))) by A9, A23, A21, TOPREAL8: 35;

      ( len f1) >= 2 by A28, NAT_2: 29;

      hence thesis by A2, A6, A29, A27, A26, A25, Th34;

    end;