jgraph_8.miz



    begin

    reserve x,y for set;

    reserve i,j,n for Nat;

    reserve p1,p2 for Point of ( TOP-REAL n);

    reserve a,b,c,d for Real;

    

     Lm1: I[01] = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR: 20, TOPMETR:def 7;

    

     Lm2: for x be set, f be FinSequence st 1 <= ( len f) holds ((f ^ <*x*>) . 1) = (f . 1) & (( <*x*> ^ f) . (( len f) + 1)) = (f . ( len f))

    proof

      let x be set, f be FinSequence;

      assume

       A1: 1 <= ( len f);

      then

       A2: ( len f) in ( dom f) by FINSEQ_3: 25;

      

       A3: (( <*x*> ^ f) . (( len f) + 1)) = (( <*x*> ^ f) . (( len <*x*>) + ( len f))) by FINSEQ_1: 39

      .= (f . ( len f)) by A2, FINSEQ_1:def 7;

      1 in ( dom f) by A1, FINSEQ_3: 25;

      hence thesis by A3, FINSEQ_1:def 7;

    end;

    

     Lm3: for f be FinSequence of REAL st (for k be Nat st 1 <= k & k < ( len f) holds (f /. k) < (f /. (k + 1))) holds f is increasing

    proof

      let f be FinSequence of REAL ;

      assume

       A1: for k be Nat st 1 <= k & k < ( len f) holds (f /. k) < (f /. (k + 1));

      now

        let i, j;

        now

          defpred P[ Nat] means (i + (1 + $1)) <= ( len f) implies (f /. i) < (f /. (i + (1 + $1)));

          assume that

           A2: i in ( dom f) and

           A3: j in ( dom f) and

           A4: i < j;

          

           A5: 1 <= i by A2, FINSEQ_3: 25;

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A7: (i + (1 + k)) <= ( len f) implies (f /. i) < (f /. (i + (1 + k)));

            now

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

              then

               A8: 1 <= ((i + 1) + k) by XXREAL_0: 2;

              

               A9: (i + (1 + (k + 1))) = ((i + (1 + k)) + 1);

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

              then

               A10: (i + (1 + k)) < (i + (1 + (k + 1))) by XREAL_1: 6;

              assume

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

              then (i + (1 + k)) < ( len f) by A10, XXREAL_0: 2;

              then (f /. (i + (1 + k))) < (f /. (i + (1 + (k + 1)))) by A1, A8, A9;

              hence (f /. i) < (f /. (i + (1 + (k + 1)))) by A7, A11, A10, XXREAL_0: 2;

            end;

            hence thesis;

          end;

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

          then (j -' (i + 1)) = (j - (i + 1)) by XREAL_1: 233;

          then

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

          

           A13: (f /. i) = (f . i) by A2, PARTFUN1:def 6;

          

           A14: j <= ( len f) by A3, FINSEQ_3: 25;

          then i < ( len f) by A4, XXREAL_0: 2;

          then

           A15: P[ 0 ] by A1, A5;

          for k be Nat holds P[k] from NAT_1:sch 2( A15, A6);

          then (f /. i) < (f /. j) by A14, A12;

          hence (f . i) < (f . j) by A3, A13, PARTFUN1:def 6;

        end;

        hence i in ( dom f) & j in ( dom f) & i < j implies (f . i) < (f . j);

      end;

      hence thesis by SEQM_3:def 1;

    end;

    registration

      let a, b, c, d;

      cluster ( closed_inside_of_rectangle (a,b,c,d)) -> convex;

      coherence

      proof

        set P = ( closed_inside_of_rectangle (a,b,c,d));

        

         A1: P = { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & c <= (p `2 ) & (p `2 ) <= d } by JGRAPH_6:def 2;

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

        assume w1 in P & w2 in P;

        then

         A2: (ex p3 be Point of ( TOP-REAL 2) st p3 = w1 & a <= (p3 `1 ) & (p3 `1 ) <= b & c <= (p3 `2 ) & (p3 `2 ) <= d) & ex p4 be Point of ( TOP-REAL 2) st p4 = w2 & a <= (p4 `1 ) & (p4 `1 ) <= b & c <= (p4 `2 ) & (p4 `2 ) <= d by A1;

        let x be object;

        assume x in ( LSeg (w1,w2));

        then

        consider l be Real such that

         A3: x = (((1 - l) * w1) + (l * w2)) and

         A4: 0 <= l & l <= 1;

        set w = (((1 - l) * w1) + (l * w2));

        

         A5: w = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )), ((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID: 55;

        

         A6: (l * w2) = |[(l * (w2 `1 )), (l * (w2 `2 ))]| by EUCLID: 57;

        then

         A7: ((l * w2) `2 ) = (l * (w2 `2 )) by EUCLID: 52;

        

         A8: ((1 - l) * w1) = |[((1 - l) * (w1 `1 )), ((1 - l) * (w1 `2 ))]| by EUCLID: 57;

        then (((1 - l) * w1) `2 ) = ((1 - l) * (w1 `2 )) by EUCLID: 52;

        then (w `2 ) = (((1 - l) * (w1 `2 )) + (l * (w2 `2 ))) by A5, A7, EUCLID: 52;

        then

         A9: c <= (w `2 ) & (w `2 ) <= d by A2, A4, XREAL_1: 173, XREAL_1: 174;

        

         A10: ((l * w2) `1 ) = (l * (w2 `1 )) by A6, EUCLID: 52;

        (((1 - l) * w1) `1 ) = ((1 - l) * (w1 `1 )) by A8, EUCLID: 52;

        then (w `1 ) = (((1 - l) * (w1 `1 )) + (l * (w2 `1 ))) by A5, A10, EUCLID: 52;

        then a <= (w `1 ) & (w `1 ) <= b by A2, A4, XREAL_1: 173, XREAL_1: 174;

        hence thesis by A1, A3, A9;

      end;

    end

    registration

      let a, b, c, d;

      cluster ( Trectangle (a,b,c,d)) -> convex;

      coherence by PRE_TOPC: 8;

    end

    theorem :: JGRAPH_8:1

    

     Th1: for e be positive Real, g be continuous Function of I[01] , ( TOP-REAL n) holds ex h be FinSequence of REAL st (h . 1) = 0 & (h . ( len h)) = 1 & 5 <= ( len h) & ( rng h) c= the carrier of I[01] & h is increasing & (for i be Nat, Q be Subset of I[01] , W be Subset of ( Euclid n) st 1 <= i & i < ( len h) & Q = [.(h /. i), (h /. (i + 1)).] & W = (g .: Q) holds ( diameter W) < e)

    proof

      1 in { r where r be Real : 0 <= r & r <= 1 };

      then

       A1: 1 in [. 0 , 1.] by RCOMP_1:def 1;

       {1} c= [. 0 , 1.] by A1, TARSKI:def 1;

      then

       A2: ( [. 0 , 1.] \/ {1}) = [. 0 , 1.] by XBOOLE_1: 12;

      ( Closed-Interval-TSpace ( 0 ,1)) = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR:def 7;

      

      then

       A3: the carrier of I[01] = the carrier of ( Closed-Interval-MSpace ( 0 ,1)) by TOPMETR: 12, TOPMETR: 20

      .= [. 0 , 1.] by TOPMETR: 10;

      let e be positive Real, g be continuous Function of I[01] , ( TOP-REAL n);

      reconsider e as positive Real;

      

       A4: n in NAT by ORDINAL1:def 12;

      then

      reconsider f = g as Function of ( Closed-Interval-MSpace ( 0 ,1)), ( Euclid n) by UNIFORM1: 10;

      

       A5: (e / 2) < e by XREAL_1: 216;

      

       A6: (e / 2) > 0 by XREAL_1: 215;

      f is uniformly_continuous by UNIFORM1: 8, A4;

      then

      consider s1 be Real such that

       A7: 0 < s1 and

       A8: for u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1)) st ( dist (u1,u2)) < s1 holds ( dist ((f /. u1),(f /. u2))) < (e / 2) by A6, UNIFORM1:def 1;

      set s = ( min (s1,(1 / 2)));

      defpred P[ Nat, object] means $2 = ((s / 2) * ($1 - 1));

      

       A9: 0 <= s by A7, XXREAL_0: 20;

      then

      reconsider j = [/(2 / s)\] as Nat by INT_1: 53;

      

       A10: (2 / s) <= j by INT_1:def 7;

      

       A11: s <= s1 by XXREAL_0: 17;

      

       A12: for u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1)) st ( dist (u1,u2)) < s holds ( dist ((f /. u1),(f /. u2))) < (e / 2)

      proof

        let u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1));

        assume ( dist (u1,u2)) < s;

        then ( dist (u1,u2)) < s1 by A11, XXREAL_0: 2;

        hence thesis by A8;

      end;

      

       A13: (2 / s) <= [/(2 / s)\] by INT_1:def 7;

      then ((2 / s) - j) <= 0 by XREAL_1: 47;

      then (1 + ((2 / s) - j)) <= (1 + 0 ) by XREAL_1: 6;

      then

       A14: ((s / 2) * (1 + ((2 / s) - j))) <= ((s / 2) * 1) by A9, XREAL_1: 64;

      

       A15: for k be Nat st k in ( Seg j) holds ex x be object st P[k, x];

      consider p be FinSequence such that

       A16: ( dom p) = ( Seg j) & for k be Nat st k in ( Seg j) holds P[k, (p . k)] from FINSEQ_1:sch 1( A15);

      

       A17: ( Seg ( len p)) = ( Seg j) by A16, FINSEQ_1:def 3;

      ( rng (p ^ <*1*>)) c= REAL

      proof

        let y be object;

        

         A18: ( len (p ^ <*1*>)) = (( len p) + 1) by FINSEQ_2: 16;

        assume y in ( rng (p ^ <*1*>));

        then

        consider x be object such that

         A19: x in ( dom (p ^ <*1*>)) and

         A20: y = ((p ^ <*1*>) . x) by FUNCT_1:def 3;

        reconsider nx = x as Nat by A19;

        

         A21: ( dom (p ^ <*1*>)) = ( Seg ( len (p ^ <*1*>))) by FINSEQ_1:def 3;

        then

         A22: 1 <= nx by A19, FINSEQ_1: 1;

        

         A23: 1 <= nx by A19, A21, FINSEQ_1: 1;

        

         A24: nx <= ( len (p ^ <*1*>)) by A19, A21, FINSEQ_1: 1;

        per cases ;

          suppose nx < (( len p) + 1);

          then

           A25: nx <= ( len p) by NAT_1: 13;

          then nx in ( Seg j) by A17, A23, FINSEQ_1: 1;

          then

           A26: (p . nx) = ((s / 2) * (nx - 1)) by A16;

          y = (p . nx) by A20, A22, A25, FINSEQ_1: 64;

          hence thesis by A26, XREAL_0:def 1;

        end;

          suppose nx >= (( len p) + 1);

          then nx = (( len p) + 1) by A24, A18, XXREAL_0: 1;

          then

           A27: y = 1 by A20, FINSEQ_1: 42;

          1 in REAL by XREAL_0:def 1;

          hence thesis by A27;

        end;

      end;

      then

      reconsider h1 = (p ^ <*1*>) as FinSequence of REAL by FINSEQ_1:def 4;

      

       A28: ( len h1) = (( len p) + 1) by FINSEQ_2: 16;

      j in NAT by ORDINAL1:def 12;

      then

       A29: ( len p) = j by A16, FINSEQ_1:def 3;

      

       A30: s <> 0 by A7, XXREAL_0: 15;

      then (2 / s) >= (2 / (1 / 2)) by A9, XREAL_1: 118, XXREAL_0: 17;

      then 4 <= j by A10, XXREAL_0: 2;

      then

       A31: (4 + 1) <= (( len p) + 1) by A29, XREAL_1: 6;

      

       A32: (s / 2) > 0 by A9, A30, XREAL_1: 215;

      

       A33: for i be Nat, r1,r2 be Real st 1 <= i & i < ( len p) & r1 = (p . i) & r2 = (p . (i + 1)) holds r1 < r2 & (r2 - r1) = (s / 2)

      proof

        let i be Nat, r1,r2 be Real;

        assume that

         A34: 1 <= i & i < ( len p) and

         A35: r1 = (p . i) and

         A36: r2 = (p . (i + 1));

        1 < (i + 1) & (i + 1) <= ( len p) by A34, NAT_1: 13;

        then (i + 1) in ( Seg j) by A17, FINSEQ_1: 1;

        then

         A37: r2 = ((s / 2) * ((i + 1) - 1)) by A16, A36;

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

        then

         A38: (i - 1) < ((i + 1) - 1) by XREAL_1: 9;

        

         A39: i in ( Seg j) by A17, A34, FINSEQ_1: 1;

        then r1 = ((s / 2) * (i - 1)) by A16, A35;

        hence r1 < r2 by A32, A37, A38, XREAL_1: 68;

        (r2 - r1) = (((s / 2) * i) - ((s / 2) * (i - 1))) by A16, A35, A39, A37;

        hence thesis;

      end;

       0 < s by A7, A30, XXREAL_0: 20;

      then 0 < j by A13, XREAL_1: 139;

      then

       A40: ( 0 + 1) <= j by NAT_1: 13;

      then 1 in ( Seg j) by FINSEQ_1: 1;

      

      then (p . 1) = ((s / 2) * (1 - 1)) by A16

      .= 0 ;

      then

       A41: (h1 . 1) = 0 by A40, A29, Lm2;

      (2 * s) <> 0 by A7, XXREAL_0: 15;

      then

       A42: ((s / 2) * (2 / s)) = ((2 * s) / (2 * s)) & ((2 * s) / (2 * s)) = 1 by XCMPLX_1: 60, XCMPLX_1: 76;

      then

       A43: (1 - ((s / 2) * (j - 1))) = ((s / 2) * (1 + ((2 / s) - [/(2 / s)\])));

      

       A44: for r1 be Real st r1 = (p . ( len p)) holds (1 - r1) <= (s / 2) by A40, A29, FINSEQ_1: 1, A14, A16, A43;

      

       A45: for i be Nat st 1 <= i & i < ( len h1) holds ((h1 /. (i + 1)) - (h1 /. i)) <= (s / 2)

      proof

        let i be Nat;

        assume that

         A46: 1 <= i and

         A47: i < ( len h1);

        

         A48: (i + 1) <= ( len h1) by A47, NAT_1: 13;

        

         A49: i <= ( len p) by A28, A47, NAT_1: 13;

        

         A50: 1 < (i + 1) by A46, NAT_1: 13;

        per cases ;

          suppose

           A51: i < ( len p);

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

          then

           A52: (h1 . (i + 1)) = (p . (i + 1)) by A50, FINSEQ_1: 64;

          

           A53: (h1 . i) = (p . i) by A46, A51, FINSEQ_1: 64;

          (h1 . i) = (h1 /. i) & (h1 . (i + 1)) = (h1 /. (i + 1)) by A46, A47, A48, A50, FINSEQ_4: 15;

          hence thesis by A33, A46, A51, A53, A52;

        end;

          suppose i >= ( len p);

          then

           A54: i = ( len p) by A49, XXREAL_0: 1;

          

           A55: (h1 /. i) = (h1 . i) by A46, A47, FINSEQ_4: 15

          .= (p . i) by A46, A49, FINSEQ_1: 64;

          (h1 /. (i + 1)) = (h1 . (i + 1)) by A48, A50, FINSEQ_4: 15

          .= 1 by A54, FINSEQ_1: 42;

          hence thesis by A44, A54, A55;

        end;

      end;

       [/(2 / s)\] < ((2 / s) + 1) by INT_1:def 7;

      then ( [/(2 / s)\] - 1) < (((2 / s) + 1) - 1) by XREAL_1: 9;

      then

       A56: ((s / 2) * (j - 1)) < ((s / 2) * (2 / s)) by A32, XREAL_1: 68;

      

       A57: for i be Nat, r1 be Real st 1 <= i & i <= ( len p) & r1 = (p . i) holds r1 < 1

      proof

        let i be Nat, r1 be Real;

        assume that

         A58: 1 <= i and

         A59: i <= ( len p) and

         A60: r1 = (p . i);

        (i - 1) <= (j - 1) by A29, A59, XREAL_1: 9;

        then

         A61: ((s / 2) * (i - 1)) <= ((s / 2) * (j - 1)) by A9, XREAL_1: 64;

        i in ( Seg j) by A17, A58, A59, FINSEQ_1: 1;

        then r1 = ((s / 2) * (i - 1)) by A16, A60;

        hence thesis by A56, A42, A61, XXREAL_0: 2;

      end;

      

       A62: for i be Nat st 1 <= i & i < ( len h1) holds (h1 /. i) < (h1 /. (i + 1))

      proof

        let i be Nat;

        assume that

         A63: 1 <= i and

         A64: i < ( len h1);

        

         A65: (i + 1) <= ( len h1) by A64, NAT_1: 13;

        

         A66: 1 < (i + 1) by A63, NAT_1: 13;

        

         A67: i <= ( len p) by A28, A64, NAT_1: 13;

        per cases ;

          suppose

           A68: i < ( len p);

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

          then

           A69: (h1 . (i + 1)) = (p . (i + 1)) by A66, FINSEQ_1: 64;

          

           A70: (h1 . i) = (p . i) by A63, A68, FINSEQ_1: 64;

          (h1 . i) = (h1 /. i) & (h1 . (i + 1)) = (h1 /. (i + 1)) by A63, A64, A65, A66, FINSEQ_4: 15;

          hence thesis by A33, A63, A68, A70, A69;

        end;

          suppose i >= ( len p);

          then

           A71: i = ( len p) by A67, XXREAL_0: 1;

          

           A72: (h1 /. (i + 1)) = (h1 . (i + 1)) by A65, A66, FINSEQ_4: 15

          .= 1 by A71, FINSEQ_1: 42;

          (h1 /. i) = (h1 . i) by A63, A64, FINSEQ_4: 15

          .= (p . i) by A63, A67, FINSEQ_1: 64;

          hence thesis by A57, A63, A67, A72;

        end;

      end;

      

       A73: ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

      

       A74: for i be Nat, Q be Subset of I[01] , W be Subset of ( Euclid n) st 1 <= i & i < ( len h1) & Q = [.(h1 /. i), (h1 /. (i + 1)).] & W = (g .: Q) holds ( diameter W) < e

      proof

        let i be Nat, Q be Subset of I[01] , W be Subset of ( Euclid n);

        assume that

         A75: 1 <= i & i < ( len h1) and

         A76: Q = [.(h1 /. i), (h1 /. (i + 1)).] and

         A77: W = (g .: Q);

        (h1 /. i) < (h1 /. (i + 1)) by A62, A75;

        then

         A78: Q <> {} by A76, XXREAL_1: 1;

        

         A79: for x,y be Point of ( Euclid n) st x in W & y in W holds ( dist (x,y)) <= (e / 2)

        proof

          let x,y be Point of ( Euclid n);

          assume that

           A80: x in W and

           A81: y in W;

          consider x3 be object such that

           A82: x3 in ( dom g) and

           A83: x3 in Q and

           A84: x = (g . x3) by A77, A80, FUNCT_1:def 6;

          reconsider x3 as Element of ( Closed-Interval-MSpace ( 0 ,1)) by A82, Lm1, TOPMETR: 12;

          reconsider r3 = x3 as Real by A83;

          

           A85: ((h1 /. (i + 1)) - (h1 /. i)) <= (s / 2) by A45, A75;

          consider y3 be object such that

           A86: y3 in ( dom g) and

           A87: y3 in Q and

           A88: y = (g . y3) by A77, A81, FUNCT_1:def 6;

          reconsider y3 as Element of ( Closed-Interval-MSpace ( 0 ,1)) by A86, Lm1, TOPMETR: 12;

          reconsider s3 = y3 as Real by A87;

          

           A89: (f . x3) = (f /. x3) & (f . y3) = (f /. y3);

           |.(r3 - s3).| <= ((h1 /. (i + 1)) - (h1 /. i)) by A76, A83, A87, UNIFORM1: 12;

          then |.(r3 - s3).| <= (s / 2) by A85, XXREAL_0: 2;

          then

           A90: ( dist (x3,y3)) <= (s / 2) by HEINE: 1;

          (s / 2) < s by A9, A30, XREAL_1: 216;

          then ( dist (x3,y3)) < s by A90, XXREAL_0: 2;

          hence thesis by A12, A84, A88, A89;

        end;

        then W is bounded by A6, TBSP_1:def 7;

        then ( diameter W) <= (e / 2) by A73, A77, A78, A79, TBSP_1:def 8;

        hence thesis by A5, XXREAL_0: 2;

      end;

      

       A91: ( rng p) c= [. 0 , 1.]

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A92: x in ( dom p) and

         A93: y = (p . x) by FUNCT_1:def 3;

        reconsider nx = x as Nat by A92;

        

         A94: (p . nx) = ((s / 2) * (nx - 1)) by A16, A92;

        then

        reconsider ry = (p . nx) as Real;

        

         A95: x in ( Seg ( len p)) by A92, FINSEQ_1:def 3;

        then

         A96: 1 <= nx by FINSEQ_1: 1;

        then

         A97: (nx - 1) >= (1 - 1) by XREAL_1: 9;

        nx <= ( len p) by A95, FINSEQ_1: 1;

        then ry < 1 by A57, A96;

        then y in { rs where rs be Real : 0 <= rs & rs <= 1 } by A9, A93, A94, A97;

        hence thesis by RCOMP_1:def 1;

      end;

      ( rng <*1*>) = {1} by FINSEQ_1: 38;

      then ( rng h1) = (( rng p) \/ {1}) by FINSEQ_1: 31;

      then

       A98: ( rng h1) c= ( [. 0 , 1.] \/ {1}) by A91, XBOOLE_1: 13;

      (h1 . ( len h1)) = 1 by A28, FINSEQ_1: 42;

      hence thesis by A28, A31, A41, A2, A98, A3, A62, A74, Lm3;

    end;

    theorem :: JGRAPH_8:2

    

     Th2: for P be Subset of ( TOP-REAL n) st P c= ( LSeg (p1,p2)) & p1 in P & p2 in P & P is connected holds P = ( LSeg (p1,p2))

    proof

      let P be Subset of ( TOP-REAL n);

      assume that

       A1: P c= ( LSeg (p1,p2)) and

       A2: p1 in P and

       A3: p2 in P and

       A4: P is connected;

      reconsider L = ( LSeg (p1,p2)) as non empty Subset of ( TOP-REAL n) by A1, A2;

      now

        

         A5: the carrier of (( TOP-REAL n) | L) = ( [#] (( TOP-REAL n) | L))

        .= L by PRE_TOPC:def 5;

        then

        reconsider PX = P as Subset of (( TOP-REAL n) | L) by A1;

        assume not ( LSeg (p1,p2)) c= P;

        then

        consider x0 be object such that

         A6: x0 in ( LSeg (p1,p2)) and

         A7: not x0 in P;

        reconsider p0 = x0 as Point of ( TOP-REAL n) by A6;

        

         A8: (( LSeg (p0,p2)) \ {p0}) c= ( LSeg (p0,p2)) by XBOOLE_1: 36;

        

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

        then

        reconsider PX1 = ( LSeg (p1,p0)) as Subset of (( TOP-REAL n) | L) by A6, A5, TOPREAL1: 6;

        

         A10: (( LSeg (p1,p0)) \ {p0}) c= ( LSeg (p1,p0)) by XBOOLE_1: 36;

        ( LSeg (p1,p0)) c= L by A6, A9, TOPREAL1: 6;

        then

        reconsider R1 = (( LSeg (p1,p0)) \ {p0}) as Subset of (( TOP-REAL n) | L) by A10, A5, XBOOLE_1: 1;

        

         A11: (( TOP-REAL n) | L) is T_2 by TOPMETR: 2;

        

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

        then ( LSeg (p0,p2)) c= L by A6, TOPREAL1: 6;

        then

        reconsider R2 = (( LSeg (p0,p2)) \ {p0}) as Subset of (( TOP-REAL n) | L) by A5, A8, XBOOLE_1: 1;

        reconsider PX2 = ( LSeg (p0,p2)) as Subset of (( TOP-REAL n) | L) by A6, A5, A12, TOPREAL1: 6;

        

         A13: (PX1 /\ PX2) = {p0} by A6, TOPREAL1: 8;

        

         A14: R1 c= PX1 by XBOOLE_1: 36;

         A15:

        now

          assume P c= R1;

          then

           A16: p2 in R1 by A3;

          p2 in PX2 by RLTOPSP1: 68;

          then p2 in (PX1 /\ PX2) by A14, A16, XBOOLE_0:def 4;

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

        end;

        

         A17: {p0} c= ( LSeg (p1,p0))

        proof

          let d be object;

          assume d in {p0};

          then d = p0 by TARSKI:def 1;

          hence thesis by RLTOPSP1: 68;

        end;

        

         A18: {p0} c= ( LSeg (p0,p2))

        proof

          let d be object;

          assume d in {p0};

          then d = p0 by TARSKI:def 1;

          hence thesis by RLTOPSP1: 68;

        end;

        PX2 is compact by COMPTS_1: 19;

        then PX2 is closed by A11, COMPTS_1: 7;

        then

         A19: ( Cl PX2) = PX2 by PRE_TOPC: 22;

        

         A20: ( Cl R2) c= ( Cl PX2) by PRE_TOPC: 19, XBOOLE_1: 36;

        (R1 /\ PX2) = ((PX1 /\ PX2) \ {p0}) by XBOOLE_1: 49

        .= {} by A13, XBOOLE_1: 37;

        then (R1 /\ ( Cl R2)) = {} by A19, A20, XBOOLE_1: 3, XBOOLE_1: 27;

        then

         A21: R1 misses ( Cl R2);

        

         A22: (PX1 /\ PX2) = {p0} by A6, TOPREAL1: 8;

        

         A23: R2 c= PX2 by XBOOLE_1: 36;

         A24:

        now

          assume P c= R2;

          then

           A25: p1 in R2 by A2;

          p1 in PX1 by RLTOPSP1: 68;

          then p1 in (PX1 /\ PX2) by A23, A25, XBOOLE_0:def 4;

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

        end;

        PX1 is compact by COMPTS_1: 19;

        then PX1 is closed by A11, COMPTS_1: 7;

        then

         A26: ( Cl PX1) = PX1 by PRE_TOPC: 22;

        

         A27: L = (( LSeg (p1,p0)) \/ ( LSeg (p0,p2))) by A6, TOPREAL1: 5

        .= (((( LSeg (p1,p0)) \ {p0}) \/ {p0}) \/ ( LSeg (p0,p2))) by A17, XBOOLE_1: 45

        .= ((( LSeg (p1,p0)) \ {p0}) \/ ( {p0} \/ ( LSeg (p0,p2)))) by XBOOLE_1: 4

        .= (R1 \/ PX2) by A18, XBOOLE_1: 12

        .= (R1 \/ ((PX2 \ {p0}) \/ {p0})) by A18, XBOOLE_1: 45

        .= ((R1 \/ {p0}) \/ R2) by XBOOLE_1: 4;

        

         A28: P c= (R1 \/ R2)

        proof

          let z be object;

          assume

           A29: z in P;

          then z in (R1 \/ {p0}) or z in R2 by A1, A27, XBOOLE_0:def 3;

          then z in R1 or z in {p0} or z in R2 by XBOOLE_0:def 3;

          hence thesis by A7, A29, TARSKI:def 1, XBOOLE_0:def 3;

        end;

        

         A30: ( Cl R1) c= ( Cl PX1) by PRE_TOPC: 19, XBOOLE_1: 36;

        (PX1 /\ R2) = ((PX1 /\ PX2) \ {p0}) by XBOOLE_1: 49

        .= {} by A22, XBOOLE_1: 37;

        then (( Cl R1) /\ R2) = {} by A26, A30, XBOOLE_1: 3, XBOOLE_1: 27;

        then ( Cl R1) misses R2;

        then

         A31: (R1,R2) are_separated by A21, CONNSP_1:def 1;

        PX is connected by A4, CONNSP_1: 46;

        hence contradiction by A31, A28, A15, A24, CONNSP_1: 16;

      end;

      hence thesis by A1;

    end;

    theorem :: JGRAPH_8:3

    

     Th3: for g be Path of p1, p2 st ( rng g) c= ( LSeg (p1,p2)) holds ( rng g) = ( LSeg (p1,p2))

    proof

      let g be Path of p1, p2;

      assume

       A1: ( rng g) c= ( LSeg (p1,p2));

      

       A2: p2 = (g . 1) by BORSUK_2:def 4;

      

       A3: p1 = (g . 0 ) by BORSUK_2:def 4;

      now

        

         A4: (g .: ( [#] I[01] )) c= ( rng g)

        proof

          let y be object;

          assume y in (g .: ( [#] I[01] ));

          then ex x be object st x in ( dom g) & x in ( [#] I[01] ) & y = (g . x) by FUNCT_1:def 6;

          hence thesis by FUNCT_1:def 3;

        end;

        1 in the carrier of I[01] by BORSUK_1: 43;

        then 1 in ( dom g) by FUNCT_2:def 1;

        then

         A5: p2 in (g .: ( [#] I[01] )) by A2, FUNCT_1:def 6;

         0 in the carrier of I[01] by BORSUK_1: 43;

        then 0 in ( dom g) by FUNCT_2:def 1;

        then

         A6: p1 in (g .: ( [#] I[01] )) by A3, FUNCT_1:def 6;

        ( [#] I[01] ) is connected by CONNSP_1: 27;

        then

         A7: (g .: ( [#] I[01] )) is connected by TOPS_2: 61;

        assume not ( LSeg (p1,p2)) c= ( rng g);

        hence contradiction by A1, A7, A6, A5, A4, Th2, XBOOLE_1: 1;

      end;

      hence thesis by A1;

    end;

    theorem :: JGRAPH_8:4

    

     Th4: for P,Q be non empty Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2), f be Path of p1, p2, g be Path of q1, q2 st ( rng f) = P & ( rng g) = Q & (for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )) & (for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )) & (for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )) & (for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )) holds P meets Q

    proof

      

       A1: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

      

       A2: ( [#] I[01] ) is compact by COMPTS_1: 1;

      let P,Q be non empty Subset of ( TOP-REAL 2), p1,p2,q1,q2 be Point of ( TOP-REAL 2), f be Path of p1, p2, g be Path of q1, q2;

      assume that

       A3: ( rng f) = P and

       A4: ( rng g) = Q and

       A5: for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 ) and

       A6: for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 ) and

       A7: for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 ) and

       A8: for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 );

      ( TopSpaceMetr ( Euclid 2)) = the TopStruct of ( TOP-REAL 2) by EUCLID:def 8;

      then

      reconsider P9 = P, Q9 = Q as Subset of ( TopSpaceMetr ( Euclid 2));

      set e = (( min_dist_min (P9,Q9)) / 5);

      (f .: the carrier of I[01] ) = ( rng f) by RELSET_1: 22;

      then P is compact by A3, A2, WEIERSTR: 8;

      then

       A9: P9 is compact by A1, COMPTS_1: 23;

      (g .: ( [#] I[01] )) = ( rng g) by RELSET_1: 22;

      then Q is compact by A4, A2, WEIERSTR: 8;

      then

       A10: Q9 is compact by A1, COMPTS_1: 23;

      assume

       A11: (P /\ Q) = {} ;

      then P misses Q;

      then

       A12: ( min_dist_min (P9,Q9)) > 0 by A10, A9, JGRAPH_1: 38;

      then

       A13: e > ( 0 / 5) by XREAL_1: 74;

      then

      consider h be FinSequence of REAL such that

       A14: (h . 1) = 0 and

       A15: (h . ( len h)) = 1 and

       A16: 5 <= ( len h) and

       A17: ( rng h) c= the carrier of I[01] and

       A18: h is increasing and

       A19: for i be Nat, R be Subset of I[01] , W be Subset of ( Euclid 2) st 1 <= i & i < ( len h) & R = [.(h /. i), (h /. (i + 1)).] & W = (f .: R) holds ( diameter W) < e by Th1;

      deffunc F( Nat) = (f . (h . $1));

      ex h19 be FinSequence st ( len h19) = ( len h) & for i be Nat st i in ( dom h19) holds (h19 . i) = F(i) from FINSEQ_1:sch 2;

      then

      consider h19 be FinSequence such that

       A20: ( len h19) = ( len h) and

       A21: for i be Nat st i in ( dom h19) holds (h19 . i) = (f . (h . i));

      

       A22: 1 <= ( len h) by A16, XXREAL_0: 2;

      then

       A23: ( len h) in ( dom h19) by A20, FINSEQ_3: 25;

      ( rng h19) c= the carrier of ( TOP-REAL 2)

      proof

        let y be object;

        

         A24: ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

        assume y in ( rng h19);

        then

        consider x be object such that

         A25: x in ( dom h19) and

         A26: y = (h19 . x) by FUNCT_1:def 3;

        reconsider i = x as Nat by A25;

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

        then i in ( dom h) by A20, A25, FINSEQ_1:def 3;

        then

         A27: (h . i) in ( rng h) by FUNCT_1:def 3;

        (h19 . i) = (f . (h . i)) by A21, A25;

        then (h19 . i) in ( rng f) by A17, A27, A24, FUNCT_1:def 3;

        hence thesis by A26;

      end;

      then

      reconsider h1 = h19 as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A28: ( len h1) >= 1 by A16, A20, XXREAL_0: 2;

      then

       A29: (h1 . 1) = (h1 /. 1) by FINSEQ_4: 15;

      

       A30: (f . 0 ) = p1 by BORSUK_2:def 4;

      

       A31: for i st 1 <= i & (i + 1) <= ( len h1) holds |.((h1 /. i) - (h1 /. (i + 1))).| < e

      proof

        reconsider Pa = P as Subset of ( TOP-REAL 2);

        

         A32: ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

        reconsider W1 = P as Subset of ( Euclid 2) by TOPREAL3: 8;

        let i;

        assume that

         A33: 1 <= i and

         A34: (i + 1) <= ( len h1);

        

         A35: 1 < (i + 1) by A33, NAT_1: 13;

        then

         A36: (h . (i + 1)) = (h /. (i + 1)) by A20, A34, FINSEQ_4: 15;

        

         A37: (i + 1) in ( dom h19) by A34, A35, FINSEQ_3: 25;

        then

         A38: (h19 . (i + 1)) = (f . (h . (i + 1))) by A21;

        then

         A39: (h1 /. (i + 1)) = (f . (h . (i + 1))) by A34, A35, FINSEQ_4: 15;

        set r1 = (((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) + 1);

        ( [#] I[01] ) is compact & (f .: the carrier of I[01] ) = ( rng f) by COMPTS_1: 1, RELSET_1: 22;

        then

         A40: Pa is compact by A3, WEIERSTR: 8;

        

         A41: for x,y be Point of ( Euclid 2) st x in W1 & y in W1 holds ( dist (x,y)) <= r1

        proof

          let x,y be Point of ( Euclid 2);

          assume that

           A42: x in W1 and

           A43: y in W1;

          reconsider pw1 = x, pw2 = y as Point of ( TOP-REAL 2) by A42, A43;

          

           A44: ( S-bound Pa) <= (pw2 `2 ) & (pw2 `2 ) <= ( N-bound Pa) by A40, A43, PSCOMP_1: 24;

          ( S-bound Pa) <= (pw1 `2 ) & (pw1 `2 ) <= ( N-bound Pa) by A40, A42, PSCOMP_1: 24;

          then

           A45: |.((pw1 `2 ) - (pw2 `2 )).| <= (( N-bound Pa) - ( S-bound Pa)) by A44, JGRAPH_1: 27;

          

           A46: ((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) <= (((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) + 1) by XREAL_1: 29;

          

           A47: ( W-bound Pa) <= (pw2 `1 ) & (pw2 `1 ) <= ( E-bound Pa) by A40, A43, PSCOMP_1: 24;

          ( W-bound Pa) <= (pw1 `1 ) & (pw1 `1 ) <= ( E-bound Pa) by A40, A42, PSCOMP_1: 24;

          then |.((pw1 `1 ) - (pw2 `1 )).| <= (( E-bound Pa) - ( W-bound Pa)) by A47, JGRAPH_1: 27;

          then ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= ((( E-bound Pa) - ( W-bound Pa)) + (( N-bound Pa) - ( S-bound Pa))) by A45, XREAL_1: 7;

          then

           A48: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= r1 by A46, XXREAL_0: 2;

          ( dist (x,y)) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) by JGRAPH_1: 28, JGRAPH_1: 32;

          hence thesis by A48, XXREAL_0: 2;

        end;

        (i + 1) in ( dom h) by A20, A34, A35, FINSEQ_3: 25;

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

        then (h19 . (i + 1)) in ( rng f) by A17, A38, A32, FUNCT_1:def 3;

        then

         A49: (f . (h . (i + 1))) is Element of ( TOP-REAL 2) by A21, A37;

        

         A50: i < ( len h1) by A34, NAT_1: 13;

        then

         A51: (h . i) = (h /. i) by A20, A33, FINSEQ_4: 15;

        

         A52: i in ( dom h) by A20, A33, A50, FINSEQ_3: 25;

        then

         A53: (h . i) in ( rng h) by FUNCT_1:def 3;

        

         A54: (i + 1) in ( dom h) by A20, A34, A35, FINSEQ_3: 25;

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

        then

        reconsider R = [.(h /. i), (h /. (i + 1)).] as Subset of I[01] by A17, A53, A51, A36, BORSUK_1: 40, XXREAL_2:def 12;

        

         A55: i in ( dom h19) by A33, A50, FINSEQ_3: 25;

        then

         A56: (h19 . i) = (f . (h . i)) by A21;

        then (h19 . i) in ( rng f) by A17, A53, A32, FUNCT_1:def 3;

        then (f . (h . i)) is Element of ( TOP-REAL 2) by A21, A55;

        then

        reconsider w1 = (f . (h . i)), w2 = (f . (h . (i + 1))) as Point of ( Euclid 2) by A49, TOPREAL3: 8;

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

        then

         A57: (h /. i) <= (h /. (i + 1)) by A18, A52, A51, A54, A36, SEQM_3:def 1;

        then (h . i) in R by A51, XXREAL_1: 1;

        then

         A58: w1 in (f .: R) by A32, FUNCT_1:def 6;

         0 in the carrier of I[01] by BORSUK_1: 43;

        then

         A59: (f . 0 ) in ( rng f) by A32, FUNCT_1:def 3;

        then ( S-bound Pa) <= (p1 `2 ) & (p1 `2 ) <= ( N-bound Pa) by A3, A30, A40, PSCOMP_1: 24;

        then ( S-bound Pa) <= ( N-bound Pa) by XXREAL_0: 2;

        then

         A60: 0 <= (( N-bound Pa) - ( S-bound Pa)) by XREAL_1: 48;

        ( W-bound Pa) <= (p1 `1 ) & (p1 `1 ) <= ( E-bound Pa) by A3, A30, A40, A59, PSCOMP_1: 24;

        then ( W-bound Pa) <= ( E-bound Pa) by XXREAL_0: 2;

        then 0 <= (( E-bound Pa) - ( W-bound Pa)) by XREAL_1: 48;

        then

         A61: W1 is bounded by A60, A41, TBSP_1:def 7;

        (h . (i + 1)) in R by A36, A57, XXREAL_1: 1;

        then

         A62: w2 in (f .: R) by A32, FUNCT_1:def 6;

        reconsider W = (f .: R) as Subset of ( Euclid 2) by TOPREAL3: 8;

        ( dom f) = ( [#] I[01] ) by FUNCT_2:def 1;

        then P = (f .: [. 0 , 1.]) by A3, BORSUK_1: 40, RELAT_1: 113;

        then W is bounded by A61, BORSUK_1: 40, RELAT_1: 123, TBSP_1: 14;

        then

         A63: ( dist (w1,w2)) <= ( diameter W) by A58, A62, TBSP_1:def 8;

        ( diameter W) < e by A19, A20, A33, A50;

        then

         A64: ( dist (w1,w2)) < e by A63, XXREAL_0: 2;

        (h1 /. i) = (f . (h . i)) by A33, A50, A56, FINSEQ_4: 15;

        hence thesis by A39, A64, JGRAPH_1: 28;

      end;

      

       A65: for i st i in ( dom h1) holds (q1 `2 ) <= ((h1 /. i) `2 ) & ((h1 /. i) `2 ) <= (q2 `2 )

      proof

        let i;

        assume

         A66: i in ( dom h1);

        then (h1 . i) = (f . (h . i)) by A21;

        then

         A67: (h1 /. i) = (f . (h . i)) by A66, PARTFUN1:def 6;

        i in ( dom h) by A20, A66, FINSEQ_3: 29;

        then

         A68: (h . i) in ( rng h) by FUNCT_1:def 3;

        ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

        then (h1 /. i) in ( rng f) by A17, A67, A68, FUNCT_1:def 3;

        hence thesis by A3, A7;

      end;

      for i st i in ( dom ( Y_axis h1)) holds (q1 `2 ) <= (( Y_axis h1) . i) & (( Y_axis h1) . i) <= (q2 `2 )

      proof

        let i;

        assume i in ( dom ( Y_axis h1));

        then i in ( Seg ( len ( Y_axis h1))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h1)) by A28, JGRAPH_1: 42;

        then

         A69: i in ( dom h1) by FINSEQ_1:def 3;

        then (( Y_axis h1) . i) = ((h1 /. i) `2 ) by JGRAPH_1: 43;

        hence thesis by A65, A69;

      end;

      then

       A70: ( Y_axis h1) lies_between ((q1 `2 ),(q2 `2 )) by GOBOARD4:def 2;

      

       A71: (f . 1) = p2 by BORSUK_2:def 4;

      

       A72: for i st i in ( dom h1) holds ((h1 /. 1) `1 ) <= ((h1 /. i) `1 ) & ((h1 /. i) `1 ) <= ((h1 /. ( len h1)) `1 )

      proof

        ( len h) in ( dom h19) by A20, A28, FINSEQ_3: 25;

        then (h1 . ( len h1)) = (f . (h . ( len h))) by A20, A21;

        then

         A73: (h1 /. ( len h1)) = (f . (h . ( len h))) by A28, FINSEQ_4: 15;

        1 in ( dom h19) by A28, FINSEQ_3: 25;

        then (h1 . 1) = (f . (h . 1)) by A21;

        then

         A74: (h1 /. 1) = (f . (h . 1)) by A28, FINSEQ_4: 15;

        let i;

        assume

         A75: i in ( dom h1);

        then (h1 . i) = (f . (h . i)) by A21;

        then

         A76: (h1 /. i) = (f . (h . i)) by A75, PARTFUN1:def 6;

        i in ( dom h) by A20, A75, FINSEQ_3: 29;

        then

         A77: (h . i) in ( rng h) by FUNCT_1:def 3;

        ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

        then (h1 /. i) in ( rng f) by A17, A76, A77, FUNCT_1:def 3;

        hence thesis by A3, A5, A30, A71, A14, A15, A74, A73;

      end;

      for i st i in ( dom ( X_axis h1)) holds (( X_axis h1) . 1) <= (( X_axis h1) . i) & (( X_axis h1) . i) <= (( X_axis h1) . ( len h1))

      proof

        let i;

        

         A78: (( X_axis h1) . 1) = ((h1 /. 1) `1 ) & (( X_axis h1) . ( len h1)) = ((h1 /. ( len h1)) `1 ) by A28, JGRAPH_1: 41;

        assume i in ( dom ( X_axis h1));

        then i in ( Seg ( len ( X_axis h1))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h1)) by A28, JGRAPH_1: 41;

        then

         A79: i in ( dom h1) by FINSEQ_1:def 3;

        then (( X_axis h1) . i) = ((h1 /. i) `1 ) by JGRAPH_1: 43;

        hence thesis by A72, A79, A78;

      end;

      then ( X_axis h1) lies_between ((( X_axis h1) . 1),(( X_axis h1) . ( len h1))) by GOBOARD4:def 2;

      then

      consider f2 be FinSequence of ( TOP-REAL 2) such that

       A80: f2 is special and

       A81: (f2 . 1) = (h1 . 1) and

       A82: (f2 . ( len f2)) = (h1 . ( len h1)) and

       A83: ( len f2) >= ( len h1) and

       A84: ( X_axis f2) lies_between ((( X_axis h1) . 1),(( X_axis h1) . ( len h1))) & ( Y_axis f2) lies_between ((q1 `2 ),(q2 `2 )) and

       A85: for j st j in ( dom f2) holds ex k be Nat st k in ( dom h1) & |.((f2 /. j) - (h1 /. k)).| < e and

       A86: for j st 1 <= j & (j + 1) <= ( len f2) holds |.((f2 /. j) - (f2 /. (j + 1))).| < e by A13, A31, A28, A70, JGRAPH_1: 39;

      

       A87: ( len f2) >= 1 by A28, A83, XXREAL_0: 2;

      then

       A88: (f2 . ( len f2)) = (f2 /. ( len f2)) by FINSEQ_4: 15;

      consider hb be FinSequence of REAL such that

       A89: (hb . 1) = 0 and

       A90: (hb . ( len hb)) = 1 and

       A91: 5 <= ( len hb) and

       A92: ( rng hb) c= the carrier of I[01] and

       A93: hb is increasing and

       A94: for i be Nat, R be Subset of I[01] , W be Subset of ( Euclid 2) st 1 <= i & i < ( len hb) & R = [.(hb /. i), (hb /. (i + 1)).] & W = (g .: R) holds ( diameter W) < e by A13, Th1;

      deffunc F( Nat) = (g . (hb . $1));

      ex h29 be FinSequence st ( len h29) = ( len hb) & for i be Nat st i in ( dom h29) holds (h29 . i) = F(i) from FINSEQ_1:sch 2;

      then

      consider h29 be FinSequence such that

       A95: ( len h29) = ( len hb) and

       A96: for i be Nat st i in ( dom h29) holds (h29 . i) = (g . (hb . i));

      ( rng h29) c= the carrier of ( TOP-REAL 2)

      proof

        let y be object;

        

         A97: ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

        assume y in ( rng h29);

        then

        consider x be object such that

         A98: x in ( dom h29) and

         A99: y = (h29 . x) by FUNCT_1:def 3;

        reconsider i = x as Nat by A98;

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

        then i in ( dom hb) by A95, A98, FINSEQ_1:def 3;

        then

         A100: (hb . i) in ( rng hb) by FUNCT_1:def 3;

        (h29 . i) = (g . (hb . i)) by A96, A98;

        then (h29 . i) in ( rng g) by A92, A100, A97, FUNCT_1:def 3;

        hence thesis by A99;

      end;

      then

      reconsider h2 = h29 as FinSequence of ( TOP-REAL 2) by FINSEQ_1:def 4;

      

       A101: ( len h2) >= 1 by A91, A95, XXREAL_0: 2;

      1 in ( dom h19) by A20, A22, FINSEQ_3: 25;

      then

       A102: (h1 /. 1) = (f . (h . 1)) by A21, A29;

      

       A103: 0 in the carrier of I[01] by BORSUK_1: 43;

      then 0 in ( dom f) by FUNCT_2:def 1;

      then

       A104: p1 in P9 by A3, A30, FUNCT_1:def 3;

      

       A105: 1 <= ( len hb) by A91, XXREAL_0: 2;

      then

       A106: (h2 . ( len h2)) = (h2 /. ( len h2)) by A95, FINSEQ_4: 15;

      

       A107: (g . 0 ) = q1 by BORSUK_2:def 4;

      

       A108: for i st 1 <= i & (i + 1) <= ( len h2) holds |.((h2 /. i) - (h2 /. (i + 1))).| < e

      proof

        reconsider Qa = Q as Subset of ( TOP-REAL 2);

        

         A109: ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

        reconsider W1 = Q as Subset of ( Euclid 2) by TOPREAL3: 8;

        let i;

        assume that

         A110: 1 <= i and

         A111: (i + 1) <= ( len h2);

        

         A112: i < ( len h2) by A111, NAT_1: 13;

        then

         A113: (hb . i) = (hb /. i) by A95, A110, FINSEQ_4: 15;

        

         A114: 1 < (i + 1) by A110, NAT_1: 13;

        then (i + 1) in ( Seg ( len hb)) by A95, A111, FINSEQ_1: 1;

        then (i + 1) in ( dom hb) by FINSEQ_1:def 3;

        then

         A115: (hb . (i + 1)) in ( rng hb) by FUNCT_1:def 3;

        

         A116: (i + 1) in ( dom h29) by A111, A114, FINSEQ_3: 25;

        then (h29 . (i + 1)) = (g . (hb . (i + 1))) by A96;

        then (h29 . (i + 1)) in ( rng g) by A92, A109, A115, FUNCT_1:def 3;

        then

         A117: (g . (hb . (i + 1))) is Element of ( TOP-REAL 2) by A96, A116;

        i in ( dom h29) by A110, A112, FINSEQ_3: 25;

        then

         A118: (h29 . i) = (g . (hb . i)) by A96;

        ( [#] I[01] ) is compact & (g .: the carrier of I[01] ) = ( rng g) by COMPTS_1: 1, RELSET_1: 22;

        then

         A119: Qa is compact by A4, WEIERSTR: 8;

        reconsider Qa as non empty Subset of ( TOP-REAL 2);

        set r1 = (((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) + 1);

        

         A120: (hb . (i + 1)) = (hb /. (i + 1)) by A95, A111, A114, FINSEQ_4: 15;

        

         A121: for x,y be Point of ( Euclid 2) st x in W1 & y in W1 holds ( dist (x,y)) <= r1

        proof

          let x,y be Point of ( Euclid 2);

          assume that

           A122: x in W1 and

           A123: y in W1;

          reconsider pw1 = x, pw2 = y as Point of ( TOP-REAL 2) by A122, A123;

          

           A124: ( S-bound Qa) <= (pw2 `2 ) & (pw2 `2 ) <= ( N-bound Qa) by A119, A123, PSCOMP_1: 24;

          ( S-bound Qa) <= (pw1 `2 ) & (pw1 `2 ) <= ( N-bound Qa) by A119, A122, PSCOMP_1: 24;

          then

           A125: |.((pw1 `2 ) - (pw2 `2 )).| <= (( N-bound Qa) - ( S-bound Qa)) by A124, JGRAPH_1: 27;

          

           A126: ((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) <= (((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) + 1) by XREAL_1: 29;

          

           A127: ( W-bound Qa) <= (pw2 `1 ) & (pw2 `1 ) <= ( E-bound Qa) by A119, A123, PSCOMP_1: 24;

          ( W-bound Qa) <= (pw1 `1 ) & (pw1 `1 ) <= ( E-bound Qa) by A119, A122, PSCOMP_1: 24;

          then |.((pw1 `1 ) - (pw2 `1 )).| <= (( E-bound Qa) - ( W-bound Qa)) by A127, JGRAPH_1: 27;

          then ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= ((( E-bound Qa) - ( W-bound Qa)) + (( N-bound Qa) - ( S-bound Qa))) by A125, XREAL_1: 7;

          then

           A128: ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) <= r1 by A126, XXREAL_0: 2;

          ( dist (x,y)) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= ( |.((pw1 `1 ) - (pw2 `1 )).| + |.((pw1 `2 ) - (pw2 `2 )).|) by JGRAPH_1: 28, JGRAPH_1: 32;

          hence thesis by A128, XXREAL_0: 2;

        end;

         0 in the carrier of I[01] by BORSUK_1: 43;

        then

         A129: (g . 0 ) in ( rng g) by A109, FUNCT_1:def 3;

        then ( S-bound Qa) <= (q1 `2 ) & (q1 `2 ) <= ( N-bound Qa) by A4, A107, A119, PSCOMP_1: 24;

        then ( S-bound Qa) <= ( N-bound Qa) by XXREAL_0: 2;

        then

         A130: 0 <= (( N-bound Qa) - ( S-bound Qa)) by XREAL_1: 48;

        i in ( Seg ( len hb)) by A95, A110, A112, FINSEQ_1: 1;

        then

         A131: i in ( dom hb) by FINSEQ_1:def 3;

        then

         A132: (hb . i) in ( rng hb) by FUNCT_1:def 3;

        then (h29 . i) in ( rng g) by A92, A118, A109, FUNCT_1:def 3;

        then

        reconsider w1 = (g . (hb . i)), w2 = (g . (hb . (i + 1))) as Point of ( Euclid 2) by A118, A117, TOPREAL3: 8;

        (i + 1) in ( Seg ( len hb)) by A95, A111, A114, FINSEQ_1: 1;

        then

         A133: (i + 1) in ( dom hb) by FINSEQ_1:def 3;

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

        then

        reconsider R = [.(hb /. i), (hb /. (i + 1)).] as Subset of I[01] by A92, A132, A113, A120, BORSUK_1: 40, XXREAL_2:def 12;

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

        then

         A134: (hb /. i) <= (hb /. (i + 1)) by A93, A131, A113, A133, A120, SEQM_3:def 1;

        then (hb . i) in R by A113, XXREAL_1: 1;

        then

         A135: w1 in (g .: R) by A109, FUNCT_1:def 6;

        ( W-bound Qa) <= (q1 `1 ) & (q1 `1 ) <= ( E-bound Qa) by A4, A107, A119, A129, PSCOMP_1: 24;

        then ( W-bound Qa) <= ( E-bound Qa) by XXREAL_0: 2;

        then 0 <= (( E-bound Qa) - ( W-bound Qa)) by XREAL_1: 48;

        then

         A136: W1 is bounded by A130, A121, TBSP_1:def 7;

        (hb . (i + 1)) in R by A120, A134, XXREAL_1: 1;

        then

         A137: w2 in (g .: R) by A109, FUNCT_1:def 6;

        reconsider W = (g .: R) as Subset of ( Euclid 2) by TOPREAL3: 8;

        ( dom g) = ( [#] I[01] ) by FUNCT_2:def 1;

        then Q = (g .: [. 0 , 1.]) by A4, BORSUK_1: 40, RELAT_1: 113;

        then W is bounded by A136, BORSUK_1: 40, RELAT_1: 123, TBSP_1: 14;

        then

         A138: ( dist (w1,w2)) <= ( diameter W) by A135, A137, TBSP_1:def 8;

        ( diameter W) < e by A94, A95, A110, A112;

        then

         A139: ( dist (w1,w2)) < e by A138, XXREAL_0: 2;

        (h2 . (i + 1)) = (h2 /. (i + 1)) by A111, A114, FINSEQ_4: 15;

        then

         A140: (h2 /. (i + 1)) = (g . (hb . (i + 1))) by A96, A116;

        (h2 /. i) = (g . (hb . i)) by A110, A112, A118, FINSEQ_4: 15;

        hence thesis by A140, A139, JGRAPH_1: 28;

      end;

      

       A141: ( dom hb) = ( Seg ( len hb)) by FINSEQ_1:def 3;

      

       A142: for i st i in ( dom hb) holds (h2 /. i) = (g . (hb . i))

      proof

        let i;

        assume

         A143: i in ( dom hb);

        then i in ( dom h29) by A95, FINSEQ_3: 29;

        then

         A144: (h2 . i) = (g . (hb . i)) by A96;

        1 <= i & i <= ( len hb) by A141, A143, FINSEQ_1: 1;

        hence thesis by A95, A144, FINSEQ_4: 15;

      end;

      

       A145: for i st i in ( dom h2) holds (p1 `1 ) <= ((h2 /. i) `1 ) & ((h2 /. i) `1 ) <= (p2 `1 )

      proof

        let i;

        assume i in ( dom h2);

        then i in ( Seg ( len h2)) by FINSEQ_1:def 3;

        then i in ( dom hb) by A95, FINSEQ_1:def 3;

        then

         A146: (h2 /. i) = (g . (hb . i)) & (hb . i) in ( rng hb) by A142, FUNCT_1:def 3;

        ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

        then (h2 /. i) in ( rng g) by A92, A146, FUNCT_1:def 3;

        hence thesis by A4, A6;

      end;

      for i st i in ( dom ( X_axis h2)) holds (p1 `1 ) <= (( X_axis h2) . i) & (( X_axis h2) . i) <= (p2 `1 )

      proof

        let i;

        assume i in ( dom ( X_axis h2));

        then i in ( Seg ( len ( X_axis h2))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h2)) by A101, JGRAPH_1: 41;

        then

         A147: i in ( dom h2) by FINSEQ_1:def 3;

        then (( X_axis h2) . i) = ((h2 /. i) `1 ) by JGRAPH_1: 43;

        hence thesis by A145, A147;

      end;

      then

       A148: ( X_axis h2) lies_between ((p1 `1 ),(p2 `1 )) by GOBOARD4:def 2;

      

       A149: (g . 1) = q2 by BORSUK_2:def 4;

      

       A150: for i st i in ( dom h2) holds ((h2 /. 1) `2 ) <= ((h2 /. i) `2 ) & ((h2 /. i) `2 ) <= ((h2 /. ( len h2)) `2 )

      proof

        let i;

        assume i in ( dom h2);

        then i in ( Seg ( len h2)) by FINSEQ_1:def 3;

        then i in ( dom hb) by A95, FINSEQ_1:def 3;

        then

         A151: (h2 /. i) = (g . (hb . i)) & (hb . i) in ( rng hb) by A142, FUNCT_1:def 3;

        1 in ( Seg ( len hb)) by A95, A101, FINSEQ_1: 1;

        then 1 in ( dom hb) by FINSEQ_1:def 3;

        then

         A152: (h2 /. 1) = (g . (hb . 1)) by A142;

        ( len hb) in ( Seg ( len hb)) by A95, A101, FINSEQ_1: 1;

        then ( len hb) in ( dom hb) by FINSEQ_1:def 3;

        then

         A153: (h2 /. ( len h2)) = (g . (hb . ( len hb))) by A95, A142;

        ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

        then (h2 /. i) in ( rng g) by A92, A151, FUNCT_1:def 3;

        hence thesis by A4, A8, A107, A149, A89, A90, A152, A153;

      end;

      for i st i in ( dom ( Y_axis h2)) holds (( Y_axis h2) . 1) <= (( Y_axis h2) . i) & (( Y_axis h2) . i) <= (( Y_axis h2) . ( len h2))

      proof

        let i;

        

         A154: (( Y_axis h2) . 1) = ((h2 /. 1) `2 ) & (( Y_axis h2) . ( len h2)) = ((h2 /. ( len h2)) `2 ) by A101, JGRAPH_1: 42;

        assume i in ( dom ( Y_axis h2));

        then i in ( Seg ( len ( Y_axis h2))) by FINSEQ_1:def 3;

        then i in ( Seg ( len h2)) by A101, JGRAPH_1: 42;

        then

         A155: i in ( dom h2) by FINSEQ_1:def 3;

        then (( Y_axis h2) . i) = ((h2 /. i) `2 ) by JGRAPH_1: 43;

        hence thesis by A150, A155, A154;

      end;

      then ( Y_axis h2) lies_between ((( Y_axis h2) . 1),(( Y_axis h2) . ( len h2))) by GOBOARD4:def 2;

      then

      consider g2 be FinSequence of ( TOP-REAL 2) such that

       A156: g2 is special and

       A157: (g2 . 1) = (h2 . 1) and

       A158: (g2 . ( len g2)) = (h2 . ( len h2)) and

       A159: ( len g2) >= ( len h2) and

       A160: ( Y_axis g2) lies_between ((( Y_axis h2) . 1),(( Y_axis h2) . ( len h2))) & ( X_axis g2) lies_between ((p1 `1 ),(p2 `1 )) and

       A161: for j st j in ( dom g2) holds ex k be Nat st k in ( dom h2) & |.((g2 /. j) - (h2 /. k)).| < e and

       A162: for j st 1 <= j & (j + 1) <= ( len g2) holds |.((g2 /. j) - (g2 /. (j + 1))).| < e by A13, A101, A148, A108, JGRAPH_1: 40;

      

       A163: ( len g2) >= 1 by A101, A159, XXREAL_0: 2;

      then

       A164: (g2 /. ( len g2)) = (g2 . ( len g2)) by FINSEQ_4: 15;

      1 in ( dom hb) by A105, FINSEQ_3: 25;

      then

       A165: (h2 /. 1) = q1 by A107, A89, A142;

      

       A166: (h2 . 1) = (h2 /. 1) by A105, A95, FINSEQ_4: 15;

      

       A167: (h1 . ( len h1)) = (h1 /. ( len h1)) by A28, FINSEQ_4: 15;

      

      then

       A168: (( X_axis f2) . ( len f2)) = ((h1 /. ( len h1)) `1 ) by A82, A87, A88, JGRAPH_1: 41

      .= (( X_axis h1) . ( len h1)) by A28, JGRAPH_1: 41;

      ( len h) in ( dom h19) by A20, A28, FINSEQ_3: 25;

      then (h1 /. ( len h1)) = p2 by A71, A15, A20, A21, A167;

      then

       A169: (( X_axis f2) . ( len f2)) = (p2 `1 ) by A82, A87, A167, A88, JGRAPH_1: 41;

      5 <= ( len f2) by A16, A20, A83, XXREAL_0: 2;

      then

       A170: 2 <= ( len f2) by XXREAL_0: 2;

       0 in ( dom g) by A103, FUNCT_2:def 1;

      then

       A171: q1 in Q9 by A4, A107, FUNCT_1:def 3;

      

       A172: (f2 . 1) = (f2 /. 1) by A87, FINSEQ_4: 15;

      (g2 . 1) = (g2 /. 1) by A163, FINSEQ_4: 15;

      

      then

       A173: (( Y_axis g2) . 1) = ((h2 /. 1) `2 ) by A157, A163, A166, JGRAPH_1: 42

      .= (( Y_axis h2) . 1) by A101, JGRAPH_1: 42;

      (g2 /. 1) = (g2 . 1) by A163, FINSEQ_4: 15;

      then

       A174: (( Y_axis g2) . 1) = (q1 `2 ) by A157, A163, A165, A166, JGRAPH_1: 42;

      ( len hb) in ( dom hb) by A105, FINSEQ_3: 25;

      then (g2 . ( len g2)) = q2 by A149, A90, A95, A142, A158, A106;

      then

       A175: (( Y_axis g2) . ( len g2)) = (q2 `2 ) by A163, A164, JGRAPH_1: 42;

      (g2 . ( len g2)) = (g2 /. ( len g2)) by A163, FINSEQ_4: 15;

      

      then

       A176: (( Y_axis g2) . ( len g2)) = ((h2 /. ( len h2)) `2 ) by A158, A163, A106, JGRAPH_1: 42

      .= (( Y_axis h2) . ( len h2)) by A101, JGRAPH_1: 42;

      5 <= ( len g2) by A91, A95, A159, XXREAL_0: 2;

      then

       A177: 2 <= ( len g2) by XXREAL_0: 2;

      1 in ( dom h19) by A28, FINSEQ_3: 25;

      then (h1 . 1) = (f . (h . 1)) by A21;

      then

       A178: (( X_axis f2) . 1) = (p1 `1 ) by A30, A14, A81, A87, A172, JGRAPH_1: 41;

      

       A179: (( X_axis f2) . 1) = ((h1 /. 1) `1 ) by A81, A87, A29, A172, JGRAPH_1: 41

      .= (( X_axis h1) . 1) by A28, JGRAPH_1: 41;

      now

        per cases ;

          case

           A180: p1 = p2;

           0 in the carrier of I[01] by BORSUK_1: 43;

          then 0 in ( dom f) by FUNCT_2:def 1;

          then

           A181: p1 in P by A3, A30, FUNCT_1: 3;

           0 in the carrier of I[01] by BORSUK_1: 43;

          then

           A182: 0 in ( dom g) by FUNCT_2:def 1;

          then

           A183: q1 in Q by A4, A107, FUNCT_1: 3;

          

           A184: for q be Point of ( TOP-REAL 2) st q in Q holds (q `1 ) = (p1 `1 )

          proof

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

            assume q in Q;

            then (p1 `1 ) <= (q `1 ) & (q `1 ) <= (p2 `1 ) by A6;

            hence thesis by A180, XXREAL_0: 1;

          end;

           A185:

          now

            assume

             A186: (q1 `2 ) = (q2 `2 );

            (q1 `2 ) <= (p1 `2 ) & (p1 `2 ) <= (q2 `2 ) by A7, A181;

            then

             A187: (p1 `2 ) = (q1 `2 ) by A186, XXREAL_0: 1;

            (q1 `1 ) = (p1 `1 ) by A4, A107, A184, A182, FUNCT_1: 3;

            then q1 = p1 by A187, TOPREAL3: 6;

            hence contradiction by A11, A183, A181, XBOOLE_0:def 4;

          end;

          

           A188: p1 in ( LSeg (q1,q2))

          proof

            1 in the carrier of I[01] by BORSUK_1: 43;

            then 1 in ( dom g) by FUNCT_2:def 1;

            then (g . 1) in ( rng g) by FUNCT_1: 3;

            then (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p2 `1 ) by A4, A6, A149;

            then

             A189: (p1 `1 ) = (q2 `1 ) by A180, XXREAL_0: 1;

            set ln = (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )));

            

             A190: (ln * (q2 `2 )) = ((((p1 `2 ) - (q1 `2 )) * (q2 `2 )) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 74

            .= ((((p1 `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 ))) / ((q2 `2 ) - (q1 `2 )));

            

             A191: ((q2 `2 ) - (q1 `2 )) <> 0 by A185;

            

            then (1 - ln) = ((((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) by XCMPLX_1: 60

            .= ((((q2 `2 ) - (q1 `2 )) - ((p1 `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 120

            .= (((q2 `2 ) - (p1 `2 )) / ((q2 `2 ) - (q1 `2 )));

            

            then

             A192: ((1 - ln) * (q1 `2 )) = ((((q2 `2 ) - (p1 `2 )) * (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 74

            .= ((((q2 `2 ) * (q1 `2 )) - ((p1 `2 ) * (q1 `2 ))) / ((q2 `2 ) - (q1 `2 )));

             0 in the carrier of I[01] by BORSUK_1: 43;

            then 0 in ( dom g) by FUNCT_2:def 1;

            then q1 in Q by A4, A107, FUNCT_1: 3;

            then (p1 `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p2 `1 ) by A6;

            then

             A193: (p1 `1 ) = (q1 `1 ) by A180, XXREAL_0: 1;

             0 in the carrier of I[01] by BORSUK_1: 43;

            then 0 in ( dom f) by FUNCT_2:def 1;

            then

             A194: (f . 0 ) in ( rng f) by FUNCT_1: 3;

            then

             A195: (q1 `2 ) <= (p1 `2 ) by A3, A7, A30;

            

             A196: ((((1 - ln) * q1) + (ln * q2)) `1 ) = ((((1 - ln) * q1) `1 ) + ((ln * q2) `1 )) by TOPREAL3: 2

            .= (((1 - ln) * (q1 `1 )) + ((ln * q2) `1 )) by TOPREAL3: 4

            .= (((1 - ln) * (p1 `1 )) + (ln * (p1 `1 ))) by A193, A189, TOPREAL3: 4

            .= (p1 `1 );

            ((((1 - ln) * q1) + (ln * q2)) `2 ) = ((((1 - ln) * q1) `2 ) + ((ln * q2) `2 )) by TOPREAL3: 2

            .= (((1 - ln) * (q1 `2 )) + ((ln * q2) `2 )) by TOPREAL3: 4

            .= (((1 - ln) * (q1 `2 )) + (ln * (q2 `2 ))) by TOPREAL3: 4

            .= (((((q2 `2 ) * (q1 `2 )) - ((p1 `2 ) * (q1 `2 ))) + (((p1 `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 )))) / ((q2 `2 ) - (q1 `2 ))) by A192, A190, XCMPLX_1: 62

            .= (((p1 `2 ) * ((q2 `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 )))

            .= ((p1 `2 ) * (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) by XCMPLX_1: 74

            .= ((p1 `2 ) * 1) by A191, XCMPLX_1: 60

            .= (p1 `2 );

            then

             A197: (((1 - ln) * q1) + (ln * q2)) = p1 by A196, TOPREAL3: 6;

            

             A198: (p1 `2 ) <= (q2 `2 ) by A3, A7, A30, A194;

            then (q2 `2 ) >= (q1 `2 ) by A195, XXREAL_0: 2;

            then (q2 `2 ) > (q1 `2 ) by A185, XXREAL_0: 1;

            then

             A199: ((q2 `2 ) - (q1 `2 )) > 0 by XREAL_1: 50;

            ((p1 `2 ) - (q1 `2 )) <= ((q2 `2 ) - (q1 `2 )) by A198, XREAL_1: 13;

            then ln <= (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) by A199, XREAL_1: 72;

            then

             A200: ln <= 1 by A199, XCMPLX_1: 60;

            ((p1 `2 ) - (q1 `2 )) >= 0 by A195, XREAL_1: 48;

            hence thesis by A199, A200, A197;

          end;

          1 in the carrier of I[01] by BORSUK_1: 43;

          then 1 in ( dom g) by FUNCT_2:def 1;

          then

           A201: q2 in Q by A4, A149, FUNCT_1: 3;

          Q c= ( LSeg (q1,q2))

          proof

            (p1 `1 ) <= (q2 `1 ) & (q2 `1 ) <= (p2 `1 ) by A6, A201;

            then

             A202: (p1 `1 ) = (q2 `1 ) by A180, XXREAL_0: 1;

            (p1 `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p2 `1 ) by A6, A183;

            then

             A203: (p1 `1 ) = (q1 `1 ) by A180, XXREAL_0: 1;

            let z be object;

            assume

             A204: z in Q;

            then

            reconsider qz = z as Point of ( TOP-REAL 2);

            

             A205: (qz `2 ) <= (q2 `2 ) by A8, A204;

            set ln = (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )));

            

             A206: (ln * (q2 `2 )) = ((((qz `2 ) - (q1 `2 )) * (q2 `2 )) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 74

            .= ((((qz `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 ))) / ((q2 `2 ) - (q1 `2 )));

            

             A207: ((q2 `2 ) - (q1 `2 )) <> 0 by A185;

            

            then (1 - ln) = ((((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) by XCMPLX_1: 60

            .= ((((q2 `2 ) - (q1 `2 )) - ((qz `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 120

            .= (((q2 `2 ) - (qz `2 )) / ((q2 `2 ) - (q1 `2 )));

            

            then

             A208: ((1 - ln) * (q1 `2 )) = ((((q2 `2 ) - (qz `2 )) * (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) by XCMPLX_1: 74

            .= ((((q2 `2 ) * (q1 `2 )) - ((qz `2 ) * (q1 `2 ))) / ((q2 `2 ) - (q1 `2 )));

            

             A209: ((((1 - ln) * q1) + (ln * q2)) `2 ) = ((((1 - ln) * q1) `2 ) + ((ln * q2) `2 )) by TOPREAL3: 2

            .= (((1 - ln) * (q1 `2 )) + ((ln * q2) `2 )) by TOPREAL3: 4

            .= (((1 - ln) * (q1 `2 )) + (ln * (q2 `2 ))) by TOPREAL3: 4

            .= (((((q2 `2 ) * (q1 `2 )) - ((qz `2 ) * (q1 `2 ))) + (((qz `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 )))) / ((q2 `2 ) - (q1 `2 ))) by A208, A206, XCMPLX_1: 62

            .= (((qz `2 ) * ((q2 `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 )))

            .= ((qz `2 ) * (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) by XCMPLX_1: 74

            .= ((qz `2 ) * 1) by A207, XCMPLX_1: 60

            .= (qz `2 );

            

             A210: (p1 `1 ) <= (qz `1 ) & (qz `1 ) <= (p2 `1 ) by A6, A204;

            ((((1 - ln) * q1) + (ln * q2)) `1 ) = ((((1 - ln) * q1) `1 ) + ((ln * q2) `1 )) by TOPREAL3: 2

            .= (((1 - ln) * (q1 `1 )) + ((ln * q2) `1 )) by TOPREAL3: 4

            .= (((1 - ln) * (p1 `1 )) + (ln * (p1 `1 ))) by A203, A202, TOPREAL3: 4

            .= (qz `1 ) by A180, A210, XXREAL_0: 1;

            then

             A211: (((1 - ln) * q1) + (ln * q2)) = qz by A209, TOPREAL3: 6;

            

             A212: (q1 `2 ) <= (qz `2 ) by A8, A204;

            then (q2 `2 ) >= (q1 `2 ) by A205, XXREAL_0: 2;

            then (q2 `2 ) > (q1 `2 ) by A185, XXREAL_0: 1;

            then

             A213: ((q2 `2 ) - (q1 `2 )) > 0 by XREAL_1: 50;

            ((qz `2 ) - (q1 `2 )) <= ((q2 `2 ) - (q1 `2 )) by A205, XREAL_1: 13;

            then ln <= (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) by A213, XREAL_1: 72;

            then

             A214: ln <= 1 by A213, XCMPLX_1: 60;

            ((qz `2 ) - (q1 `2 )) >= 0 by A212, XREAL_1: 48;

            hence thesis by A213, A214, A211;

          end;

          then p1 in Q by A4, A188, Th3;

          hence contradiction by A104, A11, XBOOLE_0:def 4;

        end;

          case

           A215: p1 <> p2;

          

           A216: 1 <= ( len hb) by A91, XXREAL_0: 2;

          then 1 in ( dom hb) by FINSEQ_3: 25;

          then

           A217: (h2 /. 1) = (g . (hb . 1)) by A142;

           A218:

          now

             0 in the carrier of I[01] by BORSUK_1: 43;

            then 0 in ( dom g) by FUNCT_2:def 1;

            then

             A219: q1 in Q by A4, A107, FUNCT_1: 3;

             0 in the carrier of I[01] by BORSUK_1: 43;

            then

             A220: 0 in ( dom f) by FUNCT_2:def 1;

            then

             A221: p1 in P by A3, A30, FUNCT_1: 3;

            assume

             A222: q1 = q2;

            

             A223: for p be Point of ( TOP-REAL 2) st p in P holds (p `2 ) = (q1 `2 )

            proof

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

              assume p in P;

              then (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 ) by A7;

              hence thesis by A222, XXREAL_0: 1;

            end;

             A224:

            now

              assume

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

              (p1 `1 ) <= (q1 `1 ) & (q1 `1 ) <= (p2 `1 ) by A6, A219;

              then

               A226: (q1 `1 ) = (p1 `1 ) by A225, XXREAL_0: 1;

              (p1 `2 ) = (q1 `2 ) by A3, A30, A223, A220, FUNCT_1: 3;

              then p1 = q1 by A226, TOPREAL3: 6;

              hence contradiction by A11, A221, A219, XBOOLE_0:def 4;

            end;

            

             A227: q1 in ( LSeg (p1,p2))

            proof

              1 in the carrier of I[01] by BORSUK_1: 43;

              then 1 in ( dom f) by FUNCT_2:def 1;

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

              then (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A3, A7, A71;

              then

               A228: (q1 `2 ) = (p2 `2 ) by A222, XXREAL_0: 1;

              set ln = (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )));

              

               A229: (ln * (p2 `1 )) = ((((q1 `1 ) - (p1 `1 )) * (p2 `1 )) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 74

              .= ((((q1 `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 ))) / ((p2 `1 ) - (p1 `1 )));

              

               A230: ((p2 `1 ) - (p1 `1 )) <> 0 by A224;

              

              then (1 - ln) = ((((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) by XCMPLX_1: 60

              .= ((((p2 `1 ) - (p1 `1 )) - ((q1 `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 120

              .= (((p2 `1 ) - (q1 `1 )) / ((p2 `1 ) - (p1 `1 )));

              

              then

               A231: ((1 - ln) * (p1 `1 )) = ((((p2 `1 ) - (q1 `1 )) * (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 74

              .= ((((p2 `1 ) * (p1 `1 )) - ((q1 `1 ) * (p1 `1 ))) / ((p2 `1 ) - (p1 `1 )));

               0 in the carrier of I[01] by BORSUK_1: 43;

              then 0 in ( dom f) by FUNCT_2:def 1;

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

              then (q1 `2 ) <= (p1 `2 ) & (p1 `2 ) <= (q2 `2 ) by A3, A7, A30;

              then

               A232: (q1 `2 ) = (p1 `2 ) by A222, XXREAL_0: 1;

               0 in the carrier of I[01] by BORSUK_1: 43;

              then 0 in ( dom g) by FUNCT_2:def 1;

              then

               A233: (g . 0 ) in ( rng g) by FUNCT_1: 3;

              then

               A234: (p1 `1 ) <= (q1 `1 ) by A4, A6, A107;

              

               A235: ((((1 - ln) * p1) + (ln * p2)) `2 ) = ((((1 - ln) * p1) `2 ) + ((ln * p2) `2 )) by TOPREAL3: 2

              .= (((1 - ln) * (p1 `2 )) + ((ln * p2) `2 )) by TOPREAL3: 4

              .= (((1 - ln) * (q1 `2 )) + (ln * (q1 `2 ))) by A232, A228, TOPREAL3: 4;

              ((((1 - ln) * p1) + (ln * p2)) `1 ) = ((((1 - ln) * p1) `1 ) + ((ln * p2) `1 )) by TOPREAL3: 2

              .= (((1 - ln) * (p1 `1 )) + ((ln * p2) `1 )) by TOPREAL3: 4

              .= (((1 - ln) * (p1 `1 )) + (ln * (p2 `1 ))) by TOPREAL3: 4

              .= (((((p2 `1 ) * (p1 `1 )) - ((q1 `1 ) * (p1 `1 ))) + (((q1 `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 )))) / ((p2 `1 ) - (p1 `1 ))) by A231, A229, XCMPLX_1: 62

              .= (((q1 `1 ) * ((p2 `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 )))

              .= ((q1 `1 ) * (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) by XCMPLX_1: 74

              .= ((q1 `1 ) * 1) by A230, XCMPLX_1: 60;

              then

               A236: (((1 - ln) * p1) + (ln * p2)) = q1 by A235, TOPREAL3: 6;

              

               A237: (q1 `1 ) <= (p2 `1 ) by A4, A6, A107, A233;

              then (p2 `1 ) >= (p1 `1 ) by A234, XXREAL_0: 2;

              then (p2 `1 ) > (p1 `1 ) by A224, XXREAL_0: 1;

              then

               A238: ((p2 `1 ) - (p1 `1 )) > 0 by XREAL_1: 50;

              ((q1 `1 ) - (p1 `1 )) <= ((p2 `1 ) - (p1 `1 )) by A237, XREAL_1: 13;

              then ln <= (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) by A238, XREAL_1: 72;

              then

               A239: ln <= 1 by A238, XCMPLX_1: 60;

              ((q1 `1 ) - (p1 `1 )) >= 0 by A234, XREAL_1: 48;

              hence thesis by A238, A239, A236;

            end;

            1 in the carrier of I[01] by BORSUK_1: 43;

            then 1 in ( dom f) by FUNCT_2:def 1;

            then

             A240: p2 in P by A3, A71, FUNCT_1: 3;

            P c= ( LSeg (p1,p2))

            proof

              (q1 `2 ) <= (p2 `2 ) & (p2 `2 ) <= (q2 `2 ) by A7, A240;

              then

               A241: (q1 `2 ) = (p2 `2 ) by A222, XXREAL_0: 1;

              (q1 `2 ) <= (p1 `2 ) & (p1 `2 ) <= (q2 `2 ) by A7, A221;

              then

               A242: (q1 `2 ) = (p1 `2 ) by A222, XXREAL_0: 1;

              let z be object;

              assume

               A243: z in P;

              then

              reconsider pz = z as Point of ( TOP-REAL 2);

              

               A244: (pz `1 ) <= (p2 `1 ) by A5, A243;

              set ln = (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )));

              

               A245: (ln * (p2 `1 )) = ((((pz `1 ) - (p1 `1 )) * (p2 `1 )) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 74

              .= ((((pz `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 ))) / ((p2 `1 ) - (p1 `1 )));

              

               A246: ((p2 `1 ) - (p1 `1 )) <> 0 by A224;

              

              then (1 - ln) = ((((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) by XCMPLX_1: 60

              .= ((((p2 `1 ) - (p1 `1 )) - ((pz `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 120

              .= (((p2 `1 ) - (pz `1 )) / ((p2 `1 ) - (p1 `1 )));

              

              then

               A247: ((1 - ln) * (p1 `1 )) = ((((p2 `1 ) - (pz `1 )) * (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) by XCMPLX_1: 74

              .= ((((p2 `1 ) * (p1 `1 )) - ((pz `1 ) * (p1 `1 ))) / ((p2 `1 ) - (p1 `1 )));

              

               A248: ((((1 - ln) * p1) + (ln * p2)) `1 ) = ((((1 - ln) * p1) `1 ) + ((ln * p2) `1 )) by TOPREAL3: 2

              .= (((1 - ln) * (p1 `1 )) + ((ln * p2) `1 )) by TOPREAL3: 4

              .= (((1 - ln) * (p1 `1 )) + (ln * (p2 `1 ))) by TOPREAL3: 4

              .= (((((p2 `1 ) * (p1 `1 )) - ((pz `1 ) * (p1 `1 ))) + (((pz `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 )))) / ((p2 `1 ) - (p1 `1 ))) by A247, A245, XCMPLX_1: 62

              .= (((pz `1 ) * ((p2 `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 )))

              .= ((pz `1 ) * (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) by XCMPLX_1: 74

              .= ((pz `1 ) * 1) by A246, XCMPLX_1: 60

              .= (pz `1 );

              

               A249: (q1 `2 ) <= (pz `2 ) & (pz `2 ) <= (q2 `2 ) by A7, A243;

              ((((1 - ln) * p1) + (ln * p2)) `2 ) = ((((1 - ln) * p1) `2 ) + ((ln * p2) `2 )) by TOPREAL3: 2

              .= (((1 - ln) * (p1 `2 )) + ((ln * p2) `2 )) by TOPREAL3: 4

              .= (((1 - ln) * (q1 `2 )) + (ln * (q1 `2 ))) by A242, A241, TOPREAL3: 4

              .= (pz `2 ) by A222, A249, XXREAL_0: 1;

              then

               A250: (((1 - ln) * p1) + (ln * p2)) = pz by A248, TOPREAL3: 6;

              

               A251: (p1 `1 ) <= (pz `1 ) by A5, A243;

              then (p2 `1 ) >= (p1 `1 ) by A244, XXREAL_0: 2;

              then (p2 `1 ) > (p1 `1 ) by A224, XXREAL_0: 1;

              then

               A252: ((p2 `1 ) - (p1 `1 )) > 0 by XREAL_1: 50;

              ((pz `1 ) - (p1 `1 )) <= ((p2 `1 ) - (p1 `1 )) by A244, XREAL_1: 13;

              then ln <= (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) by A252, XREAL_1: 72;

              then

               A253: ln <= 1 by A252, XCMPLX_1: 60;

              ((pz `1 ) - (p1 `1 )) >= 0 by A251, XREAL_1: 48;

              hence thesis by A252, A253, A250;

            end;

            then q1 in P by A3, A227, Th3;

            hence contradiction by A171, A11, XBOOLE_0:def 4;

          end;

          ( len hb) in ( dom hb) by A216, FINSEQ_3: 25;

          then

           A254: (g2 . 1) <> (g2 . ( len g2)) by A107, A149, A89, A90, A95, A142, A157, A158, A166, A106, A218, A217;

          (f2 /. 1) <> (f2 /. ( len f2)) by A30, A71, A14, A15, A20, A21, A81, A82, A29, A172, A88, A102, A23, A215;

          then ( L~ f2) meets ( L~ g2) by A80, A84, A156, A160, A172, A88, A178, A169, A174, A175, A179, A168, A173, A176, A170, A177, A254, JGRAPH_1: 26;

          then

          consider s be object such that

           A255: s in ( L~ f2) and

           A256: s in ( L~ g2) by XBOOLE_0: 3;

          reconsider ps = s as Point of ( TOP-REAL 2) by A255;

          ps in ( union { ( LSeg (f2,i)) : 1 <= i & (i + 1) <= ( len f2) }) by A255, TOPREAL1:def 4;

          then

          consider x such that

           A257: ps in x & x in { ( LSeg (f2,i)) : 1 <= i & (i + 1) <= ( len f2) } by TARSKI:def 4;

          ps in ( union { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) }) by A256, TOPREAL1:def 4;

          then

          consider y such that

           A258: ps in y & y in { ( LSeg (g2,j)) : 1 <= j & (j + 1) <= ( len g2) } by TARSKI:def 4;

          consider i such that

           A259: x = ( LSeg (f2,i)) and

           A260: 1 <= i and

           A261: (i + 1) <= ( len f2) by A257;

          ( LSeg (f2,i)) = ( LSeg ((f2 /. i),(f2 /. (i + 1)))) by A260, A261, TOPREAL1:def 3;

          then

           A262: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A257, A259, JGRAPH_1: 36;

          i < ( len f2) by A261, NAT_1: 13;

          then i in ( dom f2) by A260, FINSEQ_3: 25;

          then

          consider k be Nat such that

           A263: k in ( dom h1) and

           A264: |.((f2 /. i) - (h1 /. k)).| < e by A85;

          consider j such that

           A265: y = ( LSeg (g2,j)) and

           A266: 1 <= j and

           A267: (j + 1) <= ( len g2) by A258;

          ( LSeg (g2,j)) = ( LSeg ((g2 /. j),(g2 /. (j + 1)))) by A266, A267, TOPREAL1:def 3;

          then

           A268: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A258, A265, JGRAPH_1: 36;

          reconsider p11 = (h1 /. k) as Point of ( TOP-REAL 2);

           |.((f2 /. i) - (f2 /. (i + 1))).| < e by A86, A260, A261;

          then |.(ps - (f2 /. i)).| < e by A262, XXREAL_0: 2;

          then |.(ps - (h1 /. k)).| <= ( |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).|) & ( |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).|) < (e + e) by A264, TOPRNS_1: 34, XREAL_1: 8;

          then |.(ps - (h1 /. k)).| < (e + e) by XXREAL_0: 2;

          then

           A269: |.(p11 - ps).| < (e + e) by TOPRNS_1: 27;

          

           A270: k in ( Seg ( len h1)) by A263, FINSEQ_1:def 3;

          then 1 <= k & k <= ( len h1) by FINSEQ_1: 1;

          then (h1 . k) = (h1 /. k) by FINSEQ_4: 15;

          then

           A271: (h1 /. k) = (f . (h . k)) by A21, A263;

          j < ( len g2) by A267, NAT_1: 13;

          then j in ( dom g2) by A266, FINSEQ_3: 25;

          then

          consider k9 be Nat such that

           A272: k9 in ( dom h2) and

           A273: |.((g2 /. j) - (h2 /. k9)).| < e by A161;

          k9 in ( Seg ( len h2)) by A272, FINSEQ_1:def 3;

          then k9 in ( dom hb) by A95, FINSEQ_1:def 3;

          then

           A274: (hb . k9) in ( rng hb) & (h2 /. k9) = (g . (hb . k9)) by A142, FUNCT_1:def 3;

          reconsider q11 = (h2 /. k9) as Point of ( TOP-REAL 2);

          reconsider x1 = p11, x2 = q11 as Point of ( Euclid 2) by EUCLID: 22;

          ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

          then

           A275: (h2 /. k9) in ( rng g) by A92, A274, FUNCT_1:def 3;

          k in ( dom h) by A20, A270, FINSEQ_1:def 3;

          then

           A276: (h . k) in ( rng h) by FUNCT_1:def 3;

          ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

          then (h1 /. k) in P by A3, A17, A271, A276, FUNCT_1:def 3;

          then ( min_dist_min (P9,Q9)) <= ( dist (x1,x2)) by A4, A10, A9, A275, WEIERSTR: 34;

          then

           A277: ( min_dist_min (P9,Q9)) <= |.(p11 - q11).| by JGRAPH_1: 28;

           |.((g2 /. j) - (g2 /. (j + 1))).| < e by A162, A266, A267;

          then |.(ps - (g2 /. j)).| < e by A268, XXREAL_0: 2;

          then |.(ps - (h2 /. k9)).| <= ( |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).|) & ( |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).|) < (e + e) by A273, TOPRNS_1: 34, XREAL_1: 8;

          then |.(ps - (h2 /. k9)).| < (e + e) by XXREAL_0: 2;

          then |.(p11 - q11).| <= ( |.(p11 - ps).| + |.(ps - q11).|) & ( |.(p11 - ps).| + |.(ps - q11).|) < ((e + e) + (e + e)) by A269, TOPRNS_1: 34, XREAL_1: 8;

          then |.(p11 - q11).| < (((e + e) + e) + e) by XXREAL_0: 2;

          then ( min_dist_min (P9,Q9)) < (4 * e) by A277, XXREAL_0: 2;

          then ((4 * e) - (5 * e)) > 0 by XREAL_1: 50;

          then (((4 - 5) * e) / e) > 0 by A13, XREAL_1: 139;

          then (4 - 5) > 0 by A12;

          hence contradiction;

        end;

      end;

      hence contradiction;

    end;

    theorem :: JGRAPH_8:5

    

     Th5: for f,g be continuous Function of I[01] , ( TOP-REAL 2), O,I be Point of I[01] st O = 0 & I = 1 & ((f . O) `1 ) = a & ((f . I) `1 ) = b & ((g . O) `2 ) = c & ((g . I) `2 ) = d & (for r be Point of I[01] holds a <= ((f . r) `1 ) & ((f . r) `1 ) <= b & a <= ((g . r) `1 ) & ((g . r) `1 ) <= b & c <= ((f . r) `2 ) & ((f . r) `2 ) <= d & c <= ((g . r) `2 ) & ((g . r) `2 ) <= d) holds ( rng f) meets ( rng g)

    proof

      let f,g be continuous Function of I[01] , ( TOP-REAL 2), O,I be Point of I[01] ;

      assume that

       A1: O = 0 & I = 1 and

       A2: ((f . O) `1 ) = a and

       A3: ((f . I) `1 ) = b and

       A4: ((g . O) `2 ) = c and

       A5: ((g . I) `2 ) = d and

       A6: for r be Point of I[01] holds a <= ((f . r) `1 ) & ((f . r) `1 ) <= b & a <= ((g . r) `1 ) & ((g . r) `1 ) <= b & c <= ((f . r) `2 ) & ((f . r) `2 ) <= d & c <= ((g . r) `2 ) & ((g . r) `2 ) <= d;

      reconsider Q = ( rng g) as non empty Subset of ( TOP-REAL 2);

      

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

      .= ( rng g) by PRE_TOPC:def 5;

      ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

      then

      reconsider g1 = g as Function of I[01] , (( TOP-REAL 2) | Q) by A7, FUNCT_2: 1;

      reconsider q2 = (g1 . I) as Point of ( TOP-REAL 2) by A5;

      reconsider q1 = (g1 . O) as Point of ( TOP-REAL 2) by A4;

      reconsider P = ( rng f) as non empty Subset of ( TOP-REAL 2);

      

       A8: the carrier of (( TOP-REAL 2) | P) = ( [#] (( TOP-REAL 2) | P))

      .= ( rng f) by PRE_TOPC:def 5;

      ( dom f) = the carrier of I[01] by FUNCT_2:def 1;

      then

      reconsider f1 = f as Function of I[01] , (( TOP-REAL 2) | P) by A8, FUNCT_2: 1;

      reconsider p2 = (f1 . I) as Point of ( TOP-REAL 2) by A3;

      reconsider p1 = (f1 . O) as Point of ( TOP-REAL 2) by A2;

      

       A9: for p be Point of ( TOP-REAL 2) st p in P holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )

      proof

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

        assume p in P;

        then ex x be object st x in ( dom f1) & p = (f1 . x) by FUNCT_1:def 3;

        hence thesis by A2, A3, A6;

      end;

      

       A10: for p be Point of ( TOP-REAL 2) st p in P holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )

      proof

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

        assume p in P;

        then ex x be object st x in ( dom f1) & p = (f1 . x) by FUNCT_1:def 3;

        hence thesis by A4, A5, A6;

      end;

      

       A11: for p be Point of ( TOP-REAL 2) st p in Q holds (q1 `2 ) <= (p `2 ) & (p `2 ) <= (q2 `2 )

      proof

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

        assume p in Q;

        then ex x be object st x in ( dom g1) & p = (g1 . x) by FUNCT_1:def 3;

        hence thesis by A4, A5, A6;

      end;

      

       A12: for p be Point of ( TOP-REAL 2) st p in Q holds (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )

      proof

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

        assume p in Q;

        then ex x be object st x in ( dom g1) & p = (g1 . x) by FUNCT_1:def 3;

        hence thesis by A2, A3, A6;

      end;

      f is Path of p1, p2 & g is Path of q1, q2 by A1, BORSUK_2:def 4;

      hence thesis by A9, A12, A10, A11, Th4;

    end;

    theorem :: JGRAPH_8:6

    for ar,br,cr,dr be Point of ( Trectangle (a,b,c,d)) holds for h be Path of ar, br, v be Path of dr, cr holds for Ar,Br,Cr,Dr be Point of ( TOP-REAL 2) st (Ar `1 ) = a & (Br `1 ) = b & (Cr `2 ) = c & (Dr `2 ) = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds ex s,t be Point of I[01] st (h . s) = (v . t)

    proof

      let ar,br,cr,dr be Point of ( Trectangle (a,b,c,d));

      let h be Path of ar, br;

      let v be Path of dr, cr;

      let Ar,Br,Cr,Dr be Point of ( TOP-REAL 2) such that

       A1: (Ar `1 ) = a & (Br `1 ) = b & (Cr `2 ) = c & (Dr `2 ) = d & ar = Ar & br = Br & cr = Cr & dr = Dr;

      set TR = ( Trectangle (a,b,c,d));

      per cases ;

        suppose

         A2: TR is empty;

        take 1[01] , 1[01] ;

        thus thesis by A2;

      end;

        suppose TR is non empty;

        then

        reconsider TR = ( Trectangle (a,b,c,d)) as non empty convex SubSpace of ( TOP-REAL 2);

        reconsider ar, br, cr, dr as Point of TR;

        reconsider h as Path of ar, br;

        reconsider v as Path of dr, cr;

        

         A3: (h . 0 ) = ar & (h . 1) = br by BORSUK_2:def 4;

        the carrier of TR is Subset of ( TOP-REAL 2) by TSEP_1: 1;

        then

        reconsider f = h, g = ( - v) as Function of I[01] , ( TOP-REAL 2) by FUNCT_2: 7;

        

         A4: (( - v) . 0 ) = cr & (( - v) . 1) = dr by BORSUK_2:def 4;

        

         A5: for r be Point of I[01] holds a <= ((f . r) `1 ) & ((f . r) `1 ) <= b & a <= ((g . r) `1 ) & ((g . r) `1 ) <= b & c <= ((f . r) `2 ) & ((f . r) `2 ) <= d & c <= ((g . r) `2 ) & ((g . r) `2 ) <= d

        proof

          let r be Point of I[01] ;

          

           A6: the carrier of TR = ( closed_inside_of_rectangle (a,b,c,d)) by PRE_TOPC: 8

          .= { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & c <= (p `2 ) & (p `2 ) <= d } by JGRAPH_6:def 2;

          (( - v) . r) in the carrier of TR;

          then

           A7: ex p be Point of ( TOP-REAL 2) st (( - v) . r) = p & a <= (p `1 ) & (p `1 ) <= b & c <= (p `2 ) & (p `2 ) <= d by A6;

          (h . r) in the carrier of TR;

          then ex p be Point of ( TOP-REAL 2) st (h . r) = p & a <= (p `1 ) & (p `1 ) <= b & c <= (p `2 ) & (p `2 ) <= d by A6;

          hence thesis by A7;

        end;

        f is continuous & g is continuous by PRE_TOPC: 26;

        then ( rng f) meets ( rng g) by A1, A3, A4, A5, Th5, BORSUK_1:def 14, BORSUK_1:def 15;

        then

        consider y be object such that

         A8: y in ( rng f) and

         A9: y in ( rng g) by XBOOLE_0: 3;

        consider t be object such that

         A10: t in ( dom g) and

         A11: (g . t) = y by A9, FUNCT_1:def 3;

        consider s be object such that

         A12: s in ( dom f) and

         A13: (f . s) = y by A8, FUNCT_1:def 3;

        reconsider s, t as Point of I[01] by A12, A10;

        reconsider t1 = (1 - t) as Point of I[01] by JORDAN5B: 4;

        take s, t1;

        (dr,cr) are_connected by BORSUK_2:def 3;

        hence thesis by A13, A11, BORSUK_2:def 6;

      end;

    end;