jordan5b.miz



    begin

    theorem :: JORDAN5B:1

    

     Th1: for i1 be Nat st 1 <= i1 holds (i1 -' 1) < i1

    proof

      let i1 be Nat;

      assume

       A1: 1 <= i1;

      (i1 - 1) < (i1 - 0 ) by XREAL_1: 15;

      hence thesis by A1, XREAL_1: 233;

    end;

    theorem :: JORDAN5B:2

    for i,k be Nat holds (i + 1) <= k implies 1 <= (k -' i)

    proof

      let i,k be Nat;

      assume (i + 1) <= k;

      then ((i + 1) -' i) <= (k -' i) by NAT_D: 42;

      hence thesis by NAT_D: 34;

    end;

    theorem :: JORDAN5B:3

    for i,k be Nat holds 1 <= i & 1 <= k implies ((k -' i) + 1) <= k

    proof

      let i,k be Nat;

      assume that

       A1: 1 <= i and

       A2: 1 <= k;

      (k -' i) <= (k -' 1) by A1, NAT_D: 41;

      then ((k -' i) + 1) <= ((k -' 1) + 1) by XREAL_1: 6;

      hence thesis by A2, XREAL_1: 235;

    end;

    

     Lm1: for r be Real st 0 <= r & r <= 1 holds 0 <= (1 - r) & (1 - r) <= 1

    proof

      let r be Real;

      assume that

       A1: 0 <= r and

       A2: r <= 1;

      

       A3: (1 - 1) <= (1 - r) by A2, XREAL_1: 13;

      (1 - r) <= (1 - 0 ) by A1, XREAL_1: 13;

      hence thesis by A3;

    end;

    theorem :: JORDAN5B:4

    for r be Real st r in the carrier of I[01] holds (1 - r) in the carrier of I[01]

    proof

      let r be Real;

      assume

       A1: r in the carrier of I[01] ;

      then

       A2: 0 <= r by BORSUK_1: 43;

      

       A3: r <= 1 by A1, BORSUK_1: 43;

      then

       A4: 0 <= (1 - r) by A2, Lm1;

      (1 - r) <= 1 by A2, A3, Lm1;

      hence thesis by A4, BORSUK_1: 43;

    end;

    theorem :: JORDAN5B:5

    for p,q,p1 be Point of ( TOP-REAL 2) st (p `2 ) <> (q `2 ) & p1 in ( LSeg (p,q)) holds ((p1 `2 ) = (p `2 ) implies p1 = p)

    proof

      let p,q,p1 be Point of ( TOP-REAL 2);

      assume that

       A1: (p `2 ) <> (q `2 ) and

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

      assume

       A3: (p1 `2 ) = (p `2 );

      assume

       A4: p1 <> p;

      consider l1 be Real such that

       A5: p1 = (((1 - l1) * p) + (l1 * q)) and 0 <= l1 and l1 <= 1 by A2;

      

       A6: (((1 - l1) * p) + (l1 * q)) = |[((((1 - l1) * p) `1 ) + ((l1 * q) `1 )), ((((1 - l1) * p) `2 ) + ((l1 * q) `2 ))]| by EUCLID: 55;

      

       A7: ((1 - l1) * p) = |[((1 - l1) * (p `1 )), ((1 - l1) * (p `2 ))]| by EUCLID: 57;

      

       A8: (l1 * q) = |[(l1 * (q `1 )), (l1 * (q `2 ))]| by EUCLID: 57;

      (p `2 ) = ((((1 - l1) * p) `2 ) + ((l1 * q) `2 )) by A3, A5, A6, EUCLID: 52

      .= (((1 - l1) * (p `2 )) + ((l1 * q) `2 )) by A7, EUCLID: 52

      .= (((1 - l1) * (p `2 )) + (l1 * (q `2 ))) by A8, EUCLID: 52;

      then ((1 - (1 - l1)) * (p `2 )) = (l1 * (q `2 ));

      then l1 = 0 by A1, XCMPLX_1: 5;

      

      then p1 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A5, RLVECT_1: 10

      .= (p + ( 0. ( TOP-REAL 2))) by RLVECT_1:def 8

      .= p by RLVECT_1: 4;

      hence thesis by A4;

    end;

    theorem :: JORDAN5B:6

    for p,q,p1 be Point of ( TOP-REAL 2) st (p `1 ) <> (q `1 ) & p1 in ( LSeg (p,q)) holds ((p1 `1 ) = (p `1 ) implies p1 = p)

    proof

      let p,q,p1 be Point of ( TOP-REAL 2);

      assume that

       A1: (p `1 ) <> (q `1 ) and

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

      assume

       A3: (p1 `1 ) = (p `1 );

      assume

       A4: p1 <> p;

      consider l1 be Real such that

       A5: p1 = (((1 - l1) * p) + (l1 * q)) and 0 <= l1 and l1 <= 1 by A2;

      

       A6: (((1 - l1) * p) + (l1 * q)) = |[((((1 - l1) * p) `1 ) + ((l1 * q) `1 )), ((((1 - l1) * p) `2 ) + ((l1 * q) `2 ))]| by EUCLID: 55;

      

       A7: ((1 - l1) * p) = |[((1 - l1) * (p `1 )), ((1 - l1) * (p `2 ))]| by EUCLID: 57;

      

       A8: (l1 * q) = |[(l1 * (q `1 )), (l1 * (q `2 ))]| by EUCLID: 57;

      (p `1 ) = ((((1 - l1) * p) `1 ) + ((l1 * q) `1 )) by A3, A5, A6, EUCLID: 52

      .= (((1 - l1) * (p `1 )) + ((l1 * q) `1 )) by A7, EUCLID: 52

      .= (((1 - l1) * (p `1 )) + (l1 * (q `1 ))) by A8, EUCLID: 52;

      then ((1 - (1 - l1)) * (p `1 )) = (l1 * (q `1 ));

      then l1 = 0 by A1, XCMPLX_1: 5;

      

      then p1 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A5, RLVECT_1: 10

      .= (p + ( 0. ( TOP-REAL 2))) by RLVECT_1:def 8

      .= p by RLVECT_1: 4;

      hence thesis by A4;

    end;

    reconsider jj = 1 as Real;

    theorem :: JORDAN5B:7

    

     Th7: for f be FinSequence of ( TOP-REAL 2), P be non empty Subset of ( TOP-REAL 2), F be Function of I[01] , (( TOP-REAL 2) | P), i be Nat st 1 <= i & (i + 1) <= ( len f) & f is being_S-Seq & P = ( L~ f) & F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) holds ex p1,p2 be Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & ( LSeg (f,i)) = (F .: [.p1, p2.]) & (F . p1) = (f /. i) & (F . p2) = (f /. (i + 1))

    proof

      let f be FinSequence of ( TOP-REAL 2), P be non empty Subset of ( TOP-REAL 2), Ff be Function of I[01] , (( TOP-REAL 2) | P), i be Nat;

      assume that

       A1: 1 <= i and

       A2: (i + 1) <= ( len f) and

       A3: f is being_S-Seq and

       A4: P = ( L~ f) and

       A5: Ff is being_homeomorphism and

       A6: (Ff . 0 ) = (f /. 1) and

       A7: (Ff . 1) = (f /. ( len f));

      

       A8: f is one-to-one by A3;

      

       A9: the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2), 1.] by TOPMETR: 18;

      

       A10: ( [#] ( Closed-Interval-TSpace ( 0 ,(1 / 2)))) = [. 0 , (1 / 2).] by TOPMETR: 18;

      

       A11: ( [#] ( Closed-Interval-TSpace ((1 / 2),1))) = [.(1 / 2), 1.] by TOPMETR: 18;

      

       A12: ( len f) >= 2 by A3, TOPREAL1:def 8;

      deffunc Q( Nat) = ( L~ (f | ($1 + 2)));

      defpred ARC[ Nat] means 1 <= ($1 + 2) & ($1 + 2) <= ( len f) implies ex NE be non empty Subset of ( TOP-REAL 2) st NE = Q($1) & for j be Nat holds for F be Function of I[01] , (( TOP-REAL 2) | NE) st 1 <= j & (j + 1) <= ($1 + 2) & F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. ($1 + 2)) holds ex p1,p2 be Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & ( LSeg (f,j)) = (F .: [.p1, p2.]) & (F . p1) = (f /. j) & (F . p2) = (f /. (j + 1));

      reconsider h1 = (( len f) - 2) as Element of NAT by A12, INT_1: 5;

      

       A13: (f | ( len f)) = (f | ( Seg ( len f))) by FINSEQ_1:def 15

      .= (f | ( dom f)) by FINSEQ_1:def 3

      .= f by RELAT_1: 68;

      

       A14: ARC[ 0 ]

      proof

        assume that

         A15: 1 <= ( 0 + 2) and

         A16: ( 0 + 2) <= ( len f);

        

         A17: 1 <= ( len (f | 2)) by A15, A16, FINSEQ_1: 59;

        

         A18: 2 <= ( len (f | 2)) by A16, FINSEQ_1: 59;

        then

        reconsider NE = Q(0) as non empty Subset of ( TOP-REAL 2) by TOPREAL1: 23;

        take NE;

        thus NE = Q(0);

        let j be Nat;

        let F be Function of I[01] , (( TOP-REAL 2) | NE);

        assume that

         A19: 1 <= j and

         A20: (j + 1) <= ( 0 + 2) and

         A21: F is being_homeomorphism and

         A22: (F . 0 ) = (f /. 1) and

         A23: (F . 1) = (f /. ( 0 + 2));

        j <= ((1 + 1) - 1) by A20, XREAL_1: 19;

        then

         A24: j = 1 by A19, XXREAL_0: 1;

        

         A25: ( len (f | 2)) = 2 by A16, FINSEQ_1: 59;

        

         A26: 1 in ( dom (f | 2)) by A17, FINSEQ_3: 25;

        

         A27: 2 in ( dom (f | 2)) by A18, FINSEQ_3: 25;

        

         A28: ((f | 2) /. 1) = ((f | 2) . 1) by A26, PARTFUN1:def 6;

        

         A29: ((f | 2) /. 2) = ((f | 2) . 2) by A27, PARTFUN1:def 6;

        

         A30: ((f | 2) /. 1) = (f /. 1) by A26, FINSEQ_4: 70;

        

         A31: (1 + 1) <= ( len f) by A16;

        

         A32: ( rng F) = ( [#] (( TOP-REAL 2) | NE)) by A21, TOPS_2:def 5

        .= ( L~ (f | 2)) by PRE_TOPC:def 5

        .= ( L~ <*((f | 2) /. 1), ((f | 2) /. 2)*>) by A25, A28, A29, FINSEQ_1: 44

        .= ( LSeg (((f | 2) /. 1),((f | 2) /. 2))) by SPPOL_2: 21

        .= ( LSeg ((f /. 1),(f /. 2))) by A27, A30, FINSEQ_4: 70

        .= ( LSeg (f,1)) by A31, TOPREAL1:def 3;

        take 0 , jj;

        thus thesis by A22, A23, A24, A32, BORSUK_1: 40, RELSET_1: 22;

      end;

      

       A33: for n be Nat st ARC[n] holds ARC[(n + 1)]

      proof

        let n be Nat;

        assume

         A34: ARC[n];

        assume that

         A35: 1 <= ((n + 1) + 2) and

         A36: ((n + 1) + 2) <= ( len f);

        

         A37: 2 <= (n + 2) by NAT_1: 11;

        (n + 2) <= ((n + 2) + 1) by NAT_1: 11;

        then

        consider NE be non empty Subset of ( TOP-REAL 2) such that

         A38: NE = Q(n) and

         A39: for j be Nat holds for F be Function of I[01] , (( TOP-REAL 2) | NE) st 1 <= j & (j + 1) <= (n + 2) & F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. (n + 2)) holds ex p1,p2 be Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & ( LSeg (f,j)) = (F .: [.p1, p2.]) & (F . p1) = (f /. j) & (F . p2) = (f /. (j + 1)) by A34, A36, A37, XXREAL_0: 2;

        

         A40: ( len (f | ((n + 1) + 2))) = ((n + 1) + 2) by A36, FINSEQ_1: 59;

        

         A41: ((n + 1) + 2) = ((n + 2) + 1);

        

         A42: 1 <= ((n + 1) + 1) by NAT_1: 11;

        

         A43: ((n + 1) + 1) <= ((n + 2) + 1) by NAT_1: 11;

        then

         A44: ((n + 1) + 1) <= ( len f) by A36, XXREAL_0: 2;

        

         A45: (n + 2) <= ( len f) by A36, A43, XXREAL_0: 2;

        

         A46: (n + 2) in ( dom (f | (n + 3))) by A40, A42, A43, FINSEQ_3: 25;

        then

         A47: (f /. (n + 2)) = ((f | (n + 3)) /. (n + 2)) by FINSEQ_4: 70;

        reconsider NE1 = Q(+) as non empty Subset of ( TOP-REAL 2) by A40, NAT_1: 11, TOPREAL1: 23;

        take NE1;

        thus NE1 = Q(+);

        let j be Nat, G be Function of I[01] , (( TOP-REAL 2) | NE1);

        assume that

         A48: 1 <= j and

         A49: (j + 1) <= ((n + 1) + 2) and

         A50: G is being_homeomorphism and

         A51: (G . 0 ) = (f /. 1) and

         A52: (G . 1) = (f /. ((n + 1) + 2));

        

         A53: G is one-to-one by A50, TOPS_2:def 5;

        

         A54: ( rng G) = ( [#] (( TOP-REAL 2) | Q(+))) by A50, TOPS_2:def 5;

        

         A55: ( dom G) = ( [#] I[01] ) by A50, TOPS_2:def 5;

        

         A56: ( rng G) = ( L~ (f | (n + 3))) by A54, PRE_TOPC:def 5;

        set pp = ((G " ) . (f /. (n + 2)));

        G is onto by A54, FUNCT_2:def 3;

        then

         A57: pp = ((G qua Function " ) . (f /. (n + 2))) by A53, TOPS_2:def 4;

        

         A58: (n + 2) <= ( len (f | (n + 2))) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

        

         A59: 1 <= ( len (f | (n + 2))) by A36, A42, A43, FINSEQ_1: 59, XXREAL_0: 2;

        

         A60: (n + 2) in ( dom (f | (n + 2))) by A42, A58, FINSEQ_3: 25;

        

         A61: 1 in ( dom (f | (n + 2))) by A59, FINSEQ_3: 25;

        

         A62: (f /. (n + 2)) in ( rng G) by A40, A46, A47, A56, GOBOARD1: 1, NAT_1: 11;

        then

         A63: pp in ( dom G) by A53, A57, FUNCT_1: 32;

        

         A64: (f /. (n + 2)) = (G . pp) by A53, A57, A62, FUNCT_1: 32;

        reconsider pp as Real;

        

         A65: ((n + 1) + 1) <> ((n + 2) + 1);

        

         A66: (n + 2) <> (n + 3);

        

         A67: (n + 2) in ( dom f) by A42, A45, FINSEQ_3: 25;

        

         A68: (n + 3) in ( dom f) by A35, A36, FINSEQ_3: 25;

        

         A69: 1 <> pp

        proof

          assume pp = 1;

          then (f /. (n + 2)) = (f /. ((n + 1) + 2)) by A52, A53, A57, A62, FUNCT_1: 32;

          hence thesis by A8, A66, A67, A68, PARTFUN2: 10;

        end;

        

         A70: 0 <= pp by A63, BORSUK_1: 43;

        pp <= 1 by A63, BORSUK_1: 43;

        then

         A71: pp < 1 by A69, XXREAL_0: 1;

        set pn = (f /. (n + 2)), pn1 = (f /. ((n + 2) + 1));

        

         A72: pn = ((f | (n + 2)) /. (n + 2)) by A60, FINSEQ_4: 70;

        

         A73: ((f | (n + 2)) /. 1) = (f /. 1) by A61, FINSEQ_4: 70;

        

         A74: ( len (f | (n + 2))) = (n + 2) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

        (f | (n + 2)) is being_S-Seq by A3, JORDAN3: 4, NAT_1: 11;

        then NE is_an_arc_of (((f | (n + 2)) /. 1),pn) by A38, A72, A74, TOPREAL1: 25;

        then

        consider F be Function of I[01] , (( TOP-REAL 2) | NE) such that

         A75: F is being_homeomorphism and

         A76: (F . 0 ) = (f /. 1) and

         A77: (F . 1) = pn by A73, TOPREAL1:def 1;

        

         A78: ((n + 1) + 1) in ( dom f) by A42, A44, FINSEQ_3: 25;

        ((n + 2) + 1) in ( dom f) by A35, A36, FINSEQ_3: 25;

        then ( LSeg (pn,pn1)) is_an_arc_of (pn,pn1) by A8, A65, A78, PARTFUN2: 10, TOPREAL1: 9;

        then

        consider F9 be Function of I[01] , (( TOP-REAL 2) | ( LSeg (pn,pn1))) such that

         A79: F9 is being_homeomorphism and

         A80: (F9 . 0 ) = pn and

         A81: (F9 . 1) = pn1 by TOPREAL1:def 1;

        set Ex1 = ( P[01] ( 0 ,(1 / 2),( (#) ( 0 ,1)),(( 0 ,1) (#) ))), Ex2 = ( P[01] ((1 / 2),1,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

        set F1 = (F * Ex1), F19 = (F9 * Ex2);

        

         A82: Ex1 is being_homeomorphism by TREAL_1: 17;

        

         A83: Ex2 is being_homeomorphism by TREAL_1: 17;

        

         A84: ( dom Ex1) = ( [#] ( Closed-Interval-TSpace ( 0 ,(1 / 2)))) by A82, TOPS_2:def 5;

        then

         A85: ( dom Ex1) = [. 0 , (1 / 2).] by TOPMETR: 18;

        ( dom F) = ( [#] I[01] ) by A75, TOPS_2:def 5;

        then

         A86: ( rng Ex1) = ( dom F) by A82, TOPMETR: 20, TOPS_2:def 5;

        then ( rng F1) = ( rng F) by RELAT_1: 28;

        then ( rng F1) = ( [#] (( TOP-REAL 2) | NE)) by A75, TOPS_2:def 5;

        then

         A87: ( rng F1) = Q(n) by A38, PRE_TOPC:def 5;

        ( dom F1) = the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by A84, A86, RELAT_1: 27;

        then

        reconsider F1 as Function of ( Closed-Interval-TSpace ( 0 ,(1 / 2))), (( TOP-REAL 2) | NE) by FUNCT_2:def 1;

        

         A88: F1 is being_homeomorphism by A75, A82, TOPMETR: 20, TOPS_2: 57;

        

        then

         A89: ( rng F1) = ( [#] (( TOP-REAL 2) | NE)) by TOPS_2:def 5

        .= Q(n) by A38, PRE_TOPC:def 5;

        

         A90: ( dom Ex2) = ( [#] ( Closed-Interval-TSpace ((1 / 2),1))) by A83, TOPS_2:def 5;

        ( dom F9) = ( [#] I[01] ) by A79, TOPS_2:def 5;

        then

         A91: ( rng Ex2) = ( dom F9) by A83, TOPMETR: 20, TOPS_2:def 5;

        then ( dom F19) = the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by A90, RELAT_1: 27;

        then

        reconsider F19 as Function of ( Closed-Interval-TSpace ((1 / 2),1)), (( TOP-REAL 2) | ( LSeg (pn,pn1))) by FUNCT_2:def 1;

        

         A92: F19 is being_homeomorphism by A79, A83, TOPMETR: 20, TOPS_2: 57;

        

        then

         A93: ( rng F19) = ( [#] (( TOP-REAL 2) | ( LSeg (pn,pn1)))) by TOPS_2:def 5

        .= ( LSeg (pn,pn1)) by PRE_TOPC:def 5;

        set FF = (F1 +* F19);

        reconsider T1 = ( Closed-Interval-TSpace ( 0 ,(1 / 2))), T2 = ( Closed-Interval-TSpace ((1 / 2),1)) as SubSpace of I[01] by TOPMETR: 20, TREAL_1: 3;

        

         A94: Q(+) = ( Q(n) \/ ( LSeg (pn,pn1))) by A67, A68, TOPREAL3: 38;

        

         A95: the carrier of (( TOP-REAL 2) | Q(+)) = ( [#] (( TOP-REAL 2) | Q(+)))

        .= Q(+) by PRE_TOPC:def 5;

        ( dom F1) = the carrier of T1 by A84, A86, RELAT_1: 27;

        then

        reconsider g11 = F1 as Function of T1, (( TOP-REAL 2) | NE1) by A87, A94, A95, RELSET_1: 4, XBOOLE_1: 7;

        ( dom F19) = the carrier of T2 by A90, A91, RELAT_1: 27;

        then

        reconsider g22 = F19 as Function of T2, (( TOP-REAL 2) | NE1) by A93, A94, A95, RELSET_1: 4, XBOOLE_1: 7;

        

         A96: [. 0 , (1 / 2).] = ( dom F1) by A10, A88, TOPS_2:def 5;

        

         A97: [.(1 / 2), 1.] = ( dom F19) by A11, A92, TOPS_2:def 5;

        

         A98: (1 / 2) in { l where l be Real : 0 <= l & l <= (1 / 2) };

        

         A99: (1 / 2) in { l where l be Real : (1 / 2) <= l & l <= 1 };

        

         A100: (1 / 2) in ( dom F1) by A96, A98, RCOMP_1:def 1;

        

         A101: (1 / 2) in ( dom F19) by A97, A99, RCOMP_1:def 1;

        

         A102: ( dom FF) = ( [. 0 , (1 / 2).] \/ [.(1 / 2), 1.]) by A96, A97, FUNCT_4:def 1

        .= [. 0 , 1.] by XXREAL_1: 174;

        

         A103: I[01] is compact by HEINE: 4, TOPMETR: 20;

        

         A104: (( TOP-REAL 2) | NE1) is T_2 by TOPMETR: 2;

        

         A105: (Ex1 . (1 / 2)) = (Ex1 . (( 0 ,(1 / 2)) (#) )) by TREAL_1:def 2

        .= (( 0 ,1) (#) ) by TREAL_1: 13

        .= 1 by TREAL_1:def 2;

        

         A106: (Ex2 . (1 / 2)) = (Ex2 . ( (#) ((1 / 2),1))) by TREAL_1:def 1

        .= ( (#) ( 0 ,1)) by TREAL_1: 13

        .= 0 by TREAL_1:def 1;

        

         A107: (F1 . (1 / 2)) = (f /. (n + 2)) by A77, A100, A105, FUNCT_1: 12;

        

         A108: (F19 . (1 / 2)) = (f /. (n + 2)) by A80, A101, A106, FUNCT_1: 12;

        

         A109: ( [. 0 , (1 / 2).] /\ [.(1 / 2), 1.]) = [.(1 / 2), (1 / 2).] by XXREAL_1: 143;

        then

         A110: (( dom F1) /\ ( dom F19)) = {(1 / 2)} by A96, A97, XXREAL_1: 17;

        

         A111: for x be set holds x in ( Q(n) /\ ( LSeg (pn,pn1))) iff x = pn

        proof

          let x be set;

          thus x in ( Q(n) /\ ( LSeg (pn,pn1))) implies x = pn

          proof

            assume

             A112: x in ( Q(n) /\ ( LSeg (pn,pn1)));

            then

             A113: x in ( LSeg (pn,pn1)) by XBOOLE_0:def 4;

            x in Q(n) by A112, XBOOLE_0:def 4;

            then x in ( union { ( LSeg ((f | (n + 2)),k)) where k be Nat : 1 <= k & (k + 1) <= ( len (f | (n + 2))) }) by TOPREAL1:def 4;

            then

            consider X be set such that

             A114: x in X and

             A115: X in { ( LSeg ((f | (n + 2)),k)) where k be Nat : 1 <= k & (k + 1) <= ( len (f | (n + 2))) } by TARSKI:def 4;

            consider k be Nat such that

             A116: X = ( LSeg ((f | (n + 2)),k)) and

             A117: 1 <= k and

             A118: (k + 1) <= ( len (f | (n + 2))) by A115;

            

             A119: ( len (f | (n + 2))) = (n + (1 + 1)) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

            

             A120: ( len (f | (n + 2))) = ((n + 1) + 1) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

            then

             A121: k <= (n + 1) by A118, XREAL_1: 6;

            

             A122: f is s.n.c. by A3;

            

             A123: f is unfolded by A3;

            now

              assume

               A124: k < (n + 1);

              

               A125: 1 <= (1 + k) by NAT_1: 11;

              

               A126: (k + 1) <= ( len f) by A44, A118, A120, XXREAL_0: 2;

              

               A127: (k + 1) < ((n + 1) + 1) by A124, XREAL_1: 6;

              set p19 = (f /. k), p29 = (f /. (k + 1));

              (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

              then k <= (n + 2) by A124, XXREAL_0: 2;

              then

               A128: k in ( Seg ( len (f | (n + 2)))) by A117, A119, FINSEQ_1: 1;

              

               A129: (k + 1) in ( Seg ( len (f | (n + 2)))) by A118, A125, FINSEQ_1: 1;

              

               A130: k in ( dom (f | (n + 2))) by A128, FINSEQ_1:def 3;

              

               A131: (k + 1) in ( dom (f | (n + 2))) by A129, FINSEQ_1:def 3;

              

               A132: ((f | (n + 2)) /. k) = p19 by A130, FINSEQ_4: 70;

              

               A133: ((f | (n + 2)) /. (k + 1)) = p29 by A131, FINSEQ_4: 70;

              

               A134: ( LSeg (f,k)) = ( LSeg (p19,p29)) by A117, A126, TOPREAL1:def 3

              .= ( LSeg ((f | (n + 2)),k)) by A117, A118, A132, A133, TOPREAL1:def 3;

              ( LSeg (f,(n + 2))) = ( LSeg (pn,pn1)) by A36, A42, TOPREAL1:def 3;

              then ( LSeg ((f | (n + 2)),k)) misses ( LSeg (pn,pn1)) by A122, A127, A134, TOPREAL1:def 7;

              then (( LSeg ((f | (n + 2)),k)) /\ ( LSeg (pn,pn1))) = {} ;

              hence contradiction by A113, A114, A116, XBOOLE_0:def 4;

            end;

            then

             A135: k = (n + 1) by A121, XXREAL_0: 1;

            

             A136: 1 <= (n + 1) by A117, A121, XXREAL_0: 2;

            

             A137: ((n + 1) + 1) <= ( len f) by A36, A43, XXREAL_0: 2;

            set p19 = (f /. (n + 1)), p29 = (f /. ((n + 1) + 1));

            

             A138: (n + 1) <= ((n + 1) + 1) by NAT_1: 11;

            

             A139: 1 <= (1 + n) by NAT_1: 11;

            

             A140: 1 <= (1 + (n + 1)) by NAT_1: 11;

            

             A141: (n + 1) in ( Seg ( len (f | (n + 2)))) by A119, A138, A139, FINSEQ_1: 1;

            

             A142: ((n + 1) + 1) in ( Seg ( len (f | (n + 2)))) by A119, A140, FINSEQ_1: 1;

            

             A143: (n + 1) in ( dom (f | (n + 2))) by A141, FINSEQ_1:def 3;

            

             A144: ((n + 1) + 1) in ( dom (f | (n + 2))) by A142, FINSEQ_1:def 3;

            

             A145: ((f | (n + 2)) /. (n + 1)) = p19 by A143, FINSEQ_4: 70;

            

             A146: ((f | (n + 2)) /. ((n + 1) + 1)) = p29 by A144, FINSEQ_4: 70;

            

             A147: ( LSeg (f,(n + 1))) = ( LSeg (p19,p29)) by A136, A137, TOPREAL1:def 3

            .= ( LSeg ((f | (n + 2)),(n + 1))) by A119, A139, A145, A146, TOPREAL1:def 3;

            ( LSeg (pn,pn1)) = ( LSeg (f,((n + 1) + 1))) by A36, A42, TOPREAL1:def 3;

            then

             A148: x in (( LSeg (f,(n + 1))) /\ ( LSeg (f,((n + 1) + 1)))) by A113, A114, A116, A135, A147, XBOOLE_0:def 4;

            1 <= (n + 1) by NAT_1: 11;

            then (( LSeg (f,(n + 1))) /\ ( LSeg (f,((n + 1) + 1)))) = {(f /. ((n + 1) + 1))} by A36, A123, TOPREAL1:def 6;

            hence thesis by A148, TARSKI:def 1;

          end;

          assume

           A149: x = pn;

          then

           A150: x in ( LSeg (pn,pn1)) by RLTOPSP1: 68;

          

           A151: ( len (f | (n + 2))) = (n + 2) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

          then

           A152: ( dom (f | (n + 2))) = ( Seg (n + 2)) by FINSEQ_1:def 3;

          (n + 2) in ( Seg (n + 2)) by A42, FINSEQ_1: 1;

          then

           A153: x = ((f | (n + 2)) /. ((n + 1) + 1)) by A149, A152, FINSEQ_4: 70;

          1 <= (n + 1) by NAT_1: 11;

          then

           A154: x in ( LSeg ((f | (n + 2)),(n + 1))) by A151, A153, TOPREAL1: 21;

          

           A155: 1 <= (n + 1) by NAT_1: 11;

          ((n + 1) + 1) <= ( len (f | (n + 2))) by A36, A43, FINSEQ_1: 59, XXREAL_0: 2;

          then ( LSeg ((f | (n + 2)),(n + 1))) in { ( LSeg ((f | (n + 2)),k)) where k be Nat : 1 <= k & (k + 1) <= ( len (f | (n + 2))) } by A155;

          then x in ( union { ( LSeg ((f | (n + 2)),k)) where k be Nat : 1 <= k & (k + 1) <= ( len (f | (n + 2))) }) by A154, TARSKI:def 4;

          then x in Q(n) by TOPREAL1:def 4;

          hence thesis by A150, XBOOLE_0:def 4;

        end;

        (f /. (n + 2)) in ( rng F19) by A101, A108, FUNCT_1:def 3;

        then

         A156: {(f /. (n + 2))} c= ( rng F19) by ZFMISC_1: 31;

        

         A157: (F1 .: (( dom F1) /\ ( dom F19))) = ( Im (F1,(1 / 2))) by A96, A97, A109, XXREAL_1: 17

        .= {(f /. (n + 2))} by A100, A107, FUNCT_1: 59;

        then

         A158: ( rng FF) = ( Q(n) \/ ( LSeg (pn,pn1))) by A89, A93, A156, TOPMETR2: 2;

        then

         A159: ( rng FF) = ( [#] (( TOP-REAL 2) | Q(+))) by A67, A68, A95, TOPREAL3: 38;

        ( rng FF) c= the carrier of (( TOP-REAL 2) | Q(+)) by A89, A93, A94, A95, A156, A157, TOPMETR2: 2;

        then

        reconsider FF as Function of I[01] , (( TOP-REAL 2) | NE1) by A102, BORSUK_1: 40, FUNCT_2: 2;

        

         A160: ( rng Ex1) = ( [#] ( Closed-Interval-TSpace ( 0 ,1))) by A82, TOPS_2:def 5;

        

         A161: 0 in { l where l be Real : 0 <= l & l <= (1 / 2) };

        

         A162: (1 / 2) in { l where l be Real : 0 <= l & l <= (1 / 2) };

        

         A163: 0 in ( dom Ex1) by A85, A161, RCOMP_1:def 1;

        

         A164: (1 / 2) in ( dom Ex1) by A85, A162, RCOMP_1:def 1;

        

         A165: Ex1 is one-to-one continuous by A82, TOPS_2:def 5;

        

         A166: (Ex1 . 0 ) = (Ex1 . ( (#) ( 0 ,(1 / 2)))) by TREAL_1:def 1

        .= ( (#) ( 0 ,1)) by TREAL_1: 13

        .= 0 by TREAL_1:def 1;

        

         A167: Ex1 is onto by A160, FUNCT_2:def 3;

        

        then

         A168: ((Ex1 " ) . 0 ) = ((Ex1 qua Function " ) . 0 ) by A165, TOPS_2:def 4

        .= 0 by A163, A165, A166, FUNCT_1: 32;

        

         A169: (Ex2 . (1 / 2)) = (Ex2 . ( (#) ((1 / 2),1))) by TREAL_1:def 1

        .= ( (#) ( 0 ,1)) by TREAL_1: 13

        .= 0 by TREAL_1:def 1;

        

         A170: ((Ex1 " ) . 1) = ((Ex1 qua Function " ) . 1) by A167, A165, TOPS_2:def 4

        .= (1 / 2) by A105, A164, A165, FUNCT_1: 32;

        

         A171: (Ex2 . 1) = (Ex2 . (((1 / 2),1) (#) )) by TREAL_1:def 2

        .= (( 0 ,1) (#) ) by TREAL_1: 13

        .= 1 by TREAL_1:def 2;

        

         A172: ( LSeg (pn,pn1)) = (F19 .: [.(1 / 2), 1.]) by A9, A93, RELSET_1: 22;

        

         A173: (FF . (1 / 2)) = (f /. (n + 2)) by A101, A108, FUNCT_4: 13;

        

         A174: for x be set st x in [. 0 , (1 / 2).] & x <> (1 / 2) holds not x in ( dom F19)

        proof

          let x be set;

          assume that

           A175: x in [. 0 , (1 / 2).] and

           A176: x <> (1 / 2);

          assume x in ( dom F19);

          then x in (( dom F1) /\ ( dom F19)) by A96, A175, XBOOLE_0:def 4;

          hence thesis by A110, A176, TARSKI:def 1;

        end;

        

         A177: (FF .: [.(1 / 2), 1.]) c= (F19 .: [.(1 / 2), 1.])

        proof

          let a be object;

          assume a in (FF .: [.(1 / 2), 1.]);

          then

          consider x be object such that x in ( dom FF) and

           A178: x in [.(1 / 2), 1.] and

           A179: a = (FF . x) by FUNCT_1:def 6;

          (FF . x) = (F19 . x) by A97, A178, FUNCT_4: 13;

          hence thesis by A97, A178, A179, FUNCT_1:def 6;

        end;

        (F19 .: [.(1 / 2), 1.]) c= (FF .: [.(1 / 2), 1.])

        proof

          let a be object;

          assume a in (F19 .: [.(1 / 2), 1.]);

          then

          consider x be object such that

           A180: x in ( dom F19) and

           A181: x in [.(1 / 2), 1.] and

           A182: a = (F19 . x) by FUNCT_1:def 6;

          

           A183: x in ( dom FF) by A180, FUNCT_4: 12;

          a = (FF . x) by A180, A182, FUNCT_4: 13;

          hence thesis by A181, A183, FUNCT_1:def 6;

        end;

        then

         A184: (FF .: [.(1 / 2), 1.]) = (F19 .: [.(1 / 2), 1.]) by A177;

        set GF = ((G " ) * FF);

        

         A185: 0 in ( dom FF) by A102, BORSUK_1: 40, BORSUK_1: 43;

        

         A186: 1 in ( dom FF) by A102, BORSUK_1: 40, BORSUK_1: 43;

         0 in { l where l be Real : 0 <= l & l <= (1 / 2) };

        then 0 in [. 0 , (1 / 2).] by RCOMP_1:def 1;

        

        then

         A187: (FF . 0 ) = (F1 . 0 ) by A174, FUNCT_4: 11

        .= (f /. 1) by A76, A163, A166, FUNCT_1: 13;

        1 in { l where l be Real : (1 / 2) <= l & l <= 1 };

        then

         A188: 1 in ( dom F19) by A97, RCOMP_1:def 1;

        

        then

         A189: (FF . 1) = (F19 . 1) by FUNCT_4: 13

        .= pn1 by A81, A171, A188, FUNCT_1: 12;

        

         A190: 0 in ( dom G) by A55, BORSUK_1: 43;

        

         A191: G is onto by A54, FUNCT_2:def 3;

        

        then

         A192: ((G " ) . (f /. 1)) = ((G qua Function " ) . (f /. 1)) by A53, TOPS_2:def 4

        .= 0 by A51, A53, A190, FUNCT_1: 32;

        then

         A193: (GF . 0 ) = 0 by A185, A187, FUNCT_1: 13;

        

         A194: 1 in ( dom G) by A55, BORSUK_1: 43;

        

         A195: ((G " ) . pn1) = ((G qua Function " ) . pn1) by A191, A53, TOPS_2:def 4

        .= 1 by A52, A53, A194, FUNCT_1: 32;

        then

         A196: (GF . 1) = 1 by A186, A189, FUNCT_1: 13;

        reconsider ppp = (1 / 2) as Point of I[01] by BORSUK_1: 43;

        ( TopSpaceMetr RealSpace ) is T_2 by PCOMPS_1: 34;

        then

         A197: I[01] is T_2 by TOPMETR: 2, TOPMETR: 20, TOPMETR:def 6;

        

         A198: T1 is compact by HEINE: 4;

        

         A199: T2 is compact by HEINE: 4;

        

         A200: F1 is continuous by A88, TOPS_2:def 5;

        

         A201: F19 is continuous by A92, TOPS_2:def 5;

        

         A202: (( TOP-REAL 2) | NE) is SubSpace of (( TOP-REAL 2) | NE1) by A38, A94, TOPMETR: 4;

        

         A203: (( TOP-REAL 2) | ( LSeg (pn,pn1))) is SubSpace of (( TOP-REAL 2) | NE1) by A94, TOPMETR: 4;

        

         A204: g11 is continuous by A200, A202, PRE_TOPC: 26;

        

         A205: g22 is continuous by A201, A203, PRE_TOPC: 26;

        

         A206: ( [#] T1) = [. 0 , (1 / 2).] by TOPMETR: 18;

        

         A207: ( [#] T2) = [.(1 / 2), 1.] by TOPMETR: 18;

        then

         A208: (( [#] T1) \/ ( [#] T2)) = ( [#] I[01] ) by A206, BORSUK_1: 40, XXREAL_1: 174;

        (( [#] T1) /\ ( [#] T2)) = {ppp} by A206, A207, XXREAL_1: 418;

        then

        reconsider FF as continuous Function of I[01] , (( TOP-REAL 2) | NE1) by A107, A108, A197, A198, A199, A204, A205, A208, COMPTS_1: 20;

        

         A209: F1 is one-to-one by A88, TOPS_2:def 5;

        

         A210: F19 is one-to-one by A92, TOPS_2:def 5;

        for x1,x2 be set st x1 in ( dom F19) & x2 in (( dom F1) \ ( dom F19)) holds (F19 . x1) <> (F1 . x2)

        proof

          let x1,x2 be set;

          assume that

           A211: x1 in ( dom F19) and

           A212: x2 in (( dom F1) \ ( dom F19));

          assume

           A213: (F19 . x1) = (F1 . x2);

          

           A214: (F19 . x1) in ( LSeg (pn,pn1)) by A93, A211, FUNCT_2: 4;

          

           A215: x2 in ( dom F1) by A212, XBOOLE_0:def 5;

          

           A216: not x2 in ( dom F19) by A212, XBOOLE_0:def 5;

          (F1 . x2) in NE by A38, A89, A212, FUNCT_2: 4;

          then (F1 . x2) in (NE /\ ( LSeg (pn,pn1))) by A213, A214, XBOOLE_0:def 4;

          then (F1 . x2) = pn by A38, A111;

          hence thesis by A100, A101, A107, A209, A215, A216, FUNCT_1:def 4;

        end;

        then

         A217: FF is one-to-one by A209, A210, TOPMETR2: 1;

        

         A218: (G " ) is being_homeomorphism by A50, TOPS_2: 56;

        FF is being_homeomorphism by A103, A104, A159, A217, COMPTS_1: 17;

        then

         A219: GF is being_homeomorphism by A218, TOPS_2: 57;

        then

         A220: GF is continuous by TOPS_2:def 5;

        

         A221: ( dom GF) = ( [#] I[01] ) by A219, TOPS_2:def 5;

        

         A222: ( rng GF) = ( [#] I[01] ) by A219, TOPS_2:def 5;

        

         A223: GF is one-to-one by A219, TOPS_2:def 5;

        then

         A224: ( dom (GF " )) = ( [#] I[01] ) by A222, TOPS_2: 49;

        

         A225: ( rng G) = ( [#] (( TOP-REAL 2) | Q(+))) by A50, TOPS_2:def 5

        .= ( rng FF) by A67, A68, A95, A158, TOPREAL3: 38;

        

         A226: (G * ((G " ) * FF)) = (FF qua Relation * (G * (G " ) qua Function)) by RELAT_1: 36

        .= (( id ( rng G)) * FF) by A53, A54, TOPS_2: 52

        .= FF by A225, RELAT_1: 54;

        

         A227: (1 / 2) in ( dom GF) by A221, BORSUK_1: 43;

        then

         A228: (GF . (1 / 2)) in ( rng GF) by FUNCT_1:def 3;

        

         A229: (GF . (1 / 2)) = ((G " ) . (FF . (1 / 2))) by A227, FUNCT_1: 12

        .= pp by A101, A108, FUNCT_4: 13;

        

         A230: [.pp, 1.] c= (GF .: [.(1 / 2), 1.])

        proof

          let a be object;

          assume a in [.pp, 1.];

          then a in { l where l be Real : pp <= l & l <= 1 } by RCOMP_1:def 1;

          then

          consider l1 be Real such that

           A231: l1 = a and

           A232: pp <= l1 and

           A233: l1 <= 1;

          

           A234: 0 <= pp by A228, A229, BORSUK_1: 43;

          set cos = ((GF " ) . l1);

          l1 in ( dom (GF " )) by A224, A232, A233, A234, BORSUK_1: 43;

          then

           A235: cos in ( rng (GF " )) by FUNCT_1:def 3;

          

           A236: l1 in ( rng GF) by A222, A232, A233, A234, BORSUK_1: 43;

          GF is onto by A222, FUNCT_2:def 3;

          

          then

           A237: (GF . cos) = (GF . ((GF qua Function " ) . l1)) by A223, TOPS_2:def 4

          .= l1 by A223, A236, FUNCT_1: 35;

          reconsider cos as Real;

          reconsider A3 = cos, A4 = 1, A5 = (1 / 2) as Point of I[01] by A235, BORSUK_1: 43;

          reconsider A1 = (GF . A3), A2 = (GF . A4) as Point of I[01] ;

          reconsider Fhc = A1, Fh0 = A2, Fh12 = (GF . A5) as Real;

          

           A238: cos <= 1

          proof

            assume cos > 1;

            then Fhc > Fh0 by A193, A196, A220, A223, JORDAN5A: 16;

            hence thesis by A102, A189, A195, A233, A237, BORSUK_1: 40, FUNCT_1: 13;

          end;

          cos >= (1 / 2)

          proof

            assume cos < (1 / 2);

            then Fhc < Fh12 by A193, A196, A220, A223, JORDAN5A: 16;

            hence thesis by A102, A173, A232, A237, BORSUK_1: 40, FUNCT_1: 13;

          end;

          then cos in { l where l be Real : (1 / 2) <= l & l <= 1 } by A238;

          then cos in [.(1 / 2), 1.] by RCOMP_1:def 1;

          hence thesis by A221, A231, A235, A237, FUNCT_1:def 6;

        end;

        (GF .: [.(1 / 2), 1.]) c= [.pp, 1.]

        proof

          let a be object;

          assume a in (GF .: [.(1 / 2), 1.]);

          then

          consider x be object such that x in ( dom GF) and

           A239: x in [.(1 / 2), 1.] and

           A240: a = (GF . x) by FUNCT_1:def 6;

          x in { l where l be Real : (1 / 2) <= l & l <= 1 } by A239, RCOMP_1:def 1;

          then

          consider l1 be Real such that

           A241: l1 = x and

           A242: (1 / 2) <= l1 and

           A243: l1 <= 1;

          reconsider ll = l1, pol = (1 / 2) as Point of I[01] by A242, A243, BORSUK_1: 43;

          reconsider A1 = (GF . 1[01] ), A2 = (GF . ll), A3 = (GF . pol) as Point of I[01] ;

          reconsider A4 = A1, A5 = A2, A6 = A3 as Real;

          

           A244: A4 >= A5

          proof

            per cases ;

              suppose 1 <> l1;

              then 1 > l1 by A243, XXREAL_0: 1;

              hence thesis by A193, A196, A220, A223, BORSUK_1:def 15, JORDAN5A: 16;

            end;

              suppose 1 = l1;

              hence thesis by BORSUK_1:def 15;

            end;

          end;

          A5 >= A6

          proof

            per cases ;

              suppose l1 <> (1 / 2);

              then l1 > (1 / 2) by A242, XXREAL_0: 1;

              hence thesis by A193, A196, A220, A223, JORDAN5A: 16;

            end;

              suppose l1 = (1 / 2);

              hence thesis;

            end;

          end;

          then A5 in { l where l be Real : pp <= l & l <= 1 } by A196, A229, A244, BORSUK_1:def 15;

          hence thesis by A240, A241, RCOMP_1:def 1;

        end;

        then [.pp, 1.] = (GF .: [.(1 / 2), 1.]) by A230;

        then

         A245: (G .: [.pp, 1.]) = ( LSeg (pn,pn1)) by A172, A184, A226, RELAT_1: 126;

        ex p1,p2 be Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & ( LSeg (f,j)) = (G .: [.p1, p2.]) & (G . p1) = (f /. j) & (G . p2) = (f /. (j + 1))

        proof

          per cases ;

            suppose (j + 1) <= (n + 2);

            then

            consider r1,r2 be Real such that

             A246: r1 < r2 and

             A247: 0 <= r1 and

             A248: r1 <= 1 and 0 <= r2 and

             A249: r2 <= 1 and

             A250: ( LSeg (f,j)) = (F .: [.r1, r2.]) and

             A251: (F . r1) = (f /. j) and

             A252: (F . r2) = (f /. (j + 1)) by A39, A48, A75, A76, A77;

            set f1 = ((Ex1 " ) . r1), f2 = ((Ex1 " ) . r2);

            

             A253: Ex1 is continuous one-to-one by A82, TOPS_2:def 5;

            

             A254: ( dom Ex1) = ( [#] ( Closed-Interval-TSpace ( 0 ,(1 / 2)))) by A82, TOPS_2:def 5;

            

             A255: ( rng Ex1) = ( [#] ( Closed-Interval-TSpace ( 0 ,1))) by A82, TOPS_2:def 5;

            then

             A256: Ex1 is onto by FUNCT_2:def 3;

            then

             A257: f1 = ((Ex1 qua Function " ) . r1) by A253, TOPS_2:def 4;

            

             A258: f2 = ((Ex1 qua Function " ) . r2) by A253, A256, TOPS_2:def 4;

            

             A259: ( rng Ex1) = ( [#] I[01] ) by A82, TOPMETR: 20, TOPS_2:def 5

            .= the carrier of I[01] ;

            then

             A260: r1 in ( rng Ex1) by A247, A248, BORSUK_1: 43;

            

             A261: r2 in ( rng Ex1) by A246, A247, A249, A259, BORSUK_1: 43;

            

             A262: f1 in the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by A253, A254, A257, A260, FUNCT_1: 32;

            

             A263: f2 in the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by A253, A254, A258, A261, FUNCT_1: 32;

            

             A264: f1 in [. 0 , (1 / 2).] by A262, TOPMETR: 18;

            

             A265: f2 in [. 0 , (1 / 2).] by A263, TOPMETR: 18;

            reconsider f1, f2 as Real;

            reconsider r19 = r1, r29 = r2 as Point of ( Closed-Interval-TSpace ( 0 ,1)) by A246, A247, A248, A249, BORSUK_1: 43, TOPMETR: 20;

            

             A266: (Ex1 " ) is being_homeomorphism by A82, TOPS_2: 56;

            

             A267: f1 = ((Ex1 " ) . r19);

            

             A268: f2 = ((Ex1 " ) . r29);

            

             A269: (Ex1 " ) is continuous one-to-one by A266, TOPS_2:def 5;

            then

             A270: f1 < f2 by A168, A170, A246, A267, A268, JORDAN5A: 15;

            

             A271: [. 0 , (1 / 2).] c= [. 0 , 1.] by XXREAL_1: 34;

            

             A272: r1 = (Ex1 . f1) by A253, A257, A260, FUNCT_1: 32;

            

             A273: r2 = (Ex1 . f2) by A253, A258, A261, FUNCT_1: 32;

            

             A274: f1 in { l where l be Real : 0 <= l & l <= (1 / 2) } by A264, RCOMP_1:def 1;

            

             A275: f2 in { l where l be Real : 0 <= l & l <= (1 / 2) } by A265, RCOMP_1:def 1;

            

             A276: ex ff1 be Real st (ff1 = f1) & ( 0 <= ff1) & (ff1 <= (1 / 2)) by A274;

            ex ff2 be Real st (ff2 = f2) & ( 0 <= ff2) & (ff2 <= (1 / 2)) by A275;

            then

             A277: (Ex1 .: [.f1, f2.]) = [.r1, r2.] by A82, A105, A166, A270, A272, A273, A276, JORDAN5A: 20;

            

             A278: (F1 .: [.f1, f2.]) c= (FF .: [.f1, f2.])

            proof

              let a be object;

              assume a in (F1 .: [.f1, f2.]);

              then

              consider x be object such that

               A279: x in ( dom F1) and

               A280: x in [.f1, f2.] and

               A281: a = (F1 . x) by FUNCT_1:def 6;

               A282:

              now

                per cases ;

                  suppose x <> (1 / 2);

                  hence (FF . x) = (F1 . x) by A10, A174, A279, FUNCT_4: 11;

                end;

                  suppose x = (1 / 2);

                  hence (FF . x) = (F1 . x) by A101, A107, A108, FUNCT_4: 13;

                end;

              end;

              x in ( dom FF) by A279, FUNCT_4: 12;

              hence thesis by A280, A281, A282, FUNCT_1:def 6;

            end;

            (FF .: [.f1, f2.]) c= (F1 .: [.f1, f2.])

            proof

              let a be object;

              assume a in (FF .: [.f1, f2.]);

              then

              consider x be object such that x in ( dom FF) and

               A283: x in [.f1, f2.] and

               A284: a = (FF . x) by FUNCT_1:def 6;

              

               A285: [.f1, f2.] c= [. 0 , (1 / 2).] by A264, A265, XXREAL_2:def 12;

              now

                per cases ;

                  suppose x <> (1 / 2);

                  hence (FF . x) = (F1 . x) by A174, A283, A285, FUNCT_4: 11;

                end;

                  suppose x = (1 / 2);

                  hence (FF . x) = (F1 . x) by A101, A107, A108, FUNCT_4: 13;

                end;

              end;

              hence thesis by A96, A283, A284, A285, FUNCT_1:def 6;

            end;

            then (F1 .: [.f1, f2.]) = (FF .: [.f1, f2.]) by A278;

            then

             A286: (F .: [.r1, r2.]) = (FF .: [.f1, f2.]) by A277, RELAT_1: 126;

            set e1 = (GF . f1), e2 = (GF . f2);

            

             A287: e1 in the carrier of I[01] by A264, A271, BORSUK_1: 40, FUNCT_2: 5;

            

             A288: e2 in the carrier of I[01] by A265, A271, BORSUK_1: 40, FUNCT_2: 5;

            

             A289: e1 in { l where l be Real : 0 <= l & l <= 1 } by A287, BORSUK_1: 40, RCOMP_1:def 1;

            

             A290: e2 in { l where l be Real : 0 <= l & l <= 1 } by A288, BORSUK_1: 40, RCOMP_1:def 1;

            consider l1 be Real such that

             A291: l1 = e1 and

             A292: 0 <= l1 and

             A293: l1 <= 1 by A289;

            consider l2 be Real such that

             A294: l2 = e2 and 0 <= l2 and

             A295: l2 <= 1 by A290;

            reconsider f19 = f1, f29 = f2 as Point of I[01] by A264, A265, A271, BORSUK_1: 40;

            

             A296: (GF . 0 ) = 0 by A185, A187, A192, FUNCT_1: 13;

            

             A297: (GF . 1) = 1 by A186, A189, A195, FUNCT_1: 13;

            

             A298: l1 = (GF . f19) by A291;

            l2 = (GF . f29) by A294;

            then

             A299: l1 < l2 by A220, A223, A270, A296, A297, A298, JORDAN5A: 16;

            

             A300: f1 < f2 by A168, A170, A246, A267, A268, A269, JORDAN5A: 15;

            

             A301: 0 <= f1 by A264, A271, BORSUK_1: 40, BORSUK_1: 43;

            f2 <= 1 by A265, A271, BORSUK_1: 40, BORSUK_1: 43;

            

            then

             A302: (G .: [.l1, l2.]) = (G .: (GF .: [.f1, f2.])) by A193, A196, A219, A291, A294, A300, A301, JORDAN5A: 20, TOPMETR: 20

            .= (FF .: [.f1, f2.]) by A226, RELAT_1: 126;

            

             A303: (FF . f19) = (F . r19)

            proof

              per cases ;

                suppose

                 A304: f19 = (1 / 2);

                

                then (FF . f19) = (F19 . (1 / 2)) by A101, FUNCT_4: 13

                .= (F9 . 0 ) by A101, A169, FUNCT_1: 12

                .= (F . r19) by A77, A80, A105, A253, A255, A257, A304, FUNCT_1: 32;

                hence thesis;

              end;

                suppose f19 <> (1 / 2);

                

                then (FF . f19) = (F1 . f19) by A174, A264, FUNCT_4: 11

                .= (F . (Ex1 . f19)) by A85, A264, FUNCT_1: 13

                .= (F . r19) by A253, A255, A257, FUNCT_1: 32;

                hence thesis;

              end;

            end;

            

             A305: (FF . f29) = (F . r29)

            proof

              per cases ;

                suppose

                 A306: f29 = (1 / 2);

                

                then (FF . f29) = (F19 . (1 / 2)) by A101, FUNCT_4: 13

                .= (F9 . 0 ) by A101, A169, FUNCT_1: 12

                .= (F . r29) by A77, A80, A105, A253, A255, A258, A306, FUNCT_1: 32;

                hence thesis;

              end;

                suppose f29 <> (1 / 2);

                

                then (FF . f29) = (F1 . f29) by A174, A265, FUNCT_4: 11

                .= (F . (Ex1 . f29)) by A85, A265, FUNCT_1: 13

                .= (F . r29) by A253, A255, A258, FUNCT_1: 32;

                hence thesis;

              end;

            end;

            

             A307: (G . l1) = (f /. j) by A102, A226, A251, A291, A303, BORSUK_1: 40, FUNCT_1: 12;

            (G . l2) = (f /. (j + 1)) by A102, A226, A252, A294, A305, BORSUK_1: 40, FUNCT_1: 12;

            hence thesis by A250, A286, A292, A293, A295, A299, A302, A307;

          end;

            suppose (j + 1) > (n + 2);

            then

             A308: (j + 1) = (n + 3) by A41, A49, NAT_1: 9;

            then ( LSeg (f,j)) = ( LSeg (pn,pn1)) by A36, A42, TOPREAL1:def 3;

            hence thesis by A52, A64, A70, A71, A245, A308;

          end;

        end;

        hence thesis;

      end;

      

       A309: for n be Nat holds ARC[n] from NAT_1:sch 2( A14, A33);

      1 <= (h1 + 2) by A12, XXREAL_0: 2;

      then ex NE be non empty Subset of ( TOP-REAL 2) st (NE = Q(h1)) & (for j be Nat holds for F be Function of I[01] , (( TOP-REAL 2) | NE) st 1 <= j & (j + 1) <= (h1 + 2) & F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. (h1 + 2)) holds ex p1,p2 be Real st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & ( LSeg (f,j)) = (F .: [.p1, p2.]) & (F . p1) = (f /. j) & (F . p2) = (f /. (j + 1))) by A309;

      hence thesis by A1, A2, A4, A5, A6, A7, A13;

    end;

    theorem :: JORDAN5B:8

    for f be FinSequence of ( TOP-REAL 2), Q,R be non empty Subset of ( TOP-REAL 2), F be Function of I[01] , (( TOP-REAL 2) | Q), i be Nat, P be non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & (F . 0 ) = (f /. 1) & (F . 1) = (f /. ( len f)) & 1 <= i & (i + 1) <= ( len f) & (F .: P) = ( LSeg (f,i)) & Q = ( L~ f) & R = ( LSeg (f,i)) holds ex G be Function of ( I[01] | P), (( TOP-REAL 2) | R) st G = (F | P) & G is being_homeomorphism

    proof

      let f be FinSequence of ( TOP-REAL 2), Q,R be non empty Subset of ( TOP-REAL 2), F be Function of I[01] , (( TOP-REAL 2) | Q), i be Nat, P be non empty Subset of I[01] ;

      assume that

       A1: f is being_S-Seq and

       A2: F is being_homeomorphism and

       A3: (F . 0 ) = (f /. 1) and

       A4: (F . 1) = (f /. ( len f)) and

       A5: 1 <= i and

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

       A7: (F .: P) = ( LSeg (f,i)) and

       A8: Q = ( L~ f) and

       A9: R = ( LSeg (f,i));

      consider ppi,pi1 be Real such that

       A10: ppi < pi1 and

       A11: 0 <= ppi and ppi <= 1 and 0 <= pi1 and

       A12: pi1 <= 1 and

       A13: ( LSeg (f,i)) = (F .: [.ppi, pi1.]) and (F . ppi) = (f /. i) and (F . pi1) = (f /. (i + 1)) by A1, A2, A3, A4, A5, A6, A8, Th7;

      ppi in { dd where dd be Real : ppi <= dd & dd <= pi1 } by A10;

      then

      reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01] by A11, A12, BORSUK_1: 40, RCOMP_1:def 1, XXREAL_1: 34;

      

       A14: the carrier of ( I[01] | Poz) = ( [#] ( I[01] | Poz))

      .= Poz by PRE_TOPC:def 5;

      

       A15: ( dom F) = ( [#] I[01] ) by A2, TOPS_2:def 5

      .= [. 0 , 1.] by BORSUK_1: 40;

      

       A16: F is one-to-one by A2, TOPS_2:def 5;

      then

       A17: P c= Poz by A7, A13, A15, BORSUK_1: 40, FUNCT_1: 87;

      Poz c= P by A7, A13, A15, A16, BORSUK_1: 40, FUNCT_1: 87;

      then

       A18: P = Poz by A17;

      set gg = (F | P);

      reconsider gg as Function of ( I[01] | Poz), (( TOP-REAL 2) | Q) by A14, A18, FUNCT_2: 32;

      reconsider SEG = ( LSeg (f,i)) as non empty Subset of (( TOP-REAL 2) | Q) by A7, A9;

      

       A19: the carrier of ((( TOP-REAL 2) | Q) | SEG) = ( [#] ((( TOP-REAL 2) | Q) | SEG))

      .= SEG by PRE_TOPC:def 5;

      

       A20: ( rng gg) c= SEG

      proof

        let ii be object;

        assume ii in ( rng gg);

        then

        consider j be object such that

         A21: j in ( dom gg) and

         A22: ii = (gg . j) by FUNCT_1:def 3;

        j in (( dom F) /\ Poz) by A18, A21, RELAT_1: 61;

        then j in ( dom F) by XBOOLE_0:def 4;

        then (F . j) in ( LSeg (f,i)) by A13, A14, A21, FUNCT_1:def 6;

        hence thesis by A14, A18, A21, A22, FUNCT_1: 49;

      end;

      reconsider SEG as non empty Subset of (( TOP-REAL 2) | Q);

      

       A23: ((( TOP-REAL 2) | Q) | SEG) = (( TOP-REAL 2) | R) by A9, GOBOARD9: 2;

      reconsider hh9 = gg as Function of ( I[01] | Poz), ((( TOP-REAL 2) | Q) | SEG) by A19, A20, FUNCT_2: 6;

      

       A24: F is continuous by A2, TOPS_2:def 5;

      

       A25: F is one-to-one by A2, TOPS_2:def 5;

      gg is continuous by A18, A24, TOPMETR: 7;

      then

       A26: hh9 is continuous by TOPMETR: 6;

      

       A27: hh9 is one-to-one by A25, FUNCT_1: 52;

      reconsider hh = hh9 as Function of ( I[01] | Poz), (( TOP-REAL 2) | R) by A9, GOBOARD9: 2;

      

       A28: ( dom hh) = ( [#] ( I[01] | Poz)) by FUNCT_2:def 1;

      then

       A29: ( dom hh) = Poz by PRE_TOPC:def 5;

      

       A30: ( rng hh) = (hh .: ( dom hh)) by A28, RELSET_1: 22

      .= ( [#] ((( TOP-REAL 2) | Q) | SEG)) by A7, A13, A15, A16, A19, A29, BORSUK_1: 40, FUNCT_1: 87, RELAT_1: 129;

      reconsider A = ( Closed-Interval-TSpace (ppi,pi1)) as strict SubSpace of I[01] by A10, A11, A12, TOPMETR: 20, TREAL_1: 3;

      

       A31: Poz = ( [#] A) by A10, TOPMETR: 18;

      ( Closed-Interval-TSpace (ppi,pi1)) is compact by A10, HEINE: 4;

      then ( [#] ( Closed-Interval-TSpace (ppi,pi1))) is compact by COMPTS_1: 1;

      then for P be Subset of A st P = Poz holds P is compact by A10, TOPMETR: 18;

      then Poz is compact by A31, COMPTS_1: 2;

      then

       A32: ( I[01] | Poz) is compact by COMPTS_1: 3;

      (( TOP-REAL 2) | R) is T_2 by TOPMETR: 2;

      hence thesis by A18, A23, A26, A27, A30, A32, COMPTS_1: 17;

    end;

    begin

    theorem :: JORDAN5B:9

    

     Th9: for p1,p2,p be Point of ( TOP-REAL 2) st p1 <> p2 & p in ( LSeg (p1,p2)) holds LE (p,p,p1,p2) by JORDAN5A: 2;

    theorem :: JORDAN5B:10

    

     Th10: for p,p1,p2 be Point of ( TOP-REAL 2) st p1 <> p2 & p in ( LSeg (p1,p2)) holds LE (p1,p,p1,p2)

    proof

      let p,p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p1 <> p2 and

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

      thus LE (p1,p,p1,p2)

      proof

        thus p1 in ( LSeg (p1,p2)) & p in ( LSeg (p1,p2)) by A2, RLTOPSP1: 68;

        let r1,r2 be Real;

        assume that 0 <= r1 and r1 <= 1 and

         A3: p1 = (((1 - r1) * p1) + (r1 * p2)) and

         A4: 0 <= r2 and r2 <= 1 and p = (((1 - r2) * p1) + (r2 * p2));

        ( 0. ( TOP-REAL 2)) = ((((1 - r1) * p1) + (r1 * p2)) + ( - p1)) by A3, RLVECT_1: 5

        .= ((((1 - r1) * p1) + (r1 * p2)) - p1)

        .= (((1 - r1) * p1) + ((r1 * p2) - p1)) by RLVECT_1:def 3

        .= (((1 - r1) * p1) + (( - p1) + (r1 * p2)))

        .= ((((1 - r1) * p1) + ( - p1)) + (r1 * p2)) by RLVECT_1:def 3

        .= ((((1 - r1) * p1) - p1) + (r1 * p2));

        

        then ( - (r1 * p2)) = (((((1 - r1) * p1) - p1) + (r1 * p2)) + ( - (r1 * p2))) by RLVECT_1: 4

        .= (((((1 - r1) * p1) - p1) + (r1 * p2)) - (r1 * p2))

        .= ((((1 - r1) * p1) - p1) + ((r1 * p2) - (r1 * p2))) by RLVECT_1:def 3

        .= ((((1 - r1) * p1) - p1) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5

        .= (((1 - r1) * p1) - p1) by RLVECT_1: 4

        .= (((1 - r1) * p1) - (1 * p1)) by RLVECT_1:def 8

        .= (((1 - r1) - 1) * p1) by RLVECT_1: 35

        .= (( - r1) * p1)

        .= ( - (r1 * p1)) by RLVECT_1: 79;

        

        then (r1 * p1) = ( - ( - (r1 * p2)))

        .= (r1 * p2);

        hence thesis by A1, A4, RLVECT_1: 36;

      end;

    end;

    theorem :: JORDAN5B:11

    

     Th11: for p,p1,p2 be Point of ( TOP-REAL 2) st p in ( LSeg (p1,p2)) & p1 <> p2 holds LE (p,p2,p1,p2)

    proof

      let p,p1,p2 be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( LSeg (p1,p2)) and

       A2: p1 <> p2;

      thus LE (p,p2,p1,p2)

      proof

        thus p in ( LSeg (p1,p2)) & p2 in ( LSeg (p1,p2)) by A1, RLTOPSP1: 68;

        let r1,r2 be Real such that 0 <= r1 and

         A3: r1 <= 1 and p = (((1 - r1) * p1) + (r1 * p2)) and 0 <= r2 and r2 <= 1 and

         A4: p2 = (((1 - r2) * p1) + (r2 * p2));

        p2 = (1 * p2) by RLVECT_1:def 8

        .= (( 0. ( TOP-REAL 2)) + (1 * p2)) by RLVECT_1: 4

        .= (((1 - 1) * p1) + (1 * p2)) by RLVECT_1: 10;

        hence thesis by A2, A3, A4, JORDAN5A: 2;

      end;

    end;

    theorem :: JORDAN5B:12

    for p1,p2,q1,q2,q3 be Point of ( TOP-REAL 2) st p1 <> p2 & LE (q1,q2,p1,p2) & LE (q2,q3,p1,p2) holds LE (q1,q3,p1,p2)

    proof

      let p1,p2,q1,q2,q3 be Point of ( TOP-REAL 2);

      assume that

       A1: p1 <> p2 and

       A2: LE (q1,q2,p1,p2) and

       A3: LE (q2,q3,p1,p2);

      

       A4: q1 in ( LSeg (p1,p2)) by A2;

      

       A5: q2 in ( LSeg (p1,p2)) by A2;

      

       A6: q3 in ( LSeg (p1,p2)) by A3;

      consider s1 be Real such that

       A7: q1 = (((1 - s1) * p1) + (s1 * p2)) and 0 <= s1 and

       A8: s1 <= 1 by A4;

      consider s2 be Real such that

       A9: q2 = (((1 - s2) * p1) + (s2 * p2)) and

       A10: 0 <= s2 and

       A11: s2 <= 1 by A5;

      

       A12: s1 <= s2 by A2, A7, A8, A9, A10, A11;

      consider s3 be Real such that

       A13: q3 = (((1 - s3) * p1) + (s3 * p2)) and

       A14: 0 <= s3 and

       A15: s3 <= 1 by A6;

      s2 <= s3 by A3, A9, A11, A13, A14, A15;

      then

       A16: s1 <= s3 by A12, XXREAL_0: 2;

      thus LE (q1,q3,p1,p2)

      proof

        thus q1 in ( LSeg (p1,p2)) & q3 in ( LSeg (p1,p2)) by A2, A3;

        let r1,r2 be Real;

        assume that 0 <= r1 and r1 <= 1 and

         A17: q1 = (((1 - r1) * p1) + (r1 * p2)) and 0 <= r2 and r2 <= 1 and

         A18: q3 = (((1 - r2) * p1) + (r2 * p2));

        s1 = r1 by A1, A7, A17, JORDAN5A: 2;

        hence thesis by A1, A13, A16, A18, JORDAN5A: 2;

      end;

    end;

    theorem :: JORDAN5B:13

    for p,q be Point of ( TOP-REAL 2) st p <> q holds ( LSeg (p,q)) = { p1 where p1 be Point of ( TOP-REAL 2) : LE (p,p1,p,q) & LE (p1,q,p,q) }

    proof

      let p,q be Point of ( TOP-REAL 2);

      assume

       A1: p <> q;

      thus ( LSeg (p,q)) c= { p1 where p1 be Point of ( TOP-REAL 2) : LE (p,p1,p,q) & LE (p1,q,p,q) }

      proof

        let a be object;

        assume

         A2: a in ( LSeg (p,q));

        then

        reconsider a9 = a as Point of ( TOP-REAL 2);

        

         A3: LE (p,a9,p,q) by A1, A2, Th10;

         LE (a9,q,p,q) by A1, A2, Th11;

        hence thesis by A3;

      end;

      thus { p1 where p1 be Point of ( TOP-REAL 2) : LE (p,p1,p,q) & LE (p1,q,p,q) } c= ( LSeg (p,q))

      proof

        let a be object;

        assume a in { p1 where p1 be Point of ( TOP-REAL 2) : LE (p,p1,p,q) & LE (p1,q,p,q) };

        then ex a9 be Point of ( TOP-REAL 2) st (a9 = a) & ( LE (p,a9,p,q)) & ( LE (a9,q,p,q));

        hence thesis;

      end;

    end;

    theorem :: JORDAN5B:14

    for n be Nat, P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) holds P is_an_arc_of (p2,p1)

    proof

      let n be Nat, P be Subset of ( TOP-REAL n), p1,p2 be Point of ( TOP-REAL n);

      assume

       A1: P is_an_arc_of (p1,p2);

      then

      consider f be Function of I[01] , (( TOP-REAL n) | P) such that

       A2: f is being_homeomorphism and

       A3: (f . 0 ) = p1 and

       A4: (f . 1) = p2 by TOPREAL1:def 1;

      set Ex = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

      

       A5: Ex is being_homeomorphism by TREAL_1: 18;

      set g = (f * Ex);

      

       A6: (Ex . (( 0 ,1) (#) )) = 0 by BORSUK_1:def 14, TREAL_1: 5, TREAL_1: 9;

      

       A7: (Ex . ( (#) ( 0 ,1))) = 1 by BORSUK_1:def 15, TREAL_1: 5, TREAL_1: 9;

      ( dom f) = ( [#] I[01] ) by A2, TOPS_2:def 5;

      then ( rng Ex) = ( dom f) by A5, TOPMETR: 20, TOPS_2:def 5;

      then

       A8: ( dom g) = ( dom Ex) by RELAT_1: 27;

      reconsider P as non empty Subset of ( TOP-REAL n) by A1, TOPREAL1: 1;

      

       A9: ( dom g) = ( [#] I[01] ) by A5, A8, TOPMETR: 20, TOPS_2:def 5;

      reconsider g as Function of I[01] , (( TOP-REAL n) | P) by TOPMETR: 20;

      

       A10: g is being_homeomorphism by A2, A5, TOPMETR: 20, TOPS_2: 57;

      

       A11: (g . 0 ) = p2 by A4, A7, A9, BORSUK_1:def 14, FUNCT_1: 12, TREAL_1: 5;

      (g . 1) = p1 by A3, A6, A9, BORSUK_1:def 15, FUNCT_1: 12, TREAL_1: 5;

      hence thesis by A10, A11, TOPREAL1:def 1;

    end;

    theorem :: JORDAN5B:15

    for i be Nat, f be FinSequence of ( TOP-REAL 2), P be Subset of ( TOP-REAL 2) st f is being_S-Seq & 1 <= i & (i + 1) <= ( len f) & P = ( LSeg (f,i)) holds P is_an_arc_of ((f /. i),(f /. (i + 1)))

    proof

      let i be Nat, f be FinSequence of ( TOP-REAL 2), P be Subset of ( TOP-REAL 2);

      assume that

       A1: f is being_S-Seq and

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: P = ( LSeg (f,i));

      

       A5: i in ( dom f) by A2, A3, SEQ_4: 134;

      

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

      

       A7: f is one-to-one by A1;

      

       A8: ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A2, A3, TOPREAL1:def 3;

      (f /. i) <> (f /. (i + 1))

      proof

        assume (f /. i) = (f /. (i + 1));

        then i = (i + 1) by A5, A6, A7, PARTFUN2: 10;

        hence thesis;

      end;

      hence thesis by A4, A8, TOPREAL1: 9;

    end;

    begin

    theorem :: JORDAN5B:16

    for g1 be FinSequence of ( TOP-REAL 2), i be Nat st 1 <= i & i <= ( len g1) & g1 is being_S-Seq holds (g1 /. 1) in ( L~ ( mid (g1,i,( len g1)))) implies i = 1

    proof

      let g1 be FinSequence of ( TOP-REAL 2), i be Nat;

      assume that

       A1: 1 <= i and

       A2: i <= ( len g1) and

       A3: g1 is being_S-Seq;

      assume (g1 /. 1) in ( L~ ( mid (g1,i,( len g1))));

      then

      consider j be Nat such that

       A4: 1 <= j and

       A5: (j + 1) <= ( len ( mid (g1,i,( len g1)))) and

       A6: (g1 /. 1) in ( LSeg (( mid (g1,i,( len g1))),j)) by SPPOL_2: 13;

      

       A7: (j + 1) in ( dom ( mid (g1,i,( len g1)))) by A4, A5, SEQ_4: 134;

      

       A8: ( mid (g1,i,( len g1))) = (g1 /^ (i -' 1)) by A2, FINSEQ_6: 117;

      j <= (j + 1) by NAT_1: 11;

      then

       A9: j <= ( len (g1 /^ (i -' 1))) by A5, A8, XXREAL_0: 2;

      then

       A10: j in ( dom (g1 /^ (i -' 1))) by A4, FINSEQ_3: 25;

      (i -' 1) <= i by A1, Th1;

      then

       A11: (i -' 1) <= ( len g1) by A2, XXREAL_0: 2;

      then

       A12: j <= (( len g1) - (i -' 1)) by A9, RFINSEQ:def 1;

      j <= ((i -' 1) + j) by NAT_1: 11;

      then

       A13: 1 <= ((i -' 1) + j) by A4, XXREAL_0: 2;

      

       A14: (j + (i -' 1)) <= ( len g1) by A12, XREAL_1: 19;

      then

       A15: ((i -' 1) + j) in ( dom g1) by A13, FINSEQ_3: 25;

      

       A16: ((g1 /^ (i -' 1)) /. j) = ((g1 /^ (i -' 1)) . j) by A10, PARTFUN1:def 6

      .= (g1 . ((i -' 1) + j)) by A4, A14, FINSEQ_6: 114

      .= (g1 /. ((i -' 1) + j)) by A15, PARTFUN1:def 6;

      

       A17: 1 <= (j + 1) by NAT_1: 11;

      (j + 1) <= ((i -' 1) + (j + 1)) by NAT_1: 11;

      then

       A18: 1 <= ((i -' 1) + (j + 1)) by A17, XXREAL_0: 2;

      (j + 1) <= ( len (g1 /^ (i -' 1))) by A2, A5, FINSEQ_6: 117;

      then

       A19: (j + 1) <= (( len g1) - (i -' 1)) by A11, RFINSEQ:def 1;

      

       A20: 1 <= (j + 1) by A7, FINSEQ_3: 25;

      

       A21: ((j + 1) + (i -' 1)) <= ( len g1) by A19, XREAL_1: 19;

      then

       A22: ((i -' 1) + (j + 1)) in ( dom g1) by A18, FINSEQ_3: 25;

      (j + 1) in ( dom (g1 /^ (i -' 1))) by A2, A7, FINSEQ_6: 117;

      

      then

       A23: ((g1 /^ (i -' 1)) /. (j + 1)) = ((g1 /^ (i -' 1)) . (j + 1)) by PARTFUN1:def 6

      .= (g1 . ((i -' 1) + (j + 1))) by A20, A21, FINSEQ_6: 114

      .= (g1 /. ((i -' 1) + (j + 1))) by A22, PARTFUN1:def 6;

      

       A24: (((i -' 1) + j) + 1) = ((i -' 1) + (j + 1));

      

       A25: (((i -' 1) + j) + 1) <= ( len g1) by A21;

      

       A26: ( LSeg (( mid (g1,i,( len g1))),j)) = ( LSeg ((g1 /. ((i -' 1) + j)),(g1 /. ((i -' 1) + (j + 1))))) by A4, A5, A8, A16, A23, TOPREAL1:def 3

      .= ( LSeg (g1,((i -' 1) + j))) by A13, A21, A24, TOPREAL1:def 3;

      

       A27: (1 + 1) <= ( len g1) by A3, TOPREAL1:def 8;

      then (g1 /. 1) in ( LSeg (g1,1)) by TOPREAL1: 21;

      then

       A28: (g1 /. 1) in (( LSeg (g1,1)) /\ ( LSeg (g1,((i -' 1) + j)))) by A6, A26, XBOOLE_0:def 4;

      then

       A29: ( LSeg (g1,1)) meets ( LSeg (g1,((i -' 1) + j)));

      assume i <> 1;

      then 1 < i by A1, XXREAL_0: 1;

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

      then (2 -' 1) <= (i -' 1) by NAT_D: 42;

      then ((2 -' 1) + 1) <= ((i -' 1) + j) by A4, XREAL_1: 7;

      then

       A30: ((i -' 1) + j) >= 2 by XREAL_1: 235;

      

       A31: g1 is s.n.c. unfolded one-to-one by A3;

      

       A32: 1 in ( dom g1) by A27, SEQ_4: 134;

      

       A33: (1 + 1) in ( dom g1) by A27, SEQ_4: 134;

      per cases by A30, XXREAL_0: 1;

        suppose ((i -' 1) + j) = 2;

        then (g1 /. 1) in {(g1 /. (1 + 1))} by A25, A28, A31, TOPREAL1:def 6;

        then (g1 /. 1) = (g1 /. (1 + 1)) by TARSKI:def 1;

        hence thesis by A31, A32, A33, PARTFUN2: 10;

      end;

        suppose ((i -' 1) + j) > 2;

        then ((i -' 1) + j) > (1 + 1);

        hence thesis by A29, A31, TOPREAL1:def 7;

      end;

    end;

    theorem :: JORDAN5B:17

    for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st f is being_S-Seq & p = (f . ( len f)) holds ( L_Cut (f,p)) = <*p*>

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: f is being_S-Seq and

       A2: p = (f . ( len f));

      ( len f) >= 2 by A1, TOPREAL1:def 8;

      then p in ( L~ f) by A2, JORDAN3: 1;

      then

       A3: p in ( L~ ( Rev f)) by SPPOL_2: 22;

      

       A4: ( L_Cut (f,p)) = ( L_Cut (( Rev ( Rev f)),p))

      .= ( Rev ( R_Cut (( Rev f),p))) by A1, A3, JORDAN3: 22;

      p = (( Rev f) . 1) by A2, FINSEQ_5: 62;

      then ( R_Cut (( Rev f),p)) = <*p*> by JORDAN3:def 4;

      hence thesis by A4, FINSEQ_5: 60;

    end;

    theorem :: JORDAN5B:18

    for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) & p <> (f . ( len f)) & f is being_S-Seq holds ( Index (p,( L_Cut (f,p)))) = 1

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: p <> (f . ( len f)) and

       A3: f is being_S-Seq;

      ( L_Cut (f,p)) is being_S-Seq by A1, A2, A3, JORDAN3: 34;

      then

       A4: 2 <= ( len ( L_Cut (f,p))) by TOPREAL1:def 8;

      then 1 <= ( len ( L_Cut (f,p))) by XXREAL_0: 2;

      then 1 in ( dom ( L_Cut (f,p))) by FINSEQ_3: 25;

      

      then (( L_Cut (f,p)) /. 1) = (( L_Cut (f,p)) . 1) by PARTFUN1:def 6

      .= p by A1, JORDAN3: 23;

      hence thesis by A4, JORDAN3: 11;

    end;

    theorem :: JORDAN5B:19

    

     Th19: for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) & f is being_S-Seq & p <> (f . ( len f)) holds p in ( L~ ( L_Cut (f,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: f is being_S-Seq;

      assume p <> (f . ( len f));

      then ( L_Cut (f,p)) is being_S-Seq by A1, A2, JORDAN3: 34;

      then

       A3: ( len ( L_Cut (f,p))) >= 2 by TOPREAL1:def 8;

      (( L_Cut (f,p)) . 1) = p by A1, JORDAN3: 23;

      hence thesis by A3, JORDAN3: 1;

    end;

    theorem :: JORDAN5B:20

    for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) & f is being_S-Seq & p <> (f . 1) holds p in ( L~ ( R_Cut (f,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: f is being_S-Seq;

      assume p <> (f . 1);

      then ( R_Cut (f,p)) is being_S-Seq by A1, A2, JORDAN3: 35;

      then

       A3: ( len ( R_Cut (f,p))) >= 2 by TOPREAL1:def 8;

      (( R_Cut (f,p)) . ( len ( R_Cut (f,p)))) = p by A1, JORDAN3: 24;

      hence thesis by A3, JORDAN3: 1;

    end;

    theorem :: JORDAN5B:21

    

     Th21: for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) & f is one-to-one holds ( B_Cut (f,p,p)) = <*p*>

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: f is one-to-one;

      

       A3: ( Index (p,f)) <> (( Index (p,f)) + 1);

      

       A4: ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

      

       A5: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

      

       A6: (( Index (p,f)) + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A7: ( Index (p,f)) in ( dom f) by A5, SEQ_4: 134;

      

       A8: (( Index (p,f)) + 1) in ( dom f) by A5, A6, SEQ_4: 134;

      p in ( LSeg (f,( Index (p,f)))) by A1, JORDAN3: 9;

      then p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A5, A6, TOPREAL1:def 3;

      then

       A9: LE (p,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A2, A3, A7, A8, Th9, PARTFUN2: 10;

      (( L_Cut (f,p)) . 1) = p by A1, JORDAN3: 23;

      then ( R_Cut (( L_Cut (f,p)),p)) = <*p*> by JORDAN3:def 4;

      hence thesis by A9, JORDAN3:def 7;

    end;

    

     Lm2: for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & p <> (f . ( len f)) & f is being_S-Seq holds p in ( L~ ( L_Cut (f,q))) or q in ( L~ ( L_Cut (f,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: q in ( L~ f) and

       A3: p <> (f . ( len f)) and

       A4: f is being_S-Seq;

      

       A5: ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

      

       A6: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

      

       A7: (( Index (p,f)) + 1) <= ( len f) by A5, NAT_1: 13;

      then

       A8: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A6, TOPREAL1:def 3;

      

       A9: ( Index (p,f)) in ( dom f) by A6, A7, SEQ_4: 134;

      

       A10: (( Index (p,f)) + 1) in ( dom f) by A6, A7, SEQ_4: 134;

      

       A11: f is one-to-one by A4;

      ( Index (p,f)) < (( Index (p,f)) + 1) by NAT_1: 13;

      then

       A12: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A9, A10, A11, PARTFUN2: 10;

      per cases by XXREAL_0: 1;

        suppose ( Index (p,f)) < ( Index (q,f));

        hence thesis by A1, A2, JORDAN3: 29;

      end;

        suppose

         A13: ( Index (p,f)) = ( Index (q,f));

        

         A14: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A1, A8, JORDAN3: 9;

        q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A2, A8, A13, JORDAN3: 9;

        then

         A15: LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) or LT (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A12, A14, JORDAN3: 28;

        now

          per cases by A15;

            suppose

             A16: LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

            thus p in ( L~ ( L_Cut (f,q))) or q in ( L~ ( L_Cut (f,p)))

            proof

              per cases ;

                suppose p <> q;

                hence thesis by A1, A2, A13, A16, JORDAN3: 31;

              end;

                suppose p = q;

                hence thesis by A1, A3, A4, Th19;

              end;

            end;

          end;

            suppose

             A17: LE (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

            thus p in ( L~ ( L_Cut (f,q))) or q in ( L~ ( L_Cut (f,p)))

            proof

              per cases ;

                suppose p <> q;

                hence thesis by A1, A2, A13, A17, JORDAN3: 31;

              end;

                suppose p = q;

                hence thesis by A1, A3, A4, Th19;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

        suppose ( Index (p,f)) > ( Index (q,f));

        hence thesis by A1, A2, JORDAN3: 29;

      end;

    end;

    theorem :: JORDAN5B:22

    

     Th22: for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & q <> (f . ( len f)) & p = (f . ( len f)) & f is being_S-Seq holds p in ( L~ ( L_Cut (f,q)))

    proof

      let f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: q in ( L~ f) and

       A3: q <> (f . ( len f)) and

       A4: p = (f . ( len f)) and

       A5: f is being_S-Seq;

      (1 + 1) <= ( len f) by A5, TOPREAL1:def 8;

      then

       A6: 1 < ( len f) by XXREAL_0: 2;

      then

       A7: (( Index (p,f)) + 1) = ( len f) by A4, A5, JORDAN3: 12;

      

       AA: ( len f) in ( dom f) by A6, FINSEQ_3: 25;

      

      then

       AB: ( mid (f,( len f),( len f))) = <*(f . ( len f))*> by JORDAN4: 15

      .= <*(f /. ( len f))*> by AA, PARTFUN1:def 6;

      ( Index (q,f)) < ( len f) by A2, JORDAN3: 8;

      then

       A8: ( Index (q,f)) <= ( Index (p,f)) by A7, NAT_1: 13;

      per cases by A8, XXREAL_0: 1;

        suppose ( Index (q,f)) = ( Index (p,f));

        

        then

         A9: ( L_Cut (f,q)) = ( <*q*> ^ ( mid (f,( len f),( len f)))) by A3, A7, JORDAN3:def 3

        .= ( <*q*> ^ <*(f /. ( len f))*>) by AB

        .= <*q, (f /. ( len f))*> by FINSEQ_1:def 9

        .= <*q, p*> by A4, A6, FINSEQ_4: 15;

        then ( rng ( L_Cut (f,q))) = {p, q} by FINSEQ_2: 127;

        then

         A10: p in ( rng ( L_Cut (f,q))) by TARSKI:def 2;

        ( len ( L_Cut (f,q))) = 2 by A9, FINSEQ_1: 44;

        then ( rng ( L_Cut (f,q))) c= ( L~ ( L_Cut (f,q))) by SPPOL_2: 18;

        hence thesis by A10;

      end;

        suppose ( Index (q,f)) < ( Index (p,f));

        hence thesis by A1, A2, JORDAN3: 29;

      end;

    end;

    theorem :: JORDAN5B:23

    for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p <> (f . ( len f)) & p in ( L~ f) & q in ( L~ f) & f is being_S-Seq holds p in ( L~ ( L_Cut (f,q))) or q in ( L~ ( L_Cut (f,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2);

      assume

       A1: p <> (f . ( len f));

      assume that

       A2: p in ( L~ f) and

       A3: q in ( L~ f) and

       A4: f is being_S-Seq;

      per cases by A1;

        suppose p <> (f . ( len f)) & q = (f . ( len f));

        hence thesis by A2, A3, A4, Th22;

      end;

        suppose p = (f . ( len f)) & q <> (f . ( len f));

        hence thesis by A2, A3, A4, Th22;

      end;

        suppose p <> (f . ( len f)) & q <> (f . ( len f));

        hence thesis by A2, A3, A4, Lm2;

      end;

    end;

    

     Lm3: for f be FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) & p <> q holds ( L~ ( B_Cut (f,p,q))) c= ( L~ f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f) and

       A2: q in ( L~ f) and

       A3: ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) and

       A4: p <> q;

      

       A5: ( B_Cut (f,p,q)) = ( R_Cut (( L_Cut (f,p)),q)) by A1, A2, A3, JORDAN3:def 7;

      now

        per cases by A3;

          case ( Index (p,f)) < ( Index (q,f));

          then q in ( L~ ( L_Cut (f,p))) by A1, A2, JORDAN3: 29;

          hence ex i1 be Nat st 1 <= i1 & (i1 + 1) <= ( len ( L_Cut (f,p))) & q in ( LSeg (( L_Cut (f,p)),i1)) by SPPOL_2: 13;

        end;

          case ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          then q in ( L~ ( L_Cut (f,p))) by A1, A2, A4, JORDAN3: 31;

          hence ex i1 be Nat st 1 <= i1 & (i1 + 1) <= ( len ( L_Cut (f,p))) & q in ( LSeg (( L_Cut (f,p)),i1)) by SPPOL_2: 13;

        end;

      end;

      then

       A6: ( L~ ( B_Cut (f,p,q))) c= ( L~ ( L_Cut (f,p))) by A5, JORDAN3: 41, SPPOL_2: 17;

      ( L~ ( L_Cut (f,p))) c= ( L~ f) by A1, JORDAN3: 42;

      hence thesis by A6;

    end;

    theorem :: JORDAN5B:24

    for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & f is being_S-Seq holds ( L~ ( B_Cut (f,p,q))) c= ( L~ f)

    proof

      let f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f) and

       A2: q in ( L~ f) and

       A3: f is being_S-Seq;

      

       A4: f is one-to-one by A3;

      per cases ;

        suppose p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A4, Th21;

        then ( len ( B_Cut (f,p,q))) = 1 by FINSEQ_1: 39;

        then ( L~ ( B_Cut (f,p,q))) = {} by TOPREAL1: 22;

        hence thesis;

      end;

        suppose p <> q & (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

        hence thesis by A1, A2, Lm3;

      end;

        suppose that

         A5: p <> q and

         A6: not (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

        

         A7: ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A6, JORDAN3:def 7;

        

         A8: ( Index (q,f)) < ( Index (p,f)) or ( Index (p,f)) = ( Index (q,f)) & not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A6, XXREAL_0: 1;

         A9:

        now

          assume that

           A10: ( Index (p,f)) = ( Index (q,f)) and

           A11: not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          

           A12: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

          

           A13: ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

          then

           A14: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

          then

           A15: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A12, TOPREAL1:def 3;

          then

           A16: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A1, JORDAN3: 9;

          

           A17: q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A2, A10, A15, JORDAN3: 9;

          

           A18: ( Index (p,f)) in ( dom f) by A12, A13, FINSEQ_3: 25;

          1 <= (( Index (p,f)) + 1) by NAT_1: 11;

          then

           A19: (( Index (p,f)) + 1) in ( dom f) by A14, FINSEQ_3: 25;

          (( Index (p,f)) + 0 ) <> (( Index (p,f)) + 1);

          then (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A4, A18, A19, PARTFUN2: 10;

          then LT (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A11, A16, A17, JORDAN3: 28;

          hence LE (q,p,(f /. ( Index (q,f))),(f /. (( Index (q,f)) + 1))) by A10;

        end;

        then

         A20: ( Rev ( B_Cut (f,q,p))) = ( B_Cut (f,p,q)) by A1, A2, A7, A8, JORDAN3:def 7;

        ( L~ ( B_Cut (f,q,p))) c= ( L~ f) by A1, A2, A5, A8, A9, Lm3;

        hence thesis by A20, SPPOL_2: 22;

      end;

    end;

    theorem :: JORDAN5B:25

    for f be non constant standard special_circular_sequence, i,j be Nat st 1 <= i & j <= ( len ( GoB f)) & i < j holds (( LSeg ((( GoB f) * (1,( width ( GoB f)))),(( GoB f) * (i,( width ( GoB f)))))) /\ ( LSeg ((( GoB f) * (j,( width ( GoB f)))),(( GoB f) * (( len ( GoB f)),( width ( GoB f))))))) = {}

    proof

      let f be non constant standard special_circular_sequence, i,j be Nat;

      assume that

       A1: 1 <= i and

       A2: j <= ( len ( GoB f)) and

       A3: i < j;

      set A = ( LSeg ((( GoB f) * (1,( width ( GoB f)))),(( GoB f) * (i,( width ( GoB f)))))), B = ( LSeg ((( GoB f) * (j,( width ( GoB f)))),(( GoB f) * (( len ( GoB f)),( width ( GoB f))))));

      assume (A /\ B) <> {} ;

      then A meets B;

      then

      consider x be object such that

       A4: x in A and

       A5: x in B by XBOOLE_0: 3;

      reconsider x1 = x as Point of ( TOP-REAL 2) by A4;

      

       A6: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      

       A7: i <= ( len ( GoB f)) by A2, A3, XXREAL_0: 2;

      ((( GoB f) * (1,( width ( GoB f)))) `1 ) <= ((( GoB f) * (i,( width ( GoB f)))) `1 )

      proof

        per cases by A1, XXREAL_0: 1;

          suppose i = 1;

          hence thesis;

        end;

          suppose i > 1;

          hence thesis by A6, A7, GOBOARD5: 3;

        end;

      end;

      then

       A8: (x1 `1 ) <= ((( GoB f) * (i,( width ( GoB f)))) `1 ) by A4, TOPREAL1: 3;

      

       A9: ((( GoB f) * (j,( width ( GoB f)))) `1 ) > ((( GoB f) * (i,( width ( GoB f)))) `1 ) by A1, A2, A3, A6, GOBOARD5: 3;

      

       A10: 1 <= j by A1, A3, XXREAL_0: 2;

      ((( GoB f) * (j,( width ( GoB f)))) `1 ) <= ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `1 )

      proof

        per cases by A2, XXREAL_0: 1;

          suppose j < ( len ( GoB f));

          hence thesis by A6, A10, GOBOARD5: 3;

        end;

          suppose j = ( len ( GoB f));

          hence thesis;

        end;

      end;

      then (x1 `1 ) >= ((( GoB f) * (j,( width ( GoB f)))) `1 ) by A5, TOPREAL1: 3;

      hence thesis by A8, A9, XXREAL_0: 2;

    end;

    theorem :: JORDAN5B:26

    for f be non constant standard special_circular_sequence, i,j be Nat st 1 <= i & j <= ( width ( GoB f)) & i < j holds (( LSeg ((( GoB f) * (( len ( GoB f)),1)),(( GoB f) * (( len ( GoB f)),i)))) /\ ( LSeg ((( GoB f) * (( len ( GoB f)),j)),(( GoB f) * (( len ( GoB f)),( width ( GoB f))))))) = {}

    proof

      let f be non constant standard special_circular_sequence, i,j be Nat;

      assume that

       A1: 1 <= i and

       A2: j <= ( width ( GoB f)) and

       A3: i < j;

      set A = ( LSeg ((( GoB f) * (( len ( GoB f)),1)),(( GoB f) * (( len ( GoB f)),i)))), B = ( LSeg ((( GoB f) * (( len ( GoB f)),j)),(( GoB f) * (( len ( GoB f)),( width ( GoB f))))));

      assume (A /\ B) <> {} ;

      then A meets B;

      then

      consider x be object such that

       A4: x in A and

       A5: x in B by XBOOLE_0: 3;

      reconsider x1 = x as Point of ( TOP-REAL 2) by A4;

      

       A6: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      

       A7: i <= ( width ( GoB f)) by A2, A3, XXREAL_0: 2;

      ((( GoB f) * (( len ( GoB f)),1)) `2 ) <= ((( GoB f) * (( len ( GoB f)),i)) `2 )

      proof

        per cases by A1, XXREAL_0: 1;

          suppose i = 1;

          hence thesis;

        end;

          suppose i > 1;

          hence thesis by A6, A7, GOBOARD5: 4;

        end;

      end;

      then

       A8: (x1 `2 ) <= ((( GoB f) * (( len ( GoB f)),i)) `2 ) by A4, TOPREAL1: 4;

      

       A9: ((( GoB f) * (( len ( GoB f)),j)) `2 ) > ((( GoB f) * (( len ( GoB f)),i)) `2 ) by A1, A2, A3, A6, GOBOARD5: 4;

      

       A10: 1 <= j by A1, A3, XXREAL_0: 2;

      ((( GoB f) * (( len ( GoB f)),j)) `2 ) <= ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `2 )

      proof

        per cases by A2, XXREAL_0: 1;

          suppose j < ( width ( GoB f));

          hence thesis by A6, A10, GOBOARD5: 4;

        end;

          suppose j = ( width ( GoB f));

          hence thesis;

        end;

      end;

      then (x1 `2 ) >= ((( GoB f) * (( len ( GoB f)),j)) `2 ) by A5, TOPREAL1: 4;

      hence thesis by A8, A9, XXREAL_0: 2;

    end;

    theorem :: JORDAN5B:27

    

     Th27: for f be FinSequence of ( TOP-REAL 2) st f is being_S-Seq holds ( L_Cut (f,(f /. 1))) = f

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is being_S-Seq;

      then

       A2: (1 + 1) <= ( len f) by TOPREAL1:def 8;

      then 1 <= ( len f) by XXREAL_0: 2;

      then

       A3: 1 in ( dom f) by FINSEQ_3: 25;

      

       A4: (1 + 1) in ( dom f) by A2, FINSEQ_3: 25;

      

       A5: 1 < ( len f) by A2, NAT_1: 13;

      

       A6: f is one-to-one by A1;

      

       A7: (f /. 1) = (f . 1) by A3, PARTFUN1:def 6;

      

       A8: ( Index ((f /. 1),f)) = 1 by A2, JORDAN3: 11;

      (f /. 1) <> (f /. (1 + 1)) by A3, A4, A6, PARTFUN2: 10;

      then (f /. 1) <> (f . (1 + 1)) by A4, PARTFUN1:def 6;

      

      hence ( L_Cut (f,(f /. 1))) = ( <*(f /. 1)*> ^ ( mid (f,(( Index ((f /. 1),f)) + 1),( len f)))) by A8, JORDAN3:def 3

      .= ( mid (f,1,( len f))) by A3, A5, A7, A8, FINSEQ_6: 126

      .= f by A2, FINSEQ_6: 120, XXREAL_0: 2;

    end;

    theorem :: JORDAN5B:28

    for f be FinSequence of ( TOP-REAL 2) st f is being_S-Seq holds ( R_Cut (f,(f /. ( len f)))) = f

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is being_S-Seq;

      then

       A2: 2 <= ( len f) by TOPREAL1:def 8;

      then

       A3: (f /. ( len f)) in ( L~ f) by JORDAN3: 1;

      

       A4: (f /. ( len f)) = (( Rev f) /. 1) by A2, CARD_1: 27, FINSEQ_5: 65;

      

      thus ( R_Cut (f,(f /. ( len f)))) = ( Rev ( Rev ( R_Cut (f,(f /. ( len f))))))

      .= ( Rev ( L_Cut (( Rev f),(f /. ( len f))))) by A1, A3, JORDAN3: 22

      .= ( Rev ( Rev f)) by A1, A4, Th27

      .= f;

    end;

    theorem :: JORDAN5B:29

    for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) holds p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))))

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume

       A1: p in ( L~ f);

      then

       A2: ( Index (p,f)) < ( len f) by JORDAN3: 8;

      

       A3: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

      

       A4: (( Index (p,f)) + 1) <= ( len f) by A2, NAT_1: 13;

      p in ( LSeg (f,( Index (p,f)))) by A1, JORDAN3: 9;

      hence thesis by A3, A4, TOPREAL1:def 3;

    end;

    theorem :: JORDAN5B:30

    for f be FinSequence of ( TOP-REAL 2) holds for i be Nat st f is unfolded s.n.c. one-to-one & ( len f) >= 2 & (f /. 1) in ( LSeg (f,i)) holds i = 1

    proof

      let f be FinSequence of ( TOP-REAL 2), i be Nat;

      assume that

       A1: f is unfolded s.n.c. one-to-one and

       A2: 2 <= ( len f);

      1 <= ( len f) by A2, XXREAL_0: 2;

      then

       A3: 1 in ( dom f) by FINSEQ_3: 25;

      

       A4: 2 in ( dom f) by A2, FINSEQ_3: 25;

      assume

       A5: (f /. 1) in ( LSeg (f,i));

      assume

       A6: i <> 1;

      per cases by A6, XXREAL_0: 1;

        suppose

         A7: i > 1;

        (1 + 1) <= ( len f) by A2;

        then (f /. 1) in ( LSeg (f,1)) by TOPREAL1: 21;

        then

         A8: (f /. 1) in (( LSeg (f,1)) /\ ( LSeg (f,i))) by A5, XBOOLE_0:def 4;

        then

         A9: ( LSeg (f,1)) meets ( LSeg (f,i));

        now

          per cases by XXREAL_0: 1;

            suppose

             A10: i = 2;

            then

             A11: (1 + 2) <= ( len f) by A5, TOPREAL1:def 3;

            (1 + 1) = 2;

            then (f /. 1) in {(f /. 2)} by A1, A8, A10, A11, TOPREAL1:def 6;

            then (f /. 1) = (f /. 2) by TARSKI:def 1;

            hence contradiction by A1, A3, A4, PARTFUN2: 10;

          end;

            suppose i > 2;

            then (1 + 1) < i;

            hence contradiction by A1, A9, TOPREAL1:def 7;

          end;

            suppose i < 2;

            then i < (1 + 1);

            hence contradiction by A7, NAT_1: 13;

          end;

        end;

        hence thesis;

      end;

        suppose i < 1;

        hence thesis by A5, TOPREAL1:def 3;

      end;

    end;

    theorem :: JORDAN5B:31

    for f be non constant standard special_circular_sequence, j be Nat, P be Subset of ( TOP-REAL 2) st 1 <= j & j <= ( width ( GoB f)) & P = ( LSeg ((( GoB f) * (1,j)),(( GoB f) * (( len ( GoB f)),j)))) holds P is_S-P_arc_joining ((( GoB f) * (1,j)),(( GoB f) * (( len ( GoB f)),j)))

    proof

      let f be non constant standard special_circular_sequence, j be Nat, P be Subset of ( TOP-REAL 2);

      assume that

       A1: 1 <= j and

       A2: j <= ( width ( GoB f)) and

       A3: P = ( LSeg ((( GoB f) * (1,j)),(( GoB f) * (( len ( GoB f)),j))));

      set p = (( GoB f) * (1,j)), q = (( GoB f) * (( len ( GoB f)),j));

      1 <= ( len ( GoB f)) by GOBOARD7: 32;

      then

       A4: (p `2 ) = (q `2 ) by A1, A2, GOBOARD5: 1;

      

       A5: (p `1 ) <> (q `1 )

      proof

        assume

         A6: (p `1 ) = (q `1 );

        

         A7: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

        

         A8: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

        then

         A9: [1, j] in ( Indices ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) by A1, A2, A7, MATRIX_0: 30;

        

         A10: [( len ( GoB f)), j] in ( Indices ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) by A1, A2, A7, A8, MATRIX_0: 30;

        (( GoB f) * (1,j)) = (( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) * (1,j)) by GOBOARD2:def 2

        .= |[(( Incr ( X_axis f)) . 1), (( Incr ( Y_axis f)) . j)]| by A9, GOBOARD2:def 1;

        then

         A11: (p `1 ) = (( Incr ( X_axis f)) . 1) by EUCLID: 52;

        

         A12: (( GoB f) * (( len ( GoB f)),j)) = (( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) * (( len ( GoB f)),j)) by GOBOARD2:def 2

        .= |[(( Incr ( X_axis f)) . ( len ( GoB f))), (( Incr ( Y_axis f)) . j)]| by A10, GOBOARD2:def 1;

        

         A13: ( len ( Incr ( X_axis f))) = ( len ( GoB f)) by A7, GOBOARD2:def 1;

        

         A14: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

        

         A15: 1 <= ( len ( Incr ( X_axis f))) by A13, GOBOARD7: 32;

        

         A16: ( len ( GoB f)) in ( dom ( Incr ( X_axis f))) by A13, A14, FINSEQ_3: 25;

        1 in ( dom ( Incr ( X_axis f))) by A15, FINSEQ_3: 25;

        then ( len ( GoB f)) = 1 by A6, A11, A12, A16, EUCLID: 52, SEQ_4: 138;

        hence thesis by GOBOARD7: 32;

      end;

      reconsider gg = <*p, q*> as FinSequence of the carrier of ( TOP-REAL 2);

      

       A17: ( len gg) = 2 by FINSEQ_1: 44;

      take gg;

      thus gg is being_S-Seq by A4, A5, SPPOL_2: 43;

      thus P = ( L~ gg) by A3, SPPOL_2: 21;

      thus thesis by A17, FINSEQ_4: 17;

    end;

    theorem :: JORDAN5B:32

    for f be non constant standard special_circular_sequence, j be Nat, P be Subset of ( TOP-REAL 2) st 1 <= j & j <= ( len ( GoB f)) & P = ( LSeg ((( GoB f) * (j,1)),(( GoB f) * (j,( width ( GoB f)))))) holds P is_S-P_arc_joining ((( GoB f) * (j,1)),(( GoB f) * (j,( width ( GoB f)))))

    proof

      let f be non constant standard special_circular_sequence, j be Nat, P be Subset of ( TOP-REAL 2);

      assume that

       A1: 1 <= j and

       A2: j <= ( len ( GoB f)) and

       A3: P = ( LSeg ((( GoB f) * (j,1)),(( GoB f) * (j,( width ( GoB f))))));

      set p = (( GoB f) * (j,1)), q = (( GoB f) * (j,( width ( GoB f))));

      1 <= ( width ( GoB f)) by GOBOARD7: 33;

      then

       A4: (p `1 ) = (q `1 ) by A1, A2, GOBOARD5: 2;

      

       A5: (p `2 ) <> (q `2 )

      proof

        assume

         A6: (p `2 ) = (q `2 );

        

         A7: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

        

         A8: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

        then

         A9: [j, 1] in ( Indices ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) by A1, A2, A7, MATRIX_0: 30;

        

         A10: [j, ( width ( GoB f))] in ( Indices ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) by A1, A2, A7, A8, MATRIX_0: 30;

        (( GoB f) * (j,1)) = (( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) * (j,1)) by GOBOARD2:def 2

        .= |[(( Incr ( X_axis f)) . j), (( Incr ( Y_axis f)) . 1)]| by A9, GOBOARD2:def 1;

        then

         A11: (p `2 ) = (( Incr ( Y_axis f)) . 1) by EUCLID: 52;

        

         A12: (( GoB f) * (j,( width ( GoB f)))) = (( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) * (j,( width ( GoB f)))) by GOBOARD2:def 2

        .= |[(( Incr ( X_axis f)) . j), (( Incr ( Y_axis f)) . ( width ( GoB f)))]| by A10, GOBOARD2:def 1;

        

         A13: ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by A7, GOBOARD2:def 1;

        

         A14: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

        

         A15: 1 <= ( len ( Incr ( Y_axis f))) by A13, GOBOARD7: 33;

        

         A16: ( width ( GoB f)) in ( dom ( Incr ( Y_axis f))) by A13, A14, FINSEQ_3: 25;

        1 in ( dom ( Incr ( Y_axis f))) by A15, FINSEQ_3: 25;

        then ( width ( GoB f)) = 1 by A6, A11, A12, A16, EUCLID: 52, SEQ_4: 138;

        hence thesis by GOBOARD7: 33;

      end;

      reconsider gg = <*p, q*> as FinSequence of the carrier of ( TOP-REAL 2);

      

       A17: ( len gg) = 2 by FINSEQ_1: 44;

      take gg;

      thus gg is being_S-Seq by A4, A5, SPPOL_2: 43;

      thus P = ( L~ gg) by A3, SPPOL_2: 21;

      thus thesis by A17, FINSEQ_4: 17;

    end;

    theorem :: JORDAN5B:33

    for f be FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) & p <> q holds ( L~ ( B_Cut (f,p,q))) c= ( L~ f) by Lm3;