jct_misc.miz

    begin

    scheme :: JCT_MISC:sch1

    NonEmpty { A() -> non empty set , F( object) -> set } :

the set of all F(a) where a be Element of A() is non empty;

      consider a0 be object such that

       A1: a0 in A() by XBOOLE_0:def 1;

      F(a0) in the set of all F(a) where a be Element of A() by A1;

      hence thesis;

    end;

    reserve r,s,r0,s0,t for Real;

    theorem :: JCT_MISC:1



     Th1: for a,b be Real st r in [.a, b.] & s in [.a, b.] holds ((r + s) / 2) in [.a, b.]

    proof

      let a,b be Real such that

       A1: r in [.a, b.] and

       A2: s in [.a, b.];

      reconsider a, b, r, s as Real;



       A3: s <= b by A2, XXREAL_1: 1;

      r <= b by A1, XXREAL_1: 1;

      then (r + s) <= (b + b) by A3, XREAL_1: 7;

      then

       A4: ((r + s) / 2) <= ((b + b) / 2) by XREAL_1: 72;



       A5: a <= s by A2, XXREAL_1: 1;

      a <= r by A1, XXREAL_1: 1;

      then (a + a) <= (r + s) by A5, XREAL_1: 7;

      then ((a + a) / 2) <= ((r + s) / 2) by XREAL_1: 72;

      hence thesis by A4;

    end;

    theorem :: JCT_MISC:2



     Th2: |.( |.(r0 - s0).| - |.(r - s).|).| <= ( |.(r0 - r).| + |.(s0 - s).|)

    proof

      ((r0 - s0) - (r - s)) = ((r0 - r) - (s0 - s));

      then

       A1: |.((r0 - s0) - (r - s)).| <= ( |.(r0 - r).| + |.(s0 - s).|) by COMPLEX1: 57;

       |.( |.(r0 - s0).| - |.(r - s).|).| <= |.((r0 - s0) - (r - s)).| by COMPLEX1: 64;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: JCT_MISC:3



     Th3: t in ].r, s.[ implies |.t.| < ( max ( |.r.|, |.s.|))

    proof

      assume

       A1: t in ].r, s.[;

      reconsider r, t, s as Real;



       A2: r < t by A1, XXREAL_1: 4;



       A3: t < s by A1, XXREAL_1: 4;

      per cases ;

        suppose

         A4: t >= 0 ;

        then t = |.t.| by ABSVALUE:def 1;

        then |.t.| < |.s.| by A3, A4, ABSVALUE:def 1;

        hence thesis by XXREAL_0: 30;

      end;

        suppose

         A5: t < 0 ;

        then

         A6: ( - t) = |.t.| by ABSVALUE:def 1;

        ( - r) = |.r.| by A2, A5, ABSVALUE:def 1;

        then |.t.| < |.r.| by A2, A6, XREAL_1: 24;

        hence thesis by XXREAL_0: 30;

      end;

    end;

    scheme :: JCT_MISC:sch2

    DoubleChoice { A,B,C() -> non empty set , P[ object, object, object] } :

ex a be Function of A(), B(), b be Function of A(), C() st for i be Element of A() holds P[i, (a . i), (b . i)]

      provided

       A1: for i be Element of A() holds ex ai be Element of B(), bi be Element of C() st P[i, ai, bi];

      defpred P1[ object, object] means P[$1, ($2 `1 ), ($2 `2 )];



       A2: for e be Element of A() holds ex u be Element of [:B(), C():] st P1[e, u]

      proof

        let e be Element of A();

        consider ai be Element of B(), bi be Element of C() such that

         A3: P[e, ai, bi] by A1;

        reconsider u = [ai, bi] as Element of [:B(), C():] by ZFMISC_1: 87;

        take u;

        thus thesis by A3;

      end;

      consider f be Function of A(), [:B(), C():] such that

       A4: for e be Element of A() holds P1[e, (f . e)] from FUNCT_2:sch 3( A2);

      take ( pr1 f), ( pr2 f);

      let i be Element of A();



       A5: ((f . i) `2 ) = (( pr2 f) . i) by FUNCT_2:def 6;

      ((f . i) `1 ) = (( pr1 f) . i) by FUNCT_2:def 5;

      hence thesis by A4, A5;

    end;

    theorem :: JCT_MISC:4



     Th4: for S,T be non empty TopSpace, G be Subset of [:S, T:] st for x be Point of [:S, T:] st x in G holds ex GS be Subset of S, GT be Subset of T st GS is open & GT is open & x in [:GS, GT:] & [:GS, GT:] c= G holds G is open

    proof

      let S,T be non empty TopSpace, G be Subset of [:S, T:] such that

       A1: for x be Point of [:S, T:] st x in G holds ex GS be Subset of S, GT be Subset of T st GS is open & GT is open & x in [:GS, GT:] & [:GS, GT:] c= G;

      set A = { [:GS, GT:] where GS be Subset of S, GT be Subset of T : GS is open & GT is open & [:GS, GT:] c= G };

      A c= ( bool the carrier of [:S, T:])

      proof

        let e be object;

        assume e in A;

        then ex GS be Subset of S, GT be Subset of T st e = [:GS, GT:] & GS is open & GT is open & [:GS, GT:] c= G;

        hence thesis;

      end;

      then

      reconsider A as Subset-Family of [:S, T:];

      reconsider A as Subset-Family of [:S, T:];

      for x be object holds x in G iff ex Y be set st x in Y & Y in A

      proof

        let x be object;

        thus x in G implies ex Y be set st x in Y & Y in A

        proof

          assume x in G;

          then

          consider GS be Subset of S, GT be Subset of T such that

           A2: GS is open and

           A3: GT is open and

           A4: x in [:GS, GT:] and

           A5: [:GS, GT:] c= G by A1;

          take [:GS, GT:];

          thus thesis by A2, A3, A4, A5;

        end;

        given Y be set such that

         A6: x in Y and

         A7: Y in A;

        ex GS be Subset of S, GT be Subset of T st Y = [:GS, GT:] & GS is open & GT is open & [:GS, GT:] c= G by A7;

        hence thesis by A6;

      end;

      then

       A8: G = ( union A) by TARSKI:def 4;

      for e be set st e in A holds ex X1 be Subset of S, Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open

      proof

        let e be set;

        assume e in A;

        then ex GS be Subset of S, GT be Subset of T st e = [:GS, GT:] & GS is open & GT is open & [:GS, GT:] c= G;

        hence thesis;

      end;

      hence thesis by A8, BORSUK_1: 5;

    end;

    begin

    theorem :: JCT_MISC:5



     Th5: for A,B be compact Subset of REAL holds (A /\ B) is compact

    proof

      let A,B be compact Subset of REAL ;

      let s1 be Real_Sequence such that

       A1: ( rng s1) c= (A /\ B);



       A2: (A /\ B) c= B by XBOOLE_1: 17;

      (A /\ B) c= A by XBOOLE_1: 17;

      then ( rng s1) c= A by A1;

      then

      consider s2 be Real_Sequence such that

       A3: s2 is subsequence of s1 and

       A4: s2 is convergent and

       A5: ( lim s2) in A by RCOMP_1:def 3;

      ( rng s2) c= ( rng s1) by A3, VALUED_0: 21;

      then ( rng s2) c= (A /\ B) by A1;

      then ( rng s2) c= B by A2;

      then

      consider s3 be Real_Sequence such that

       A6: s3 is subsequence of s2 and

       A7: s3 is convergent and

       A8: ( lim s3) in B by RCOMP_1:def 3;

      take s3;

      thus s3 is subsequence of s1 by A3, A6, VALUED_0: 20;

      thus s3 is convergent by A7;

      ( lim s3) = ( lim s2) by A4, A6, SEQ_4: 17;

      hence thesis by A5, A8, XBOOLE_0:def 4;

    end;

    theorem :: JCT_MISC:6

    for T be non empty TopSpace holds for f be continuous RealMap of T holds for A be Subset of T st A is connected holds (f .: A) is interval

    proof

      let T be non empty TopSpace;

      let f be continuous RealMap of T;

      let A be Subset of T;

      assume

       A1: A is connected;

      let r,s be ExtReal;



       A2: A c= (f " (f .: A)) by FUNCT_2: 42;

      assume

       A3: r in (f .: A);

      then

      consider p be Point of T such that

       A4: p in A and

       A5: r = (f . p) by FUNCT_2: 65;

      assume

       A6: s in (f .: A);

      then

      consider q be Point of T such that

       A7: q in A and

       A8: s = (f . q) by FUNCT_2: 65;

      assume

       A9: not [.r, s.] c= (f .: A);

      reconsider r, s as Real by A3, A6;

      consider t be Element of REAL such that

       A10: t in [.r, s.] and

       A11: not t in (f .: A) by A9;

      reconsider r, s, t as Real;

      set P1 = (f " ( left_open_halfline t)), Q1 = (f " ( right_open_halfline t)), P = (P1 /\ A), Q = (Q1 /\ A), X = (( left_open_halfline t) \/ ( right_open_halfline t));



       A12: Q1 is open by PSCOMP_1: 8;

      t <= s by A10, XXREAL_1: 1;

      then

       A13: t < s by A6, A11, XXREAL_0: 1;

      ( right_open_halfline t) = { r1 where r1 be Real : t < r1 } by XXREAL_1: 230;

      then s in ( right_open_halfline t) by A13;

      then q in Q1 by A8, FUNCT_2: 38;

      then

       A14: Q <> ( {} T) by A7, XBOOLE_0:def 4;

      (( left_open_halfline t) /\ ( right_open_halfline t)) = ].t, t.[ by XXREAL_1: 269

      .= {} by XXREAL_1: 28;

      then ( left_open_halfline t) misses ( right_open_halfline t);

      then P1 misses Q1 by FUNCT_1: 71;

      then (P1 /\ Q1) = {} ;

      then

       A15: (P1 /\ Q1) misses (P \/ Q);

      reconsider Y = {t} as Subset of REAL ;

      (Y ` ) = ( REAL \ [.t, t.]) by XXREAL_1: 17

      .= X by XXREAL_1: 385;



      then

       A16: ((f " Y) ` ) = (f " X) by FUNCT_2: 100

      .= (P1 \/ Q1) by RELAT_1: 140;

      (f " {t}) misses (f " (f .: A)) by A11, FUNCT_1: 71, ZFMISC_1: 50;

      then (f " {t}) misses A by A2, XBOOLE_1: 63;

      then A c= (P1 \/ Q1) by A16, SUBSET_1: 23;



      then

       A17: A = (A /\ (P1 \/ Q1)) by XBOOLE_1: 28

      .= (P \/ Q) by XBOOLE_1: 23;



       A18: P c= P1 by XBOOLE_1: 17;

      r <= t by A10, XXREAL_1: 1;

      then

       A19: r < t by A3, A11, XXREAL_0: 1;

      ( left_open_halfline t) = { r1 where r1 be Real : r1 < t } by XXREAL_1: 229;

      then r in ( left_open_halfline t) by A19;

      then p in P1 by A5, FUNCT_2: 38;

      then

       A20: P <> ( {} T) by A4, XBOOLE_0:def 4;



       A21: Q c= Q1 by XBOOLE_1: 17;

      P1 is open by PSCOMP_1: 8;

      then (P,Q) are_separated by A12, A18, A21, A15, TSEP_1: 45;

      hence contradiction by A1, A17, A20, A14, CONNSP_1: 15;

    end;

    definition

      let A,B be Subset of REAL ;

      :: JCT_MISC:def1

      func dist (A,B) -> Real means

      : Def1: ex X be Subset of REAL st X = { |.(r - s).| where r,s be Real : r in A & s in B } & it = ( lower_bound X);

      existence

      proof

        set Y = { |.(r - s).| where r,s be Real : r in A & s in B };

        Y c= REAL

        proof

          let e be object;

          assume e in Y;

          then ex r,s be Real st e = |.(r - s).| & r in A & s in B;

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider Y0 = Y as Subset of REAL ;

        take ( lower_bound Y0);

        thus thesis;

      end;

      uniqueness ;

      commutativity

      proof

        let IT be Real, A,B be Subset of REAL ;

        given X0 be Subset of REAL such that

         A1: X0 = { |.(r - s).| where r,s be Real : r in A & s in B } and

         A2: IT = ( lower_bound X0);

        set Y = { |.(r - s).| where r,s be Real : r in B & s in A };

        Y c= REAL

        proof

          let e be object;

          assume e in Y;

          then ex r,s be Real st e = |.(r - s).| & r in B & s in A;

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider Y0 = Y as Subset of REAL ;

        take Y0;

        thus Y0 = { |.(r - s).| where r,s be Real : r in B & s in A };

        X0 = Y0

        proof

          thus X0 c= Y0

          proof

            let x be object;

            assume x in X0;

            then

            consider r,s be Real such that

             A3: x = |.(r - s).| and

             A4: r in A and

             A5: s in B by A1;

            x = |.(s - r).| by A3, UNIFORM1: 11;

            hence thesis by A4, A5;

          end;

          let x be object;

          assume x in Y0;

          then

          consider r,s be Real such that

           A6: x = |.(r - s).| and

           A7: r in B and

           A8: s in A;

          x = |.(s - r).| by A6, UNIFORM1: 11;

          hence thesis by A1, A7, A8;

        end;

        hence thesis by A2;

      end;

    end

    theorem :: JCT_MISC:7



     Th7: for A,B be Subset of REAL , r, s st r in A & s in B holds |.(r - s).| >= ( dist (A,B))

    proof

      let A,B be Subset of REAL ;

      set Y = { |.(r - s).| where r,s be Real : r in A & s in B };

      let r, s;

      assume that

       A1: r in A and

       A2: s in B;

      Y c= REAL

      proof

        let e be object;

        assume e in Y;

        then ex r,s be Real st e = |.(r - s).| & r in A & s in B;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider Y0 = Y as Subset of REAL ;



       A3: Y0 is bounded_below

      proof

        take 0 ;

        let r0 be ExtReal;

        assume r0 in Y0;

        then ex r,s be Real st r0 = |.(r - s).| & r in A & s in B;

        hence thesis by COMPLEX1: 46;

      end;



       A4: ( dist (A,B)) = ( lower_bound Y0) by Def1;

       |.(r - s).| in Y0 by A1, A2;

      hence thesis by A4, A3, SEQ_4:def 2;

    end;

    theorem :: JCT_MISC:8



     Th8: for A,B be Subset of REAL , C,D be non empty Subset of REAL st C c= A & D c= B holds ( dist (A,B)) <= ( dist (C,D))

    proof

      let A,B be Subset of REAL , C,D be non empty Subset of REAL such that

       A1: C c= A and

       A2: D c= B;

      consider s0 be object such that

       A3: s0 in D by XBOOLE_0:def 1;

      set Y = { |.(r - s).| where r,s be Real : r in C & s in D };

      consider r0 be object such that

       A4: r0 in C by XBOOLE_0:def 1;



       A5: Y c= REAL

      proof

        let e be object;

        assume e in Y;

        then ex r,s be Real st e = |.(r - s).| & r in C & s in D;

        hence thesis by XREAL_0:def 1;

      end;

      reconsider r0, s0 as Real by A4, A3;

       |.(r0 - s0).| in Y by A4, A3;

      then

      reconsider Y as non empty Subset of REAL by A5;

      set X = { |.(r - s).| where r,s be Real : r in A & s in B };

      X c= REAL

      proof

        let e be object;

        assume e in X;

        then ex r,s be Real st e = |.(r - s).| & r in A & s in B;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider X as Subset of REAL ;



       A6: Y c= X

      proof

        let x be object;

        assume x in Y;

        then ex r,s be Real st x = |.(r - s).| & r in C & s in D;

        hence thesis by A1, A2;

      end;



       A7: X is bounded_below

      proof

        take 0 ;

        let r0 be ExtReal;

        assume r0 in X;

        then ex r,s be Real st r0 = |.(r - s).| & r in A & s in B;

        hence thesis by COMPLEX1: 46;

      end;



       A8: ( dist (C,D)) = ( lower_bound Y) by Def1;

      ( dist (A,B)) = ( lower_bound X) by Def1;

      hence thesis by A7, A8, A6, SEQ_4: 47;

    end;

    theorem :: JCT_MISC:9



     Th9: for A,B be non empty compact Subset of REAL holds ex r,s be Real st r in A & s in B & ( dist (A,B)) = |.(r - s).|

    proof

      defpred P[ set, set] means ex r,s be Real st $1 = [r, s] & $2 = |.(r - s).|;

      let A,B be non empty compact Subset of REAL ;

      reconsider At = A, Bt = B as non empty compact Subset of R^1 by JORDAN5A: 25, TOPMETR: 17;



       A1: the carrier of ( R^1 | Bt) = Bt by PRE_TOPC: 8;

      reconsider AB = [:( R^1 | At), ( R^1 | Bt):] as compact non empty TopSpace;



       A2: the carrier of ( R^1 | At) = At by PRE_TOPC: 8;

       A3:

      now

        let x be Element of AB;

        x in the carrier of AB;

        then x in [:A, B:] by A2, A1, BORSUK_1:def 2;

        then

        consider r,s be object such that

         A4: r in REAL and

         A5: s in REAL and

         A6: x = [r, s] by ZFMISC_1: 84;

        reconsider r, s as Real by A4, A5;

        reconsider t = |.(r - s).| as Element of REAL by XREAL_0:def 1;

        take t;

        thus P[x, t] by A6;

      end;

      consider f be RealMap of AB such that

       A7: for x be Element of AB holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      for Y be Subset of REAL st Y is open holds (f " Y) is open

      proof

        let Y be Subset of REAL such that

         A8: Y is open;

        for x be Point of AB st x in (f " Y) holds ex YS be Subset of ( R^1 | At), YT be Subset of ( R^1 | Bt) st YS is open & YT is open & x in [:YS, YT:] & [:YS, YT:] c= (f " Y)

        proof

          let x be Point of AB;

          consider r,s be Real such that

           A9: x = [r, s] and

           A10: (f . x) = |.(r - s).| by A7;

          assume x in (f " Y);

          then (f . x) in Y by FUNCT_1:def 7;

          then

          consider N be Neighbourhood of (f . x) such that

           A11: N c= Y by A8, RCOMP_1: 18;

          consider g be Real such that

           A12: 0 < g and

           A13: N = ].((f . x) - g), ((f . x) + g).[ by RCOMP_1:def 6;

          reconsider a = (r - (g / 2)), b = (r + (g / 2)), c = (s - (g / 2)), d = (s + (g / 2)) as Real;

          reconsider S = ].a, b.[, T = ].c, d.[ as Subset of R^1 by TOPMETR: 17;

          reconsider YT = (T /\ B) as Subset of ( R^1 | Bt) by A1, XBOOLE_1: 17;

          reconsider YS = (S /\ A) as Subset of ( R^1 | At) by A2, XBOOLE_1: 17;



           A14: s in T by A12, TOPREAL6: 15, XREAL_1: 215;

          take YS, YT;



           A15: T is open by JORDAN6: 35;

          S is open by JORDAN6: 35;

          hence YS is open & YT is open by A2, A1, A15, TSP_1:def 1;



           A16: r in S by A12, TOPREAL6: 15, XREAL_1: 215;

          x in the carrier of AB;

          then

           A17: x in [:A, B:] by A2, A1, BORSUK_1:def 2;

          then s in B by A9, ZFMISC_1: 87;

          then

           A18: s in YT by A14, XBOOLE_0:def 4;

          (f .: [:YS, YT:]) c= N

          proof

            let e be object;

            assume e in (f .: [:YS, YT:]);

            then

            consider y be Element of AB such that

             A19: y in [:YS, YT:] and

             A20: e = (f . y) by FUNCT_2: 65;

            consider r1,s1 be Real such that

             A21: y = [r1, s1] and

             A22: (f . y) = |.(r1 - s1).| by A7;



             A23: |.( |.(r1 - s1).| - |.(r - s).|).| <= ( |.(r1 - r).| + |.(s1 - s).|) by Th2;

            s1 in YT by A19, A21, ZFMISC_1: 87;

            then s1 in ].(s - (g / 2)), (s + (g / 2)).[ by XBOOLE_0:def 4;

            then

             A24: |.(s1 - s).| < (g / 2) by RCOMP_1: 1;

            r1 in YS by A19, A21, ZFMISC_1: 87;

            then r1 in ].(r - (g / 2)), (r + (g / 2)).[ by XBOOLE_0:def 4;

            then

             A25: |.(r1 - r).| < (g / 2) by RCOMP_1: 1;

            g = ((g / 2) + (g / 2));

            then ( |.(r1 - r).| + |.(s1 - s).|) < g by A25, A24, XREAL_1: 8;

            then |.( |.(r1 - s1).| - |.(r - s).|).| < g by A23, XXREAL_0: 2;

            hence thesis by A13, A10, A20, A22, RCOMP_1: 1;

          end;

          then

           A26: (f .: [:YS, YT:]) c= Y by A11;

          r in A by A9, A17, ZFMISC_1: 87;

          then r in YS by A16, XBOOLE_0:def 4;

          hence x in [:YS, YT:] by A9, A18, ZFMISC_1: 87;

          ( dom f) = the carrier of AB by FUNCT_2:def 1;

          hence thesis by A26, FUNCT_1: 93;

        end;

        hence thesis by Th4;

      end;

      then

      reconsider f as continuous RealMap of AB by PSCOMP_1: 8;

      (f .: the carrier of AB) is with_min by MEASURE6:def 13;

      then ( lower_bound (f .: the carrier of AB)) in (f .: the carrier of AB) by MEASURE6:def 5;

      then

      consider x be Element of AB such that

       A27: x in the carrier of AB and

       A28: ( lower_bound (f .: the carrier of AB)) = (f . x) by FUNCT_2: 65;



       A29: x in [:A, B:] by A2, A1, A27, BORSUK_1:def 2;

      then

      consider r1,s1 be object such that

       A30: r1 in REAL and

       A31: s1 in REAL and

       A32: x = [r1, s1] by ZFMISC_1: 84;



       A33: (f .: the carrier of AB) = { |.(r - s).| where r,s be Real : r in A & s in B }

      proof

        hereby

          let x be object;

          assume x in (f .: the carrier of AB);

          then

          consider y be Element of AB such that

           A34: y in the carrier of AB and

           A35: x = (f . y) by FUNCT_2: 65;

          consider r1,s1 be Real such that

           A36: y = [r1, s1] and

           A37: (f . y) = |.(r1 - s1).| by A7;



           A38: [r1, s1] in [:A, B:] by A2, A1, A34, A36, BORSUK_1:def 2;

          then

           A39: s1 in B by ZFMISC_1: 87;

          r1 in A by A38, ZFMISC_1: 87;

          hence x in { |.(r - s).| where r,s be Real : r in A & s in B } by A35, A37, A39;

        end;

        let x be object;

        assume x in { |.(r - s).| where r,s be Real : r in A & s in B };

        then

        consider r,s be Real such that

         A40: x = |.(r - s).| and

         A41: r in A and

         A42: s in B;

         [r, s] in [:A, B:] by A41, A42, ZFMISC_1: 87;

        then

        reconsider y = [r, s] as Element of AB by A2, A1, BORSUK_1:def 2;

        consider r1,s1 be Real such that

         A43: y = [r1, s1] and

         A44: (f . y) = |.(r1 - s1).| by A7;



         A45: s1 = s by A43, XTUPLE_0: 1;

        r1 = r by A43, XTUPLE_0: 1;

        hence thesis by A40, A44, A45, FUNCT_2: 35;

      end;

      reconsider r1, s1 as Real by A30, A31;

      take r1, s1;

      thus r1 in A & s1 in B by A29, A32, ZFMISC_1: 87;

      consider r,s be Real such that

       A46: x = [r, s] and

       A47: (f . x) = |.(r - s).| by A7;



       A48: s1 = s by A32, A46, XTUPLE_0: 1;

      r1 = r by A32, A46, XTUPLE_0: 1;

      hence thesis by A28, A33, A47, A48, Def1;

    end;

    theorem :: JCT_MISC:10



     Th10: for A,B be non empty compact Subset of REAL holds ( dist (A,B)) >= 0

    proof

      let A,B be non empty compact Subset of REAL ;

      set X = { |.(r - s).| where r,s be Real : r in A & s in B };

      consider r0 be object such that

       A1: r0 in A by XBOOLE_0:def 1;



       A2: X c= REAL

      proof

        let e be object;

        assume e in X;

        then ex r,s be Real st e = |.(r - s).| & r in A & s in B;

        hence thesis by XREAL_0:def 1;

      end;

      consider s0 be object such that

       A3: s0 in B by XBOOLE_0:def 1;

      reconsider r0, s0 as Real by A1, A3;

       |.(r0 - s0).| in X by A1, A3;

      then

      reconsider X as non empty Subset of REAL by A2;



       A4: for t be Real st t in X holds t >= 0

      proof

        let t be Real;

        assume t in X;

        then ex r,s be Real st t = |.(r - s).| & r in A & s in B;

        hence thesis by COMPLEX1: 46;

      end;

      ( dist (A,B)) = ( lower_bound X) by Def1;

      hence thesis by A4, SEQ_4: 43;

    end;

    theorem :: JCT_MISC:11



     Th11: for A,B be non empty compact Subset of REAL st A misses B holds ( dist (A,B)) > 0

    proof

      let A,B be non empty compact Subset of REAL such that

       A1: A misses B;

      consider r0, s0 such that

       A2: r0 in A and

       A3: s0 in B and

       A4: ( dist (A,B)) = |.(r0 - s0).| by Th9;

      reconsider r0, s0 as Real;

      assume ( dist (A,B)) <= 0 ;

      then |.(r0 - s0).| = 0 by A4, Th10;

      then r0 = s0 by GOBOARD7: 2;

      hence contradiction by A1, A2, A3, XBOOLE_0: 3;

    end;

    theorem :: JCT_MISC:12

    for e,f be Real, A,B be compact Subset of REAL st A misses B & A c= [.e, f.] & B c= [.e, f.] holds for S be sequence of ( bool REAL ) st for i be Nat holds (S . i) is interval & (S . i) meets A & (S . i) meets B holds ex r be Real st r in [.e, f.] & not r in (A \/ B) & for i be Nat holds ex k be Nat st i <= k & r in (S . k)

    proof

      let e,f be Real, A,B be compact Subset of REAL such that

       A1: A misses B and

       A2: A c= [.e, f.] and

       A3: B c= [.e, f.];

      let S be sequence of ( bool REAL ) such that

       A4: for i be Nat holds (S . i) is interval & (S . i) meets A & (S . i) meets B;

      defpred P[ set, Subset of REAL ] means $2 is non empty closed_interval & $2 meets A & $2 meets B & $2 c= (S . $1);



       A5: for i be Element of NAT holds ex u be Subset of REAL st P[i, u]

      proof

        let i be Element of NAT ;



         A6: (S . i) is interval by A4;

        (S . i) meets B by A4;

        then

        consider y be object such that

         A7: y in (S . i) and

         A8: y in B by XBOOLE_0: 3;

        (S . i) meets A by A4;

        then

        consider x be object such that

         A9: x in (S . i) and

         A10: x in A by XBOOLE_0: 3;

        reconsider y as Real by A8;

        reconsider x as Real by A10;

        per cases ;

          suppose

           A11: x <= y;

          take [.x, y.];

          thus [.x, y.] is non empty closed_interval by A11, MEASURE5: 14;

          x in [.x, y.] by A11;

          hence [.x, y.] meets A by A10, XBOOLE_0: 3;

          y in [.x, y.] by A11;

          hence [.x, y.] meets B by A8, XBOOLE_0: 3;

          thus [.x, y.] c= (S . i) by A9, A7, A6;

        end;

          suppose

           A12: y <= x;

          take [.y, x.];

          thus [.y, x.] is non empty closed_interval by A12, MEASURE5: 14;

          x in [.y, x.] by A12;

          hence [.y, x.] meets A by A10, XBOOLE_0: 3;

          y in [.y, x.] by A12;

          hence [.y, x.] meets B by A8, XBOOLE_0: 3;

          thus [.y, x.] c= (S . i) by A9, A7, A6;

        end;

      end;

      consider T be sequence of ( bool REAL ) such that

       A13: for i be Element of NAT holds P[i, (T . i)] from FUNCT_2:sch 3( A5);

      (T . 0 ) meets B by A13;

      then

       A14: B is non empty;

      deffunc G( Nat) = ((T . $1) /\ B);

      deffunc F( Nat) = ((T . $1) /\ A);

      consider SA be sequence of ( bool REAL ) such that

       A15: for i be Element of NAT holds (SA . i) = F(i) from FUNCT_2:sch 4;

      consider SB be sequence of ( bool REAL ) such that

       A16: for i be Element of NAT holds (SB . i) = G(i) from FUNCT_2:sch 4;

      defpred P[ Nat, Real, Real] means $2 in (SA . $1) & $3 in (SB . $1) & ( dist ((SA . $1),(SB . $1))) = |.($2 - $3).|;



       A17: for i be Element of NAT holds ex ai,bi be Element of REAL st P[i, ai, bi]

      proof

        let i be Element of NAT ;

        reconsider Si = (T . i) as non empty closed_interval Subset of REAL by A13;



         A18: (T . i) meets B by A13;



         A19: (SA . i) = (Si /\ A) by A15;



         A20: (SB . i) = (Si /\ B) by A16;

        (T . i) meets A by A13;

        then

        reconsider SAi = (SA . i), SBi = (SB . i) as non empty compact Subset of REAL by A18, A19, A20, Th5;

        consider ai,bi be Real such that

         A21: ai in SAi and

         A22: bi in SBi and

         A23: ( dist (SAi,SBi)) = |.(ai - bi).| by Th9;

        reconsider ai, bi as Element of REAL by XREAL_0:def 1;

        take ai, bi;

        thus thesis by A21, A22, A23;

      end;

      consider sa,sb be Real_Sequence such that

       A24: for i be Element of NAT holds P[i, (sa . i), (sb . i)] from DoubleChoice( A17);

      ( rng sa) c= [.e, f.]

      proof

        let u be object;

        assume u in ( rng sa);

        then

        consider x be object such that

         A25: x in ( dom sa) and

         A26: u = (sa . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A25;

        (sa . n) in (SA . n) by A24;

        then u in ((T . n) /\ A) by A15, A26;

        then u in A by XBOOLE_0:def 4;

        hence thesis by A2;

      end;

      then

      consider ga be Real_Sequence such that

       A27: ga is subsequence of sa and

       A28: ga is convergent and

       A29: ( lim ga) in [.e, f.] by RCOMP_1:def 3;

      consider Nseq be increasing sequence of NAT such that

       A30: ga = (sa * Nseq) by A27, VALUED_0:def 17;

      set gb = (sb * Nseq);

      ( rng gb) c= [.e, f.]

      proof

        let u be object;

        assume u in ( rng gb);

        then

        consider x be object such that

         A31: x in ( dom gb) and

         A32: u = (gb . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A31;

        (gb . n) = (sb . (Nseq . n)) by FUNCT_2: 15;

        then (gb . n) in (SB . (Nseq . n)) by A24;

        then u in ((T . (Nseq . n)) /\ B) by A16, A32;

        then u in B by XBOOLE_0:def 4;

        hence thesis by A3;

      end;

      then

      consider fb be Real_Sequence such that

       A33: fb is subsequence of gb and

       A34: fb is convergent and

       A35: ( lim fb) in [.e, f.] by RCOMP_1:def 3;

      consider Nseq1 be increasing sequence of NAT such that

       A36: fb = (gb * Nseq1) by A33, VALUED_0:def 17;

      set fa = (ga * Nseq1), r = ((( lim fa) + ( lim fb)) / 2);

      set d0 = ( dist (A,B)), ff = ((1 / 2) (#) (fa + fb));



       A37: fa is convergent by A28, SEQ_4: 16;

      then

       A38: (fa + fb) is convergent by A34, SEQ_2: 5;

      then

       A39: ff is convergent by SEQ_2: 7;

      (T . 0 ) meets A by A13;

      then A is non empty;

      then d0 > 0 by A1, A14, Th11;

      then

       A40: (d0 / 2) > 0 by XREAL_1: 139;

      r = ((1 / 2) * (( lim fa) + ( lim fb)))

      .= ((1 / 2) * ( lim (fa + fb))) by A34, A37, SEQ_2: 6

      .= ( lim ff) by A38, SEQ_2: 8;

      then

      consider k0 be Nat such that

       A41: for i be Nat st k0 <= i holds |.((ff . i) - r).| < (d0 / 2) by A39, A40, SEQ_2:def 7;



       A42: k0 in NAT by ORDINAL1:def 12;

      take r;

      ( lim fa) = ( lim ga) by A28, SEQ_4: 17;

      hence r in [.e, f.] by A29, A35, Th1;

      now

        set i = (Nseq . (Nseq1 . k0)), di = ( dist ((SA . i),(SB . i)));



         A43: (2 * |.((((sa . i) + (sb . i)) / 2) - r).|) = ( |.2.| * |.((((sa . i) + (sb . i)) / 2) - r).|) by ABSVALUE:def 1

        .= |.(2 * ((((sa . i) + (sb . i)) / 2) - r)).| by COMPLEX1: 65

        .= |.(((sa . i) + (sb . i)) - (2 * r)).|;



         A44: (fa . k0) = (ga . (Nseq1 . k0)) by FUNCT_2: 15, A42

        .= (sa . i) by A30, FUNCT_2: 15;

        (T . i) meets B by A13;

        then ((T . i) /\ B) <> {} ;

        then

         A45: (SB . i) is non empty by A16;



         A46: (SB . i) = ((T . i) /\ B) by A16;

        then

         A47: (SB . i) c= B by XBOOLE_1: 17;



         A48: (SB . i) c= (T . i) by A46, XBOOLE_1: 17;



         A49: (SA . i) = ((T . i) /\ A) by A15;

        then

         A50: (SA . i) c= A by XBOOLE_1: 17;

        (T . i) meets A by A13;

        then ((T . i) /\ A) <> {} ;

        then

         A51: (SA . i) is non empty by A15;

        then

         A52: d0 <= di by A45, A50, A47, Th8;

        (d0 / 2) <= (di / 2) by A51, A45, A50, A47, Th8, XREAL_1: 72;

        then

         A53: ((di / 2) + (d0 / 2)) <= ((di / 2) + (di / 2)) by XREAL_1: 6;

        (ff . k0) = ((1 / 2) * ((fa + fb) . k0)) by SEQ_1: 9

        .= (((fa + fb) . k0) / 2)

        .= (((fa . k0) + (fb . k0)) / 2) by SEQ_1: 7;

        then

         A54: |.((((fa . k0) + (fb . k0)) / 2) - r).| < (d0 / 2) by A41;

        (T . i) is non empty closed_interval by A13;

        then

         A55: ex a,b be Real st a <= b & (T . i) = [.a, b.] by MEASURE5: 14;



         A56: (sb . i) in (SB . i) by A24;



         A57: (SA . i) c= (T . i) by A49, XBOOLE_1: 17;



         A58: (fb . k0) = (gb . (Nseq1 . k0)) by A36, FUNCT_2: 15, A42

        .= (sb . i) by FUNCT_2: 15;

        (2 * (d0 / 2)) = d0;

        then

         A59: (2 * |.((((sa . i) + (sb . i)) / 2) - r).|) < d0 by A54, A44, A58, XREAL_1: 68;



         A60: (sa . i) in (SA . i) by A24;

        then

         A61: di <= |.((sb . i) - (sa . i)).| by A56, Th7;

         A62:

        now

          per cases ;

            suppose (sa . i) <= (sb . i);

            then ((sb . i) - (sa . i)) >= 0 by XREAL_1: 48;

            then di <= ((sb . i) - (sa . i)) by A61, ABSVALUE:def 1;

            then d0 <= ((sb . i) - (sa . i)) by A52, XXREAL_0: 2;

            then |.(((sa . i) + (sb . i)) - (2 * r)).| <= ((sb . i) - (sa . i)) by A59, A43, XXREAL_0: 2;

            then

             A63: r in [.(sa . i), (sb . i).] by RCOMP_1: 2;

             [.(sa . i), (sb . i).] c= (T . i) by A55, A60, A56, A57, A48, XXREAL_2:def 12;

            hence r in (T . i) by A63;

          end;

            suppose

             A64: (sb . i) <= (sa . i);



             A65: |.((sb . i) - (sa . i)).| = |.((sa . i) - (sb . i)).| by UNIFORM1: 11;

            ((sa . i) - (sb . i)) >= 0 by A64, XREAL_1: 48;

            then di <= ((sa . i) - (sb . i)) by A61, A65, ABSVALUE:def 1;

            then d0 <= ((sa . i) - (sb . i)) by A52, XXREAL_0: 2;

            then |.(((sb . i) + (sa . i)) - (2 * r)).| <= ((sa . i) - (sb . i)) by A59, A43, XXREAL_0: 2;

            then

             A66: r in [.(sb . i), (sa . i).] by RCOMP_1: 2;

             [.(sb . i), (sa . i).] c= (T . i) by A55, A60, A56, A57, A48, XXREAL_2:def 12;

            hence r in (T . i) by A66;

          end;

        end;

        assume

         A67: r in (A \/ B);

        per cases by A67, XBOOLE_0:def 3;

          suppose

           A68: r in B;

          (SB . i) = ((T . i) /\ B) by A16;

          then

           A69: r in (SB . i) by A62, A68, XBOOLE_0:def 4;



           A70: |.(((fa . k0) - (fb . k0)) / 2).| = ( |.((fa . k0) - (fb . k0)).| / |.2.|) by COMPLEX1: 67

          .= ( |.((fa . k0) - (fb . k0)).| / 2) by ABSVALUE:def 1;

          ((fa . k0) - r) = ((((fa . k0) - (fb . k0)) / 2) + ((((fa . k0) + (fb . k0)) / 2) - r));

          then

           A71: |.((fa . k0) - r).| <= ( |.(((fa . k0) - (fb . k0)) / 2).| + |.((((fa . k0) + (fb . k0)) / 2) - r).|) by COMPLEX1: 56;

          ( |.(((fa . k0) - (fb . k0)) / 2).| + |.((((fa . k0) + (fb . k0)) / 2) - r).|) < ( |.(((fa . k0) - (fb . k0)) / 2).| + (d0 / 2)) by A54, XREAL_1: 6;

          then |.((fa . k0) - r).| < (( |.((fa . k0) - (fb . k0)).| / 2) + (d0 / 2)) by A71, A70, XXREAL_0: 2;

          then |.((fa . k0) - r).| < ((di / 2) + (d0 / 2)) by A24, A44, A58;

          then

           A72: |.((fa . k0) - r).| < di by A53, XXREAL_0: 2;

          (fa . k0) in (SA . i) by A24, A44;

          hence contradiction by A69, A72, Th7;

        end;

          suppose

           A73: r in A;

          (SA . i) = ((T . i) /\ A) by A15;

          then

           A74: r in (SA . i) by A62, A73, XBOOLE_0:def 4;



           A75: |.(((fb . k0) - (fa . k0)) / 2).| = ( |.((fb . k0) - (fa . k0)).| / |.2.|) by COMPLEX1: 67

          .= ( |.((fb . k0) - (fa . k0)).| / 2) by ABSVALUE:def 1;

          ((fb . k0) - r) = ((((fb . k0) - (fa . k0)) / 2) + ((((fb . k0) + (fa . k0)) / 2) - r));

          then

           A76: |.((fb . k0) - r).| <= ( |.(((fb . k0) - (fa . k0)) / 2).| + |.((((fb . k0) + (fa . k0)) / 2) - r).|) by COMPLEX1: 56;



           A77: |.((fb . k0) - (fa . k0)).| = |.((fa . k0) - (fb . k0)).| by UNIFORM1: 11

          .= di by A24, A44, A58;

          ( |.(((fb . k0) - (fa . k0)) / 2).| + |.((((fb . k0) + (fa . k0)) / 2) - r).|) < ( |.(((fb . k0) - (fa . k0)) / 2).| + (d0 / 2)) by A54, XREAL_1: 6;

          then |.((fb . k0) - r).| < (( |.((fb . k0) - (fa . k0)).| / 2) + (d0 / 2)) by A76, A75, XXREAL_0: 2;

          then

           A78: |.((fb . k0) - r).| < di by A53, A77, XXREAL_0: 2;

          (fb . k0) in (SB . i) by A24, A58;

          hence contradiction by A74, A78, Th7;

        end;

      end;

      hence not r in (A \/ B);

      let i be Nat;

      set k = ( max (k0,i));



       A79: k in NAT by ORDINAL1:def 12;

      take j = (Nseq . (Nseq1 . k));



       A80: (fb . k) = (gb . (Nseq1 . k)) by A36, FUNCT_2: 15, A79

      .= (sb . j) by FUNCT_2: 15;



       A81: i <= k by XXREAL_0: 25;



       A82: (sb . j) in (SB . j) by A24;

      (T . j) meets B by A13;

      then ((T . j) /\ B) <> {} ;

      then

       A83: (SB . j) is non empty by A16;



       A84: ( dom Nseq) = NAT by FUNCT_2:def 1;

      (T . j) meets A by A13;

      then ((T . j) /\ A) <> {} ;

      then

       A85: (SA . j) is non empty by A15;



       A86: i <= (Nseq . i) by SEQM_3: 14;



       A87: (SA . j) = ((T . j) /\ A) by A15;

      then

       A88: (SA . j) c= (T . j) by XBOOLE_1: 17;

      (ff . k) = ((1 / 2) * ((fa + fb) . k)) by A79, SEQ_1: 9

      .= (((fa + fb) . k) / 2)

      .= (((fa . k) + (fb . k)) / 2) by A79, SEQ_1: 7;

      then

       A89: |.((((fa . k) + (fb . k)) / 2) - r).| < (d0 / 2) by A41, A79, XXREAL_0: 25;



       A90: (2 * (d0 / 2)) = d0;

      (fa . k) = (ga . (Nseq1 . k)) by FUNCT_2: 15, A79

      .= (sa . j) by A30, FUNCT_2: 15;

      then

       A91: (2 * |.((((sa . j) + (sb . j)) / 2) - r).|) < d0 by A89, A80, A90, XREAL_1: 68;

      (T . j) is non empty closed_interval by A13;

      then

       A92: ex a,b be Real st a <= b & (T . j) = [.a, b.] by MEASURE5: 14;



       A93: (SB . j) = ((T . j) /\ B) by A16;

      then

       A94: (SB . j) c= B by XBOOLE_1: 17;



       A95: (SB . j) c= (T . j) by A93, XBOOLE_1: 17;



       A96: i in NAT by ORDINAL1:def 12;

      ( dom Nseq1) = NAT by FUNCT_2:def 1;

      then (Nseq1 . i) <= (Nseq1 . k) by A81, VALUED_0:def 15, A79, A96;

      then

       A97: (Nseq . (Nseq1 . i)) <= j by A84, VALUED_0:def 15;

      i <= (Nseq1 . i) by SEQM_3: 14;

      then (Nseq . i) <= (Nseq . (Nseq1 . i)) by A84, VALUED_0:def 15, A96;

      then i <= (Nseq . (Nseq1 . i)) by A86, XXREAL_0: 2;

      hence i <= j by A97, XXREAL_0: 2;

      set di = ( dist ((SA . j),(SB . j)));



       A98: (2 * |.((((sa . j) + (sb . j)) / 2) - r).|) = ( |.2.| * |.((((sa . j) + (sb . j)) / 2) - r).|) by ABSVALUE:def 1

      .= |.(2 * ((((sa . j) + (sb . j)) / 2) - r)).| by COMPLEX1: 65

      .= |.(((sa . j) + (sb . j)) - (2 * r)).|;

      (SA . j) c= A by A87, XBOOLE_1: 17;

      then

       A99: d0 <= di by A85, A83, A94, Th8;



       A100: (sa . j) in (SA . j) by A24;

      then

       A101: di <= |.((sb . j) - (sa . j)).| by A82, Th7;

       A102:

      now

        per cases ;

          suppose (sa . j) <= (sb . j);

          then ((sb . j) - (sa . j)) >= 0 by XREAL_1: 48;

          then di <= ((sb . j) - (sa . j)) by A101, ABSVALUE:def 1;

          then d0 <= ((sb . j) - (sa . j)) by A99, XXREAL_0: 2;

          then |.(((sa . j) + (sb . j)) - (2 * r)).| <= ((sb . j) - (sa . j)) by A91, A98, XXREAL_0: 2;

          then

           A103: r in [.(sa . j), (sb . j).] by RCOMP_1: 2;

           [.(sa . j), (sb . j).] c= (T . j) by A92, A100, A82, A88, A95, XXREAL_2:def 12;

          hence r in (T . j) by A103;

        end;

          suppose

           A104: (sb . j) <= (sa . j);



           A105: |.((sb . j) - (sa . j)).| = |.((sa . j) - (sb . j)).| by UNIFORM1: 11;

          ((sa . j) - (sb . j)) >= 0 by A104, XREAL_1: 48;

          then di <= ((sa . j) - (sb . j)) by A101, A105, ABSVALUE:def 1;

          then d0 <= ((sa . j) - (sb . j)) by A99, XXREAL_0: 2;

          then |.(((sb . j) + (sa . j)) - (2 * r)).| <= ((sa . j) - (sb . j)) by A91, A98, XXREAL_0: 2;

          then

           A106: r in [.(sb . j), (sa . j).] by RCOMP_1: 2;

           [.(sb . j), (sa . j).] c= (T . j) by A92, A100, A82, A88, A95, XXREAL_2:def 12;

          hence r in (T . j) by A106;

        end;

      end;

      (T . j) c= (S . j) by A13;

      hence thesis by A102;

    end;

    theorem :: JCT_MISC:13



     Th13: for S be closed Subset of ( TOP-REAL 2) st S is bounded holds ( proj2 .: S) is closed

    proof

      let S be closed Subset of ( TOP-REAL 2);

      assume S is bounded;



      then ( Cl ( proj2 .: S)) = ( proj2 .: ( Cl S)) by TOPREAL6: 84

      .= ( proj2 .: S) by PRE_TOPC: 22;

      hence thesis;

    end;

    theorem :: JCT_MISC:14



     Th14: for S be Subset of ( TOP-REAL 2) st S is bounded holds ( proj2 .: S) is real-bounded

    proof

      let S be Subset of ( TOP-REAL 2);

      assume S is bounded;

      then

      reconsider C = S as bounded Subset of ( Euclid 2) by JORDAN2C: 11;

      consider r be Real, x be Point of ( Euclid 2) such that

       A1: 0 < r and

       A2: C c= ( Ball (x,r)) by METRIC_6:def 3;

      reconsider P = ( Ball (x,r)) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

      reconsider p = x as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      set t = ( max ( |.((p `2 ) - r).|, |.((p `2 ) + r).|));

      now

        assume that

         A3: |.((p `2 ) - r).| <= 0 and

         A4: |.((p `2 ) + r).| <= 0 ;

         |.((p `2 ) - r).| = 0 by A3, COMPLEX1: 46;

        then |.(r - (p `2 )).| = 0 by UNIFORM1: 11;

        then

         A5: (r - (p `2 )) = 0 by ABSVALUE: 2;

         |.((p `2 ) + r).| = 0 by A4, COMPLEX1: 46;

        hence contradiction by A1, A5, ABSVALUE: 2;

      end;

      then

       A6: t > 0 by XXREAL_0: 30;



       A7: ( proj2 .: P) = ].((p `2 ) - r), ((p `2 ) + r).[ by TOPREAL6: 44;

      for s st s in ( proj2 .: S) holds |.s.| < t

      proof

        let s;

        ( proj2 .: S) c= ( proj2 .: P) by A2, RELAT_1: 123;

        hence thesis by A7, Th3;

      end;

      hence thesis by A6, SEQ_4: 4;

    end;

    theorem :: JCT_MISC:15

    for S be compact Subset of ( TOP-REAL 2) holds ( proj2 .: S) is compact

    proof

      let S be compact Subset of ( TOP-REAL 2);

      ( proj2 .: S) is closed by Th13;

      hence thesis by Th14, RCOMP_1: 11;

    end;