urysohn2.miz



    begin

    theorem :: URYSOHN2:1

    

     Th1: for A be Subset of REAL , x be Real st x <> 0 holds ((x " ) ** (x ** A)) = A

    proof

      let A be Subset of REAL ;

      let x be Real;

      assume

       A1: x <> 0 ;

      thus ((x " ) ** (x ** A)) c= A

      proof

        let y be object;

        assume

         A2: y in ((x " ) ** (x ** A));

        consider z be Real such that

         A3: z in (x ** A) and

         A4: y = ((x " ) * z) by A2, INTEGRA2: 39;

        consider t be Real such that

         A5: t in A and

         A6: z = (x * t) by A3, INTEGRA2: 39;

        y = (((x " ) * x) * t) by A4, A6

        .= (1 * t) by A1, XCMPLX_0:def 7

        .= t;

        hence thesis by A5;

      end;

      let y be object;

      assume

       A7: y in A;

      then

      reconsider y as Real;

      set t = (y / (x " ));

      

       A8: t in (x ** A) by A7, MEMBER_1: 193;

      y = ((x " ) * t) by A1, XCMPLX_1: 87, XCMPLX_1: 202;

      hence thesis by A8, MEMBER_1: 193;

    end;

    theorem :: URYSOHN2:2

    

     Th2: for x be Real st x <> 0 holds for A be Subset of REAL holds A = REAL implies (x ** A) = A

    proof

      let x be Real;

      assume

       A1: x <> 0 ;

      let A be Subset of REAL ;

      assume

       A2: A = REAL ;

      for y be object st y in A holds y in (x ** A)

      proof

        let y be object;

        assume y in A;

        then

        reconsider y as Real;

        reconsider z = (y / x) as Element of REAL by XREAL_0:def 1;

        y = (x * z) by A1, XCMPLX_1: 87;

        hence thesis by A2, MEMBER_1: 193;

      end;

      then A c= (x ** A);

      hence thesis by A2;

    end;

    theorem :: URYSOHN2:3

    

     Th3: for A be Subset of REAL st A <> {} holds ( 0 ** A) = { 0 }

    proof

      let A be Subset of REAL ;

      assume

       A1: A <> {} ;

      

       A2: { 0 } c= ( 0 ** A)

      proof

        let y be object;

        consider t be object such that

         A3: t in A by A1, XBOOLE_0:def 1;

        reconsider t as Element of A by A3;

        reconsider t as Real;

        assume y in { 0 };

        then y = ( 0 * t) by TARSKI:def 1;

        hence thesis by A3, MEMBER_1: 193;

      end;

      ( 0 ** A) c= { 0 }

      proof

        let y be object;

        assume

         A4: y in ( 0 ** A);

        then

        reconsider y as Real;

        ex z be Real st z in A & y = ( 0 * z) by A4, INTEGRA2: 39;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by A2;

    end;

    theorem :: URYSOHN2:4

    for x be Real holds (x ** {} ) = {} ;

    theorem :: URYSOHN2:5

    

     Th5: for a,b be R_eal st a <= b holds a = -infty & b = -infty or a = -infty & b in REAL or a = -infty & b = +infty or a in REAL & b in REAL or a in REAL & b = +infty or a = +infty & b = +infty

    proof

      let a,b be R_eal;

      a in REAL or a in { -infty , +infty } by XBOOLE_0:def 3, XXREAL_0:def 4;

      then

       A1: a in REAL or a = -infty or a = +infty by TARSKI:def 2;

      b in REAL or b in { -infty , +infty } by XBOOLE_0:def 3, XXREAL_0:def 4;

      then

       A2: b in REAL or b = -infty or b = +infty by TARSKI:def 2;

      assume a <= b;

      hence thesis by A1, A2, XXREAL_0: 9, XXREAL_0: 12;

    end;

    theorem :: URYSOHN2:6

    

     Th6: for A be Interval holds ( 0 ** A) is interval

    proof

      let A be Interval;

      per cases ;

        suppose A = {} ;

        hence thesis;

      end;

        suppose A <> {} ;

        then ( 0 ** A) = { 0 } by Th3;

        then ( 0 ** A) = [. 0 , 0 .] by XXREAL_1: 17;

        hence thesis;

      end;

    end;

    theorem :: URYSOHN2:7

    

     Th7: for A be non empty Interval, x be Real st x <> 0 holds A is open_interval implies (x ** A) is open_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: x <> 0 ;

      assume

       A2: A is open_interval;

      then

      consider a,b be R_eal such that

       A3: A = ].a, b.[ by MEASURE5:def 2;

      

       A4: a < b by A3, XXREAL_1: 28;

      now

        per cases ;

          case

           A5: x < 0 ;

          now

            per cases by A4, Th5;

              case a = -infty & b = -infty ;

              then ].a, b.[ = {} ;

              then (x ** A) = {} by A3;

              hence thesis;

            end;

              case

               A6: a = -infty & b in REAL ;

              then

              reconsider s = b as Real;

              set c = +infty ;

              (x * s) is R_eal by XXREAL_0:def 1;

              then

              consider d be R_eal such that

               A7: d = (x * s);

              

               A8: ].d, c.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A9: q in ].d, c.[;

                then

                reconsider q as Real;

                reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

                reconsider q1 = q as R_eal by XXREAL_0:def 1;

                

                 A10: d < q1 by A9, MEASURE5:def 1;

                

                 A11: q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  (x * q2) = q by A1, XCMPLX_1: 87;

                  then

                   A12: q3 < b by A5, A7, A10, XREAL_1: 65;

                  a < q3 by A6, XXREAL_0: 12;

                  hence thesis by A3, A12, MEASURE5:def 1;

                end;

                q = (x * (q / x)) by A1, XCMPLX_1: 87;

                hence thesis by A11, MEMBER_1: 193;

              end;

              (x ** A) c= ].d, c.[

              proof

                let q be object;

                assume

                 A13: q in (x ** A);

                then

                reconsider q as Element of REAL ;

                consider z2 be Real such that

                 A14: z2 in A and

                 A15: q = (x * z2) by A13, INTEGRA2: 39;

                reconsider q as R_eal by XXREAL_0:def 1;

                

                 A16: q < +infty by XXREAL_0: 9;

                reconsider z2 as R_eal by XXREAL_0:def 1;

                z2 < b by A3, A14, MEASURE5:def 1;

                then

                consider r,o be Real such that

                 A17: r = z2 & o = b and r <= o by A6;

                reconsider o1 = (x * o), r1 = (x * r) as R_eal by XXREAL_0:def 1;

                r < o by A3, A14, A17, MEASURE5:def 1;

                then o1 < r1 by A5, XREAL_1: 69;

                hence thesis by A7, A15, A17, A16, MEASURE5:def 1;

              end;

              then (x ** A) = ].d, c.[ by A8;

              hence thesis by MEASURE5:def 2;

            end;

              case a = -infty & b = +infty ;

              hence thesis by A2, A3, A5, Th2, XXREAL_1: 224;

            end;

              case

               A18: a in REAL & b in REAL ;

              then

              reconsider s = a, r = b as Real;

              reconsider d = (x * s), g = (x * r) as R_eal by XXREAL_0:def 1;

              

               A19: ].g, d.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A20: q in ].g, d.[;

                then

                reconsider q as Real;

                set q2 = (q / x);

                reconsider q1 = q as R_eal by XXREAL_0:def 1;

                

                 A21: q1 < d by A20, MEASURE5:def 1;

                

                 A22: g < q1 by A20, MEASURE5:def 1;

                

                 A23: q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  (x * q2) = q by A1, XCMPLX_1: 87;

                  then

                   A24: a < q3 by A5, A21, XREAL_1: 65;

                  (q / x) < ((x * r) / x) by A5, A22, XREAL_1: 75;

                  then q3 < b by A5, XCMPLX_1: 89;

                  hence thesis by A3, A24, MEASURE5:def 1;

                end;

                q = (x * (q / x)) by A1, XCMPLX_1: 87;

                hence thesis by A23, MEMBER_1: 193;

              end;

              (x ** A) c= ].g, d.[

              proof

                let q be object;

                assume

                 A25: q in (x ** A);

                then

                reconsider q as Real;

                consider z2 be Real such that

                 A26: z2 in A and

                 A27: q = (x * z2) by A25, INTEGRA2: 39;

                reconsider z2 as R_eal by XXREAL_0:def 1;

                a < z2 by A3, A26, MEASURE5:def 1;

                then

                consider 1o,1ra be Real such that

                 A28: 1o = a & 1ra = z2 and 1o <= 1ra by A18;

                z2 < b by A3, A26, MEASURE5:def 1;

                then

                consider 2o,2r be Real such that

                 A29: 2o = z2 & 2r = b and 2o <= 2r by A18;

                reconsider 1o1 = (x * 1o), 1r1 = (x * 1ra), 2o1 = (x * 2o), 2r1 = (x * 2r) as R_eal by XXREAL_0:def 1;

                2o < 2r by A3, A26, A29, MEASURE5:def 1;

                then

                 A30: 2r1 < 2o1 by A5, XREAL_1: 69;

                1o < 1ra by A3, A26, A28, MEASURE5:def 1;

                then 1r1 < 1o1 by A5, XREAL_1: 69;

                hence thesis by A27, A28, A29, A30, MEASURE5:def 1;

              end;

              then (x ** A) = ].g, d.[ by A19;

              hence thesis by MEASURE5:def 2;

            end;

              case

               A31: a in REAL & b = +infty ;

              then

              reconsider s = a as Real;

              set c = -infty ;

              reconsider d = (x * s) as R_eal by XXREAL_0:def 1;

              

               A32: ].c, d.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A33: q in ].c, d.[;

                then

                reconsider q as Real;

                reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

                reconsider q1 = q as R_eal by XXREAL_0:def 1;

                

                 A34: q = (x * (q / x)) by A1, XCMPLX_1: 87;

                q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  q1 <= d by A33, MEASURE5:def 1;

                  then (x * q2) < (x * s) by A33, A34, MEASURE5:def 1;

                  then

                   A35: a < q3 by A5, XREAL_1: 65;

                  q3 < b by A31, XXREAL_0: 9;

                  hence thesis by A3, A35, MEASURE5:def 1;

                end;

                hence thesis by A34, MEMBER_1: 193;

              end;

              (x ** A) c= ].c, d.[

              proof

                let q be object;

                assume

                 A36: q in (x ** A);

                then

                reconsider q as Element of REAL ;

                consider z2 be Real such that

                 A37: z2 in A and

                 A38: q = (x * z2) by A36, INTEGRA2: 39;

                reconsider z2, q as R_eal by XXREAL_0:def 1;

                a < z2 by A3, A37, MEASURE5:def 1;

                then

                consider o,r be Real such that

                 A39: o = a & r = z2 and o <= r by A31;

                reconsider o1 = (x * o), r1 = (x * r) as R_eal by XXREAL_0:def 1;

                

                 A40: -infty < q by XXREAL_0: 12;

                o < r by A3, A37, A39, MEASURE5:def 1;

                then r1 < o1 by A5, XREAL_1: 69;

                hence thesis by A38, A39, A40, MEASURE5:def 1;

              end;

              then (x ** A) = ].c, d.[ by A32;

              hence thesis by MEASURE5:def 2;

            end;

              case a = +infty & b = +infty ;

              then ].a, b.[ = {} ;

              then (x ** A) = {} by A3;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          case x = 0 ;

          hence thesis by A1;

        end;

          case

           A41: 0 < x;

          now

            per cases by A4, Th5;

              case a = -infty & b = -infty ;

              then ].a, b.[ = {} ;

              then (x ** A) = {} by A3;

              hence thesis;

            end;

              case

               A42: a = -infty & b in REAL ;

              then

              reconsider s = b as Real;

              set c = -infty ;

              reconsider d = (x * s) as R_eal by XXREAL_0:def 1;

              

               A43: ].c, d.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A44: q in ].c, d.[;

                then

                reconsider q as Real;

                reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

                reconsider q1 = q as R_eal by XXREAL_0:def 1;

                

                 A45: q1 < d by A44, MEASURE5:def 1;

                

                 A46: q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  (x * q2) = q by A1, XCMPLX_1: 87;

                  then

                   A47: q3 < b by A41, A45, XREAL_1: 64;

                  a < q3 by A42, XXREAL_0: 12;

                  hence thesis by A3, A47, MEASURE5:def 1;

                end;

                q = (x * (q / x)) by A1, XCMPLX_1: 87;

                hence thesis by A46, MEMBER_1: 193;

              end;

              (x ** A) c= ].c, d.[

              proof

                let q be object;

                assume

                 A48: q in (x ** A);

                then

                reconsider q as Element of REAL ;

                consider z2 be Real such that

                 A49: z2 in A and

                 A50: q = (x * z2) by A48, INTEGRA2: 39;

                reconsider z2, q as R_eal by XXREAL_0:def 1;

                z2 < b by A3, A49, MEASURE5:def 1;

                then

                consider r,o be Real such that

                 A51: r = z2 & o = b and r <= o by A42;

                reconsider o1 = (x * o), r1 = (x * r) as R_eal by XXREAL_0:def 1;

                

                 A52: -infty < q by XXREAL_0: 12;

                r < o by A3, A49, A51, MEASURE5:def 1;

                then r1 < o1 by A41, XREAL_1: 68;

                hence thesis by A50, A51, A52, MEASURE5:def 1;

              end;

              then (x ** A) = ].c, d.[ by A43;

              hence thesis by MEASURE5:def 2;

            end;

              case a = -infty & b = +infty ;

              hence thesis by A2, A3, A41, Th2, XXREAL_1: 224;

            end;

              case

               A53: a in REAL & b in REAL ;

              then

              reconsider s = a, r = b as Real;

              reconsider d = (x * s) as R_eal by XXREAL_0:def 1;

              reconsider g = (x * r) as R_eal by XXREAL_0:def 1;

              

               A54: ].d, g.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A55: q in ].d, g.[;

                then

                reconsider q as Real;

                set q2 = (q / x);

                q is R_eal by XXREAL_0:def 1;

                then

                consider q1 be R_eal such that

                 A56: q1 = q;

                

                 A57: q1 < g by A55, A56, MEASURE5:def 1;

                

                 A58: d < q1 by A55, A56, MEASURE5:def 1;

                

                 A59: q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  (x * q2) = q by A1, XCMPLX_1: 87;

                  then

                   A60: a < q3 by A41, A56, A58, XREAL_1: 64;

                  (q / x) < ((x * r) / x) by A41, A56, A57, XREAL_1: 74;

                  then q3 < b by A41, XCMPLX_1: 89;

                  hence thesis by A3, A60, MEASURE5:def 1;

                end;

                q = (x * (q / x)) by A1, XCMPLX_1: 87;

                hence thesis by A59, MEMBER_1: 193;

              end;

              (x ** A) c= ].d, g.[

              proof

                let q be object;

                assume

                 A61: q in (x ** A);

                then

                reconsider q as Real;

                consider z2 be Real such that

                 A62: z2 in A and

                 A63: q = (x * z2) by A61, INTEGRA2: 39;

                reconsider z2 as R_eal by XXREAL_0:def 1;

                z2 < b by A3, A62, MEASURE5:def 1;

                then

                consider 2o,2r be Real such that

                 A64: 2o = z2 & 2r = b and 2o <= 2r by A53;

                reconsider 2o1 = (x * 2o), 2r1 = (x * 2r) as R_eal by XXREAL_0:def 1;

                2o < 2r by A3, A62, A64, MEASURE5:def 1;

                then

                 A65: 2o1 < 2r1 by A41, XREAL_1: 68;

                a < z2 by A3, A62, MEASURE5:def 1;

                then

                consider 1o,1ra be Real such that

                 A66: 1o = a & 1ra = z2 and 1o <= 1ra by A53;

                reconsider 1o1 = (x * 1o), 1r1 = (x * 1ra) as R_eal by XXREAL_0:def 1;

                1o < 1ra by A3, A62, A66, MEASURE5:def 1;

                then 1o1 < 1r1 by A41, XREAL_1: 68;

                hence thesis by A63, A66, A64, A65, MEASURE5:def 1;

              end;

              then (x ** A) = ].d, g.[ by A54;

              hence thesis by MEASURE5:def 2;

            end;

              case

               A67: a in REAL & b = +infty ;

              then

              reconsider s = a as Element of REAL ;

              set c = +infty ;

              reconsider d = (x * s) as R_eal by XXREAL_0:def 1;

              

               A68: (x ** A) c= ].d, c.[

              proof

                let q be object;

                assume

                 A69: q in (x ** A);

                then

                reconsider q as Element of REAL ;

                consider z2 be Real such that

                 A70: z2 in A and

                 A71: q = (x * z2) by A69, INTEGRA2: 39;

                reconsider q as R_eal by XXREAL_0:def 1;

                

                 A72: q < +infty by XXREAL_0: 9;

                reconsider z2 as R_eal by XXREAL_0:def 1;

                a < z2 by A3, A70, MEASURE5:def 1;

                then

                consider o,r be Real such that

                 A73: o = a & r = z2 and o <= r by A67;

                reconsider o1 = (x * o), r1 = (x * r) as R_eal by XXREAL_0:def 1;

                o < r by A3, A70, A73, MEASURE5:def 1;

                then o1 < r1 by A41, XREAL_1: 68;

                hence thesis by A71, A73, A72, MEASURE5:def 1;

              end;

               ].d, c.[ c= (x ** A)

              proof

                let q be object;

                assume

                 A74: q in ].d, c.[;

                then

                reconsider q as Real;

                reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

                reconsider q1 = q as R_eal by XXREAL_0:def 1;

                

                 A75: q = (x * (q / x)) by A1, XCMPLX_1: 87;

                

                 A76: d < q1 by A74, MEASURE5:def 1;

                q2 in A

                proof

                  reconsider q3 = q2 as R_eal;

                  a < q3 & q3 < b by A41, A67, A76, A75, XREAL_1: 64, XXREAL_0: 9;

                  hence thesis by A3, MEASURE5:def 1;

                end;

                hence thesis by A75, MEMBER_1: 193;

              end;

              then (x ** A) = ].d, c.[ by A68;

              hence thesis by MEASURE5:def 2;

            end;

              case a = +infty & b = +infty ;

              then ].a, b.[ = {} ;

              then (x ** A) = {} by A3;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:8

    

     Th8: for A be non empty Interval, x be Real st x <> 0 holds A is closed_interval implies (x ** A) is closed_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: x <> 0 ;

      assume A is closed_interval;

      then

      consider a,b be Real such that

       A2: A = [.a, b.] by MEASURE5:def 3;

      reconsider a, b as R_eal by XXREAL_0:def 1;

      now

        per cases ;

          case

           A3: x < 0 ;

          now

            reconsider s = a, r = b as Real;

            reconsider d = (x * s) as R_eal by XXREAL_0:def 1;

            reconsider g = (x * r) as R_eal by XXREAL_0:def 1;

            

             A4: [.g, d.] c= (x ** A)

            proof

              let q be object;

              assume

               A5: q in [.g, d.];

              then

              reconsider q as Real;

              set q2 = (q / x);

              reconsider q1 = q as R_eal by XXREAL_0:def 1;

              

               A6: g <= q1 by A5, XXREAL_1: 1;

              

               A7: q2 in A

              proof

                reconsider q3 = q2 as R_eal;

                

                 A8: q3 <= b

                proof

                  consider p,o be Real such that

                   A9: p = g & o = q1 and

                   A10: p <= o by A6;

                  (o / x) <= (p / x) by A3, A10, XREAL_1: 73;

                  hence thesis by A3, A9, XCMPLX_1: 89;

                end;

                a <= q3

                proof

                  q1 <= d & (x * q2) = q by A1, A5, XCMPLX_1: 87, XXREAL_1: 1;

                  hence thesis by A3, XREAL_1: 69;

                end;

                hence thesis by A2, A8, XXREAL_1: 1;

              end;

              q = (x * (q / x)) by A1, XCMPLX_1: 87;

              hence thesis by A7, MEMBER_1: 193;

            end;

            (x ** A) c= [.g, d.]

            proof

              let q be object;

              assume

               A11: q in (x ** A);

              then

              reconsider q as Real;

              consider z2 be Real such that

               A12: z2 in A and

               A13: q = (x * z2) by A11, INTEGRA2: 39;

              reconsider z2 as R_eal by XXREAL_0:def 1;

              a <= z2 by A2, A12, XXREAL_1: 1;

              then

              consider 1o,1ra be Real such that

               A14: 1o = a & 1ra = z2 and

               A15: 1o <= 1ra;

              z2 <= b by A2, A12, XXREAL_1: 1;

              then

              consider 2o,2r be Real such that

               A16: 2o = z2 & 2r = b and

               A17: 2o <= 2r;

              

               A18: (x * 2r) <= (x * 2o) by A3, A17, XREAL_1: 65;

              (x * 1o) is R_eal & (x * 1ra) is R_eal by XXREAL_0:def 1;

              then

              consider 1o1,1r1 be R_eal such that

               A19: 1o1 = (x * 1o) & 1r1 = (x * 1ra);

              1r1 <= 1o1 by A3, A15, A19, XREAL_1: 65;

              hence thesis by A13, A14, A16, A18, A19, XXREAL_1: 1;

            end;

            then (x ** A) = [.g, d.] by A4;

            hence thesis by MEASURE5:def 3;

          end;

          hence thesis;

        end;

          case x = 0 ;

          hence thesis by A1;

        end;

          case

           A20: 0 < x;

          now

            per cases by Th5;

              case a in REAL & b in REAL ;

              reconsider r = b as Real;

              reconsider s = a as Real;

              reconsider g = (x * r) as R_eal by XXREAL_0:def 1;

              (x * s) is R_eal by XXREAL_0:def 1;

              then

              consider d be R_eal such that

               A21: d = (x * s);

              

               A22: [.d, g.] c= (x ** A)

              proof

                let q be object;

                assume

                 A23: q in [.d, g.];

                then

                reconsider q as Real by A21;

                set q2 = (q / x);

                q is R_eal by XXREAL_0:def 1;

                then

                consider q1 be R_eal such that

                 A24: q1 = q;

                

                 A25: q = (x * (q / x)) by A1, XCMPLX_1: 87;

                q2 in A

                proof

                  consider q3 be R_eal such that

                   A26: q3 = q2;

                  

                   A27: q3 <= b

                  proof

                    q1 <= g by A23, A24, XXREAL_1: 1;

                    then

                    consider p,o be Real such that

                     A28: p = q1 & o = g and

                     A29: p <= o by A24;

                    (p / x) <= (o / x) by A20, A29, XREAL_1: 72;

                    hence thesis by A20, A24, A26, A28, XCMPLX_1: 89;

                  end;

                  a <= q3

                  proof

                    d <= q1 by A23, A24, XXREAL_1: 1;

                    hence thesis by A20, A21, A24, A25, A26, XREAL_1: 68;

                  end;

                  hence thesis by A2, A26, A27, XXREAL_1: 1;

                end;

                hence thesis by A25, MEMBER_1: 193;

              end;

              (x ** A) c= [.d, g.]

              proof

                let q be object;

                assume

                 A30: q in (x ** A);

                then

                reconsider q as Real;

                consider z2 be Real such that

                 A31: z2 in A and

                 A32: q = (x * z2) by A30, INTEGRA2: 39;

                reconsider z2 as R_eal by XXREAL_0:def 1;

                a <= z2 by A2, A31, XXREAL_1: 1;

                then

                consider 1o,1ra be Real such that

                 A33: 1o = a & 1ra = z2 and

                 A34: 1o <= 1ra;

                z2 <= b by A2, A31, XXREAL_1: 1;

                then

                consider 2o,2r be Real such that

                 A35: 2o = z2 & 2r = b and

                 A36: 2o <= 2r;

                

                 A37: (x * 2o) <= (x * 2r) by A20, A36, XREAL_1: 64;

                (x * 1o) is R_eal & (x * 1ra) is R_eal by XXREAL_0:def 1;

                then

                consider 1o1,1r1 be R_eal such that

                 A38: 1o1 = (x * 1o) & 1r1 = (x * 1ra);

                1o1 <= 1r1 by A20, A34, A38, XREAL_1: 64;

                hence thesis by A21, A32, A33, A35, A37, A38, XXREAL_1: 1;

              end;

              then (x ** A) = [.d, g.] by A22;

              hence thesis by A21, MEASURE5:def 3;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:9

    

     Th9: for A be non empty Interval, x be Real st 0 < x holds A is right_open_interval implies (x ** A) is right_open_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      assume A is right_open_interval;

      then

      consider a be Real, b be R_eal such that

       A2: A = [.a, b.[ by MEASURE5:def 4;

      

       A3: a < b by A2, XXREAL_1: 27;

      reconsider a as R_eal by XXREAL_0:def 1;

      now

        per cases by A3, Th5;

          case a = -infty & b = -infty ;

          hence thesis;

        end;

          case a = -infty & b in REAL ;

          hence thesis;

        end;

          case a = -infty & b = +infty ;

          hence thesis;

        end;

          case

           A4: a in REAL & b in REAL ;

          then

          consider r be Real such that

           A5: r = b;

          (x * r) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A6: g = (x * r);

          consider s be Real such that

           A7: s = a;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A8: d = (x * s);

          

           A9: [.d, g.[ c= (x ** A)

          proof

            let q be object;

            assume

             A10: q in [.d, g.[;

            then

            reconsider q as Real by A8;

            set q2 = (q / x);

            q is R_eal by XXREAL_0:def 1;

            then

            consider q1 be R_eal such that

             A11: q1 = q;

            

             A12: q2 in A

            proof

              consider q3 be R_eal such that

               A13: q3 = q2;

              

               A14: q3 < b

              proof

                q1 <= g by A10, A11, XXREAL_1: 3;

                then

                consider p,o be Real such that

                 A15: p = q1 & o = g and p <= o by A6, A11;

                p < o by A10, A11, A15, XXREAL_1: 3;

                then (p / x) < (o / x) by A1, XREAL_1: 74;

                hence thesis by A1, A5, A6, A11, A13, A15, XCMPLX_1: 89;

              end;

              a <= q3

              proof

                d <= q1 & (x * q2) = q by A1, A10, A11, XCMPLX_1: 87, XXREAL_1: 3;

                hence thesis by A1, A7, A8, A11, A13, XREAL_1: 68;

              end;

              hence thesis by A2, A13, A14, XXREAL_1: 3;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A12, MEMBER_1: 193;

          end;

          (x ** A) c= [.d, g.[

          proof

            let q be object;

            assume

             A16: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A17: z2 in A and

             A18: q = (x * z2) by A16, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            z2 <= b by A2, A17, XXREAL_1: 3;

            then

            consider 2o,2r be Real such that

             A19: 2o = z2 & 2r = b and 2o <= 2r by A4;

            (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

            then

            consider 2o1,2r1 be R_eal such that

             A20: 2o1 = (x * 2o) & 2r1 = (x * 2r);

            2o < 2r by A2, A17, A19, XXREAL_1: 3;

            then

             A21: 2o1 < 2r1 by A1, A20, XREAL_1: 68;

            a <= z2 by A2, A17, XXREAL_1: 3;

            then

            consider 1o,1ra be Real such that

             A22: 1o = a & 1ra = z2 and

             A23: 1o <= 1ra;

            (x * 1o) <= (x * 1ra) by A1, A23, XREAL_1: 64;

            hence thesis by A7, A5, A8, A6, A18, A22, A19, A20, A21, XXREAL_1: 3;

          end;

          then (x ** A) = [.d, g.[ by A9;

          hence thesis by A8, MEASURE5:def 4;

        end;

          case

           A24: a in REAL & b = +infty ;

          consider s be Real such that

           A25: s = a;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A26: d = (x * s);

          consider c be R_eal such that

           A27: c = +infty ;

          

           A28: [.d, c.[ c= (x ** A)

          proof

            let q be object;

            assume

             A29: q in [.d, c.[;

            then

            reconsider q as Real by A26;

            reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

            q is R_eal by XXREAL_0:def 1;

            then

            consider q1 be R_eal such that

             A30: q1 = q;

            

             A31: q2 in A

            proof

              consider q3 be R_eal such that

               A32: q3 = q2;

              

               A33: a <= q3

              proof

                d <= q1 & (x * q2) = q by A1, A29, A30, XCMPLX_1: 87, XXREAL_1: 3;

                hence thesis by A1, A25, A26, A30, A32, XREAL_1: 68;

              end;

              q3 < b by A24, A32, XXREAL_0: 9;

              hence thesis by A2, A32, A33, XXREAL_1: 3;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A31, MEMBER_1: 193;

          end;

          (x ** A) c= [.d, c.[

          proof

            let q be object;

            assume

             A34: q in (x ** A);

            then

            reconsider q as Element of REAL ;

            consider z2 be Real such that

             A35: z2 in A and

             A36: q = (x * z2) by A34, INTEGRA2: 39;

            reconsider q as R_eal by XXREAL_0:def 1;

            

             A37: q < +infty by XXREAL_0: 9;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            a <= z2 by A2, A35, XXREAL_1: 3;

            then

            consider o,r be Real such that

             A38: o = a & r = z2 and

             A39: o <= r;

            (x * o) <= (x * r) by A1, A39, XREAL_1: 64;

            hence thesis by A25, A27, A26, A36, A38, A37, XXREAL_1: 3;

          end;

          then (x ** A) = [.d, c.[ by A28;

          hence thesis by A26, MEASURE5:def 4;

        end;

          case a = +infty & b = +infty ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:10

    

     Th10: for A be non empty Interval, x be Real st x < 0 holds A is right_open_interval implies (x ** A) is left_open_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: x < 0 ;

      assume A is right_open_interval;

      then

      consider a be Real, b be R_eal such that

       A2: A = [.a, b.[ by MEASURE5:def 4;

      

       A3: a < b by A2, XXREAL_1: 27;

      reconsider a as R_eal by XXREAL_0:def 1;

      now

        per cases by A3, Th5;

          case a = -infty & b = -infty ;

          hence thesis;

        end;

          case a = -infty & b in REAL ;

          hence thesis;

        end;

          case a = -infty & b = +infty ;

          hence thesis;

        end;

          case

           A4: a in REAL & b in REAL ;

          then

          consider r be Real such that

           A5: r = b;

          (x * r) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A6: g = (x * r);

          consider s be Real such that

           A7: s = a;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A8: d = (x * s);

          

           A9: ].g, d.] c= (x ** A)

          proof

            let q be object;

            assume

             A10: q in ].g, d.];

            then

            reconsider q as Real by A8;

            set q2 = (q / x);

            q is R_eal by XXREAL_0:def 1;

            then

            consider q1 be R_eal such that

             A11: q1 = q;

            

             A12: g < q1 by A10, A11, XXREAL_1: 2;

            

             A13: q2 in A

            proof

              consider q3 be R_eal such that

               A14: q3 = q2;

              

               A15: q3 < b

              proof

                consider p,o be Real such that

                 A16: p = g & o = q1 and p <= o by A6, A11, A12;

                g < q1 by A10, A11, XXREAL_1: 2;

                then (o / x) < (p / x) by A1, A16, XREAL_1: 75;

                hence thesis by A1, A5, A6, A11, A14, A16, XCMPLX_1: 89;

              end;

              a <= q3

              proof

                q1 <= d & (x * q2) = q by A1, A10, A11, XCMPLX_1: 87, XXREAL_1: 2;

                hence thesis by A1, A7, A8, A11, A14, XREAL_1: 69;

              end;

              hence thesis by A2, A14, A15, XXREAL_1: 3;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A13, MEMBER_1: 193;

          end;

          (x ** A) c= ].g, d.]

          proof

            let q be object;

            assume

             A17: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A18: z2 in A and

             A19: q = (x * z2) by A17, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            z2 <= b by A2, A18, XXREAL_1: 3;

            then

            consider 2o,2r be Real such that

             A20: 2o = z2 & 2r = b and 2o <= 2r by A4;

            (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

            then

            consider 2o1,2r1 be R_eal such that

             A21: 2o1 = (x * 2o) & 2r1 = (x * 2r);

            2o < 2r by A2, A18, A20, XXREAL_1: 3;

            then

             A22: 2r1 < 2o1 by A1, A21, XREAL_1: 69;

            a <= z2 by A2, A18, XXREAL_1: 3;

            then

            consider 1o,1ra be Real such that

             A23: 1o = a & 1ra = z2 and

             A24: 1o <= 1ra;

            (x * 1ra) <= (x * 1o) by A1, A24, XREAL_1: 65;

            hence thesis by A7, A5, A8, A6, A19, A23, A20, A21, A22, XXREAL_1: 2;

          end;

          then (x ** A) = ].g, d.] by A9;

          hence thesis by A8, MEASURE5:def 5;

        end;

          case

           A25: a in REAL & b = +infty ;

          consider s be Real such that

           A26: s = a;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A27: d = (x * s);

          consider c be R_eal such that

           A28: c = -infty ;

          

           A29: ].c, d.] c= (x ** A)

          proof

            let q be object;

            assume

             A30: q in ].c, d.];

            then

            reconsider q as Real by A27;

            reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

            reconsider q1 = q as R_eal by XXREAL_0:def 1;

            

             A31: q2 in A

            proof

              reconsider q3 = q2 as R_eal;

              

               A32: a <= q3

              proof

                q1 <= d & (x * q2) = q by A1, A30, XCMPLX_1: 87, XXREAL_1: 2;

                hence thesis by A1, A26, A27, XREAL_1: 69;

              end;

              q3 < b by A25, XXREAL_0: 9;

              hence thesis by A2, A32, XXREAL_1: 3;

            end;

            q = (x * q2) by A1, XCMPLX_1: 87;

            hence thesis by A31, MEMBER_1: 193;

          end;

          (x ** A) c= ].c, d.]

          proof

            let q be object;

            assume

             A33: q in (x ** A);

            then

            reconsider q as Element of REAL ;

            consider z2 be Real such that

             A34: z2 in A and

             A35: q = (x * z2) by A33, INTEGRA2: 39;

            reconsider q as R_eal by XXREAL_0:def 1;

            

             A36: -infty < q by XXREAL_0: 12;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            a <= z2 by A2, A34, XXREAL_1: 3;

            then

            consider o,r be Real such that

             A37: o = a & r = z2 and

             A38: o <= r;

            (x * r) <= (x * o) by A1, A38, XREAL_1: 65;

            hence thesis by A26, A28, A27, A35, A37, A36, XXREAL_1: 2;

          end;

          then (x ** A) = ].c, d.] by A29;

          hence thesis by A27, MEASURE5:def 5;

        end;

          case a = +infty & b = +infty ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:11

    

     Th11: for A be non empty Interval, x be Real st 0 < x holds A is left_open_interval implies (x ** A) is left_open_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      assume A is left_open_interval;

      then

      consider a be R_eal, b be Real such that

       A2: A = ].a, b.] by MEASURE5:def 5;

      

       A3: a < b by A2, XXREAL_1: 26;

      reconsider b as R_eal by XXREAL_0:def 1;

      now

        per cases by A3, Th5;

          case a = -infty & b = -infty ;

          hence thesis;

        end;

          case

           A4: a = -infty & b in REAL ;

          consider s be Real such that

           A5: s = b;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A6: d = (x * s);

          consider c be R_eal such that

           A7: c = -infty ;

          

           A8: ].c, d.] c= (x ** A)

          proof

            let q be object;

            assume

             A9: q in ].c, d.];

            then

            reconsider q as Real by A6;

            reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

            reconsider q1 = q as R_eal by XXREAL_0:def 1;

            

             A10: q2 in A

            proof

              consider q3 be R_eal such that

               A11: q3 = q2;

              

               A12: q3 <= b

              proof

                q1 <= d & (x * q2) = q by A1, A9, XCMPLX_1: 87, XXREAL_1: 2;

                hence thesis by A1, A5, A6, A11, XREAL_1: 68;

              end;

              a < q3 by A4, A11, XXREAL_0: 12;

              hence thesis by A2, A11, A12, XXREAL_1: 2;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A10, MEMBER_1: 193;

          end;

          (x ** A) c= ].c, d.]

          proof

            let q be object;

            assume

             A13: q in (x ** A);

            then

            reconsider q as Element of REAL ;

            consider z2 be Real such that

             A14: z2 in A and

             A15: q = (x * z2) by A13, INTEGRA2: 39;

            reconsider q as R_eal by XXREAL_0:def 1;

            

             A16: -infty < q by XXREAL_0: 12;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            z2 <= b by A2, A14, XXREAL_1: 2;

            then

            consider r,o be Real such that

             A17: r = z2 & o = b and

             A18: r <= o;

            (x * r) <= (x * o) by A1, A18, XREAL_1: 64;

            hence thesis by A5, A7, A6, A15, A17, A16, XXREAL_1: 2;

          end;

          then (x ** A) = ].c, d.] by A8;

          hence thesis by A6, MEASURE5:def 5;

        end;

          case a = -infty & b = +infty ;

          hence thesis;

        end;

          case

           A19: a in REAL & b in REAL ;

          then

          reconsider s = a as Real;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A20: d = (x * s);

          consider r be Real such that

           A21: r = b;

          (x * r) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A22: g = (x * r);

          

           A23: ].d, g.] c= (x ** A)

          proof

            let q be object;

            assume

             A24: q in ].d, g.];

            then

            reconsider q as Real by A22;

            set q2 = (q / x);

            reconsider q1 = q as R_eal by XXREAL_0:def 1;

            

             A25: q2 in A

            proof

              consider q3 be R_eal such that

               A26: q3 = q2;

              

               A27: q3 <= b

              proof

                q1 <= g by A24, XXREAL_1: 2;

                then

                consider p,o be Real such that

                 A28: p = q1 & o = g and

                 A29: p <= o by A22;

                (p / x) <= (o / x) by A1, A29, XREAL_1: 72;

                hence thesis by A1, A21, A22, A26, A28, XCMPLX_1: 89;

              end;

              d < q1 & (x * q2) = q by A1, A24, XCMPLX_1: 87, XXREAL_1: 2;

              then a < q3 by A1, A20, A26, XREAL_1: 64;

              hence thesis by A2, A26, A27, XXREAL_1: 2;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A25, MEMBER_1: 193;

          end;

          (x ** A) c= ].d, g.]

          proof

            let q be object;

            assume

             A30: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A31: z2 in A and

             A32: q = (x * z2) by A30, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            a <= z2 by A2, A31, XXREAL_1: 2;

            then

            consider 1o,1ra be Real such that

             A33: 1o = a & 1ra = z2 and 1o <= 1ra by A19;

            1o < 1ra by A2, A31, A33, XXREAL_1: 2;

            then

             A34: (x * 1o) < (x * 1ra) by A1, XREAL_1: 68;

            z2 <= b by A2, A31, XXREAL_1: 2;

            then

            consider 2o,2r be Real such that

             A35: 2o = z2 & 2r = b and

             A36: 2o <= 2r;

            (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

            then

            consider 2o1,2r1 be R_eal such that

             A37: 2o1 = (x * 2o) & 2r1 = (x * 2r);

            2o1 <= 2r1 by A1, A36, A37, XREAL_1: 64;

            hence thesis by A21, A20, A22, A32, A33, A35, A34, A37, XXREAL_1: 2;

          end;

          then (x ** A) = ].d, g.] by A23;

          hence thesis by A22, MEASURE5:def 5;

        end;

          case a in REAL & b = +infty ;

          hence thesis;

        end;

          case a = +infty & b = +infty ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:12

    

     Th12: for A be non empty Interval, x be Real st x < 0 holds A is left_open_interval implies (x ** A) is right_open_interval

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: x < 0 ;

      assume A is left_open_interval;

      then

      consider a be R_eal, b be Real such that

       A2: A = ].a, b.] by MEASURE5:def 5;

      

       A3: a < b by A2, XXREAL_1: 26;

      reconsider b as R_eal by XXREAL_0:def 1;

      now

        per cases by A3, Th5;

          case a = -infty & b = -infty ;

          hence thesis;

        end;

          case

           A4: a = -infty & b in REAL ;

          consider s be Real such that

           A5: s = b;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A6: d = (x * s);

          consider c be R_eal such that

           A7: c = +infty ;

          

           A8: [.d, c.[ c= (x ** A)

          proof

            let q be object;

            assume

             A9: q in [.d, c.[;

            then

            reconsider q as Element of REAL by A6, XREAL_0:def 1;

            consider q2 be Real such that

             A10: q2 = (q / x);

            reconsider q2 as Element of REAL by XREAL_0:def 1;

            q is R_eal by XXREAL_0:def 1;

            then

            consider q1 be R_eal such that

             A11: q1 = q;

            

             A12: q2 in A

            proof

              q2 is R_eal by XXREAL_0:def 1;

              then

              consider q3 be R_eal such that

               A13: q3 = q2;

              

               A14: q3 <= b

              proof

                d <= q1 & (x * q2) = q by A1, A9, A11, A10, XCMPLX_1: 87, XXREAL_1: 3;

                hence thesis by A1, A5, A6, A11, A13, XREAL_1: 69;

              end;

              a < q3 by A4, A13, XXREAL_0: 12;

              hence thesis by A2, A13, A14, XXREAL_1: 2;

            end;

            q = (x * q2) by A1, A10, XCMPLX_1: 87;

            hence thesis by A12, MEMBER_1: 193;

          end;

          (x ** A) c= [.d, c.[

          proof

            let q be object;

            assume

             A15: q in (x ** A);

            then

            reconsider q as Element of REAL ;

            consider z2 be Real such that

             A16: z2 in A and

             A17: q = (x * z2) by A15, INTEGRA2: 39;

            reconsider q as R_eal by XXREAL_0:def 1;

            

             A18: q < +infty by XXREAL_0: 9;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            z2 <= b by A2, A16, XXREAL_1: 2;

            then

            consider r,o be Real such that

             A19: r = z2 & o = b and

             A20: r <= o;

            (x * o) <= (x * r) by A1, A20, XREAL_1: 65;

            hence thesis by A5, A7, A6, A17, A19, A18, XXREAL_1: 3;

          end;

          then (x ** A) = [.d, c.[ by A8;

          hence thesis by A6, MEASURE5:def 4;

        end;

          case a = -infty & b = +infty ;

          hence thesis;

        end;

          case

           A21: a in REAL & b in REAL ;

          then

          reconsider s = a, r = b as Real;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A22: d = (x * s);

          (x * r) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A23: g = (x * r);

          

           A24: [.g, d.[ c= (x ** A)

          proof

            let q be object;

            assume

             A25: q in [.g, d.[;

            then

            reconsider q as Real by A23;

            consider q2 be Real such that

             A26: q2 = (q / x);

            q is R_eal by XXREAL_0:def 1;

            then

            consider q1 be R_eal such that

             A27: q1 = q;

            

             A28: q1 < d by A25, A27, XXREAL_1: 3;

            

             A29: q2 in A

            proof

              q2 is R_eal by XXREAL_0:def 1;

              then

              consider q3 be R_eal such that

               A30: q3 = q2;

              

               A31: q3 <= b

              proof

                g <= q1 by A25, A27, XXREAL_1: 3;

                then

                consider p,o be Real such that

                 A32: p = g & o = q1 and

                 A33: p <= o by A23, A27;

                (o / x) <= (p / x) by A1, A33, XREAL_1: 73;

                hence thesis by A1, A23, A27, A26, A30, A32, XCMPLX_1: 89;

              end;

              (x * q2) = q by A1, A26, XCMPLX_1: 87;

              then a < q3 by A1, A22, A27, A28, A30, XREAL_1: 65;

              hence thesis by A2, A30, A31, XXREAL_1: 2;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A26, A29, MEMBER_1: 193;

          end;

          (x ** A) c= [.g, d.[

          proof

            let q be object;

            assume

             A34: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A35: z2 in A and

             A36: q = (x * z2) by A34, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            a <= z2 by A2, A35, XXREAL_1: 2;

            then

            consider 1o,1ra be Real such that

             A37: 1o = a & 1ra = z2 and 1o <= 1ra by A21;

            1o < 1ra by A2, A35, A37, XXREAL_1: 2;

            then

             A38: (x * 1ra) < (x * 1o) by A1, XREAL_1: 69;

            z2 <= b by A2, A35, XXREAL_1: 2;

            then

            consider 2o,2r be Real such that

             A39: 2o = z2 & 2r = b and

             A40: 2o <= 2r;

            (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

            then

            consider 2o1,2r1 be R_eal such that

             A41: 2o1 = (x * 2o) & 2r1 = (x * 2r);

            2r1 <= 2o1 by A1, A40, A41, XREAL_1: 65;

            hence thesis by A22, A23, A36, A37, A39, A38, A41, XXREAL_1: 3;

          end;

          then (x ** A) = [.g, d.[ by A24;

          hence thesis by A23, MEASURE5:def 4;

        end;

          case a in REAL & b = +infty ;

          hence thesis;

        end;

          case a = +infty & b = +infty ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:13

    for A be non empty Interval, x be Real st 0 < x holds for B be non empty Interval st B = (x ** A) holds A = [.( inf A), ( sup A).] implies (B = [.( inf B), ( sup B).] & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      let B be non empty Interval;

      assume

       A2: B = (x ** A);

      A = [.( inf A), ( sup A).] implies (B = [.( inf B), ( sup B).] & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

      proof

        assume

         A3: A = [.( inf A), ( sup A).];

        

         A4: for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t)

        proof

          let s,t be Real;

          assume that

           A5: s = ( inf A) and

           A6: t = ( sup A);

          ( inf B) = (x * s) & ( sup B) = (x * t)

          proof

            s <= t by A5, A6, XXREAL_2: 40;

            then

             A7: (x * s) <= (x * t) by A1, XREAL_1: 64;

            (x * s) is R_eal by XXREAL_0:def 1;

            then

            consider d be R_eal such that

             A8: d = (x * s);

            (x * t) is R_eal by XXREAL_0:def 1;

            then

            consider g be R_eal such that

             A9: g = (x * t);

            

             A10: [.d, g.] c= (x ** A)

            proof

              let q be object;

              assume

               A11: q in [.d, g.];

              then

              reconsider q as Real by A8, A9;

              set q2 = (q / x);

              reconsider q1 = q as R_eal by XXREAL_0:def 1;

              

               A12: q2 in A

              proof

                consider q3 be R_eal such that

                 A13: q3 = q2;

                

                 A14: q3 <= ( sup A)

                proof

                  q1 <= g by A11, XXREAL_1: 1;

                  then

                  consider p,o be Real such that

                   A15: p = q1 & o = g and

                   A16: p <= o by A9;

                  (p / x) <= (o / x) by A1, A16, XREAL_1: 72;

                  hence thesis by A1, A6, A9, A13, A15, XCMPLX_1: 89;

                end;

                ( inf A) <= q3

                proof

                  d <= q1 & (x * q2) = q by A1, A11, XCMPLX_1: 87, XXREAL_1: 1;

                  hence thesis by A1, A5, A8, A13, XREAL_1: 68;

                end;

                hence thesis by A3, A13, A14, XXREAL_1: 1;

              end;

              q = (x * q2) by A1, XCMPLX_1: 87;

              hence thesis by A12, MEMBER_1: 193;

            end;

            (x ** A) c= [.d, g.]

            proof

              let q be object;

              assume

               A17: q in (x ** A);

              then

              reconsider q as Real;

              consider z2 be Real such that

               A18: z2 in A and

               A19: q = (x * z2) by A17, INTEGRA2: 39;

              reconsider z2 as R_eal by XXREAL_0:def 1;

              ( inf A) <= z2 by A3, A18, XXREAL_1: 1;

              then

              consider 1o,1ra be Real such that

               A20: 1o = ( inf A) & 1ra = z2 and

               A21: 1o <= 1ra by A5;

              

               A22: (x * 1o) <= (x * 1ra) by A1, A21, XREAL_1: 64;

              z2 <= ( sup A) by A3, A18, XXREAL_1: 1;

              then

              consider 2o,2r be Real such that

               A23: 2o = z2 & 2r = ( sup A) and

               A24: 2o <= 2r by A6;

              (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

              then

              consider 2o1,2r1 be R_eal such that

               A25: 2o1 = (x * 2o) & 2r1 = (x * 2r);

              2o1 <= 2r1 by A1, A24, A25, XREAL_1: 64;

              hence thesis by A5, A6, A8, A9, A19, A20, A23, A22, A25, XXREAL_1: 1;

            end;

            then (x ** A) = [.d, g.] by A10;

            hence thesis by A2, A8, A9, A7, MEASURE6: 10, MEASURE6: 14;

          end;

          hence thesis;

        end;

        ( inf A) <= ( sup A) by XXREAL_2: 40;

        then ( inf A) in A & ( sup A) in A by A3, XXREAL_1: 1;

        then A is closed_interval by A3, MEASURE5:def 3;

        then (x ** A) is closed_interval by A1, Th8;

        hence thesis by A2, A4, MEASURE6: 17;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:14

    for A be non empty Interval, x be Real st 0 < x holds for B be non empty Interval st B = (x ** A) holds A = ].( inf A), ( sup A).] implies (B = ].( inf B), ( sup B).] & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      let B be non empty Interval;

      assume

       A2: B = (x ** A);

      

       A3: ( inf A) <= ( sup A) by XXREAL_2: 40;

      assume

       A4: A = ].( inf A), ( sup A).];

      then ( inf A) <> ( sup A);

      then ( inf A) < ( sup A) by A3, XXREAL_0: 1;

      then ( sup A) in A by A4, XXREAL_1: 2;

      then

      reconsider b = ( sup A) as Real;

      

       A5: for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t)

      proof

        let s,t be Real;

        assume that

         A6: s = ( inf A) and

         A7: t = ( sup A);

        ( inf B) = (x * s) & ( sup B) = (x * t)

        proof

          s <= t by A6, A7, XXREAL_2: 40;

          then

           A8: (x * s) <= (x * t) by A1, XREAL_1: 64;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A9: d = (x * s);

          (x * t) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A10: g = (x * t);

          

           A11: ].d, g.] c= (x ** A)

          proof

            let q be object;

            assume

             A12: q in ].d, g.];

            then

            reconsider q as Real by A10;

            set q2 = (q / x);

            reconsider q1 = q as R_eal by XXREAL_0:def 1;

            

             A13: q2 in A

            proof

              reconsider q3 = q2 as R_eal;

              

               A14: q3 <= ( sup A)

              proof

                q1 <= g by A12, XXREAL_1: 2;

                then

                consider p,o be Real such that

                 A15: p = q1 & o = g and

                 A16: p <= o by A10;

                (p / x) <= (o / x) by A1, A16, XREAL_1: 72;

                hence thesis by A1, A7, A10, A15, XCMPLX_1: 89;

              end;

              d < q1 & (x * q2) = q by A1, A12, XCMPLX_1: 87, XXREAL_1: 2;

              then ( inf A) < q3 by A1, A6, A9, XREAL_1: 64;

              hence thesis by A4, A14, XXREAL_1: 2;

            end;

            q = (x * q2) by A1, XCMPLX_1: 87;

            hence thesis by A13, MEMBER_1: 193;

          end;

          (x ** A) c= ].d, g.]

          proof

            let q be object;

            assume

             A17: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A18: z2 in A and

             A19: q = (x * z2) by A17, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            reconsider q as R_eal by XXREAL_0:def 1;

            ( inf A) <= z2 by A4, A18, XXREAL_1: 2;

            then

            consider 1o,1ra be Real such that

             A20: 1o = ( inf A) & 1ra = z2 and 1o <= 1ra by A6;

            1o < 1ra by A4, A18, A20, XXREAL_1: 2;

            then

             A21: d < q by A1, A6, A9, A19, A20, XREAL_1: 68;

            z2 <= ( sup A) by A4, A18, XXREAL_1: 2;

            then

            consider 2o,2r be Real such that

             A22: 2o = z2 & 2r = ( sup A) and

             A23: 2o <= 2r by A7;

            (x * 2o) <= (x * 2r) by A1, A23, XREAL_1: 64;

            hence thesis by A7, A10, A19, A22, A21, XXREAL_1: 2;

          end;

          then (x ** A) = ].d, g.] by A11;

          hence thesis by A2, A9, A10, A8, MEASURE6: 9, MEASURE6: 13;

        end;

        hence thesis;

      end;

      A = ].( inf A), b.] by A4;

      then A is left_open_interval by MEASURE5:def 5;

      then B is left_open_interval by A1, A2, Th11;

      hence thesis by A5, MEASURE6: 19;

    end;

    theorem :: URYSOHN2:15

    for A be non empty Interval, x be Real st 0 < x holds for B be non empty Interval st B = (x ** A) holds A = ].( inf A), ( sup A).[ implies (B = ].( inf B), ( sup B).[ & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      let B be non empty Interval;

      assume

       A2: B = (x ** A);

      A = ].( inf A), ( sup A).[ implies (B = ].( inf B), ( sup B).[ & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

      proof

        assume

         A3: A = ].( inf A), ( sup A).[;

        

         A4: for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t) & B is open_interval

        proof

          let s,t be Real;

          assume that

           A5: s = ( inf A) and

           A6: t = ( sup A);

          ( inf B) = (x * s) & ( sup B) = (x * t) & B is open_interval

          proof

            s <= t by A5, A6, XXREAL_2: 40;

            then

             A7: (x * s) <= (x * t) by A1, XREAL_1: 64;

            (x * s) is R_eal by XXREAL_0:def 1;

            then

            consider d be R_eal such that

             A8: d = (x * s);

            (x * t) is R_eal by XXREAL_0:def 1;

            then

            consider g be R_eal such that

             A9: g = (x * t);

            

             A10: ].d, g.[ c= (x ** A)

            proof

              let q be object;

              assume

               A11: q in ].d, g.[;

              then

              reconsider q as Real;

              set q2 = (q / x);

              q is R_eal by XXREAL_0:def 1;

              then

              consider q1 be R_eal such that

               A12: q1 = q;

              

               A13: q1 < g by A11, A12, MEASURE5:def 1;

              

               A14: q2 in A

              proof

                consider q3 be R_eal such that

                 A15: q3 = q2;

                

                 A16: q3 < ( sup A)

                proof

                  consider p,o be Real such that

                   A17: p = q1 & o = g and p <= o by A9, A12, A13;

                  (p / x) < (o / x) by A1, A13, A17, XREAL_1: 74;

                  hence thesis by A1, A6, A9, A12, A15, A17, XCMPLX_1: 89;

                end;

                d < q1 & (x * q2) = q by A1, A11, A12, MEASURE5:def 1, XCMPLX_1: 87;

                then ( inf A) < q3 by A1, A5, A8, A12, A15, XREAL_1: 64;

                hence thesis by A3, A15, A16, MEASURE5:def 1;

              end;

              q = (x * (q / x)) by A1, XCMPLX_1: 87;

              hence thesis by A14, MEMBER_1: 193;

            end;

            (x ** A) c= ].d, g.[

            proof

              let q be object;

              assume

               A18: q in (x ** A);

              then

              reconsider q as Real;

              consider z2 be Real such that

               A19: z2 in A and

               A20: q = (x * z2) by A18, INTEGRA2: 39;

              reconsider z2 as R_eal by XXREAL_0:def 1;

              ( inf A) <= z2 by A3, A19, MEASURE5:def 1;

              then

              consider 1o,1ra be Real such that

               A21: 1o = ( inf A) & 1ra = z2 and 1o <= 1ra by A5;

              1o < 1ra by A3, A19, A21, MEASURE5:def 1;

              then

               A22: (x * 1o) < (x * 1ra) by A1, XREAL_1: 68;

              z2 <= ( sup A) by A3, A19, MEASURE5:def 1;

              then

              consider 2o,2r be Real such that

               A23: 2o = z2 & 2r = ( sup A) and 2o <= 2r by A6;

              (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

              then

              consider 2o1,2r1 be R_eal such that

               A24: 2o1 = (x * 2o) & 2r1 = (x * 2r);

              2o < 2r by A3, A19, A23, MEASURE5:def 1;

              then 2o1 < 2r1 by A1, A24, XREAL_1: 68;

              hence thesis by A5, A6, A8, A9, A20, A21, A23, A22, A24, MEASURE5:def 1;

            end;

            then (x ** A) = ].d, g.[ by A10;

            hence thesis by A2, A8, A9, A7, MEASURE5:def 2, MEASURE6: 8, MEASURE6: 12;

          end;

          hence thesis;

        end;

        A is open_interval by A3, MEASURE5:def 2;

        then (x ** A) is open_interval by A1, Th7;

        hence thesis by A2, A4, MEASURE6: 16;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN2:16

    for A be non empty Interval, x be Real st 0 < x holds for B be non empty Interval st B = (x ** A) holds A = [.( inf A), ( sup A).[ implies (B = [.( inf B), ( sup B).[ & for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t))

    proof

      let A be non empty Interval;

      let x be Real;

      assume

       A1: 0 < x;

      let B be non empty Interval;

      assume

       A2: B = (x ** A);

      

       A3: ( inf A) <= ( sup A) by XXREAL_2: 40;

      assume

       A4: A = [.( inf A), ( sup A).[;

      then ( inf A) <> ( sup A);

      then ( inf A) < ( sup A) by A3, XXREAL_0: 1;

      then ( inf A) in A by A4, XXREAL_1: 3;

      then

      reconsider a = ( inf A) as Real;

      

       A5: for s,t be Real st s = ( inf A) & t = ( sup A) holds ( inf B) = (x * s) & ( sup B) = (x * t) & B is right_open_interval

      proof

        let s,t be Real;

        assume that

         A6: s = ( inf A) and

         A7: t = ( sup A);

        ( inf B) = (x * s) & ( sup B) = (x * t) & B is right_open_interval

        proof

          s <= t by A6, A7, XXREAL_2: 40;

          then

           A8: (x * s) <= (x * t) by A1, XREAL_1: 64;

          (x * s) is R_eal by XXREAL_0:def 1;

          then

          consider d be R_eal such that

           A9: d = (x * s);

          (x * t) is R_eal by XXREAL_0:def 1;

          then

          consider g be R_eal such that

           A10: g = (x * t);

          

           A11: [.d, g.[ c= (x ** A)

          proof

            let q be object;

            assume

             A12: q in [.d, g.[;

            then

            reconsider q as Real by A9;

            reconsider q2 = (q / x) as Element of REAL by XREAL_0:def 1;

            reconsider q1 = q as R_eal by XXREAL_0:def 1;

            

             A13: q1 < g by A12, XXREAL_1: 3;

            

             A14: q2 in A

            proof

              reconsider q3 = q2 as R_eal;

              ( inf A) <= q3 & q3 < ( sup A) & q3 in REAL

              proof

                

                 A15: q3 < ( sup A)

                proof

                  consider p,o be Real such that

                   A16: p = q1 & o = g and p <= o by A10, A13;

                  q1 < g by A12, XXREAL_1: 3;

                  then (p / x) < (o / x) by A1, A16, XREAL_1: 74;

                  hence thesis by A1, A7, A10, A16, XCMPLX_1: 89;

                end;

                d <= q1 & (x * q2) = q by A1, A12, XCMPLX_1: 87, XXREAL_1: 3;

                hence thesis by A1, A6, A9, A15, XREAL_1: 68;

              end;

              hence thesis by A4, XXREAL_1: 3;

            end;

            q = (x * (q / x)) by A1, XCMPLX_1: 87;

            hence thesis by A14, MEMBER_1: 193;

          end;

          (x ** A) c= [.d, g.[

          proof

            let q be object;

            assume

             A17: q in (x ** A);

            then

            reconsider q as Real;

            consider z2 be Real such that

             A18: z2 in A and

             A19: q = (x * z2) by A17, INTEGRA2: 39;

            reconsider z2 as R_eal by XXREAL_0:def 1;

            z2 <= ( sup A) by A4, A18, XXREAL_1: 3;

            then

            consider 2o,2r be Real such that

             A20: 2o = z2 & 2r = ( sup A) and 2o <= 2r by A7;

            (x * 2o) is R_eal & (x * 2r) is R_eal by XXREAL_0:def 1;

            then

            consider 2o1,2r1 be R_eal such that

             A21: 2o1 = (x * 2o) & 2r1 = (x * 2r);

            2o < 2r by A4, A18, A20, XXREAL_1: 3;

            then

             A22: 2o1 < 2r1 by A1, A21, XREAL_1: 68;

            ( inf A) <= z2 by A4, A18, XXREAL_1: 3;

            then

            consider 1o,1ra be Real such that

             A23: 1o = ( inf A) & 1ra = z2 and

             A24: 1o <= 1ra by A6;

            (x * 1o) <= (x * 1ra) by A1, A24, XREAL_1: 64;

            hence thesis by A6, A7, A9, A10, A19, A23, A20, A21, A22, XXREAL_1: 3;

          end;

          then (x ** A) = [.d, g.[ by A11;

          hence thesis by A2, A9, A10, A8, MEASURE5:def 4, MEASURE6: 11, MEASURE6: 15;

        end;

        hence thesis;

      end;

      A = [.a, ( sup A).[ by A4;

      then A is right_open_interval by MEASURE5:def 4;

      then (x ** A) is right_open_interval by A1, Th9;

      hence thesis by A2, A5, MEASURE6: 18;

    end;

    theorem :: URYSOHN2:17

    

     Th17: for A be non empty Interval, x be Real holds (x ** A) is Interval

    proof

      let A be non empty Interval;

      let x be Real;

      per cases ;

        suppose x = 0 ;

        hence thesis by Th6;

      end;

        suppose

         A1: x <> 0 ;

        now

          per cases by MEASURE5: 1;

            case A is open_interval;

            then (x ** A) is open_interval by A1, Th7;

            hence thesis;

          end;

            case A is closed_interval;

            then (x ** A) is closed_interval by A1, Th8;

            hence thesis;

          end;

            case

             A2: A is right_open_interval;

            per cases by A1;

              case x < 0 ;

              then (x ** A) is left_open_interval by A2, Th10;

              hence thesis;

            end;

              case 0 < x;

              then (x ** A) is right_open_interval by A2, Th9;

              hence thesis;

            end;

          end;

            case

             A3: A is left_open_interval;

            now

              per cases by A1;

                case x < 0 ;

                then (x ** A) is right_open_interval by A3, Th12;

                hence thesis;

              end;

                case 0 < x;

                then (x ** A) is left_open_interval by A3, Th11;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    registration

      let A be interval Subset of REAL ;

      let x be Real;

      cluster (x ** A) -> interval;

      correctness

      proof

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose A is non empty;

          hence thesis by Th17;

        end;

      end;

    end

    

     Lm1: for A be non empty Subset of REAL , x be Real st x > 0 & (x ** A) is bounded_above holds A is bounded_above

    proof

      let A be non empty Subset of REAL , x be Real such that

       A1: x > 0 and

       A2: (x ** A) is bounded_above;

      

       A3: ( sup (x ** A)) <> +infty by A2;

      consider r be Real such that

       A4: r in A by MEMBERED: 9;

      per cases by A3, XXREAL_0: 14;

        suppose

         A5: ( sup (x ** A)) = -infty ;

        take 0 ;

        

         A6: (x * r) in (x ** A) by A4, MEMBER_1: 193;

         -infty is UpperBound of (x ** A) by A5, XXREAL_2:def 3;

        hence thesis by A6, XXREAL_0: 6, XXREAL_2:def 1;

      end;

        suppose ( sup (x ** A)) in REAL ;

        then

        reconsider r = ( sup (x ** A)) as Real;

        take (r / x);

        let z be ExtReal;

        assume

         A7: z in A;

        ((x " ) ** (x ** A)) = A by A1, Th1;

        then

        consider s be Real such that

         A8: s in (x ** A) and

         A9: z = ((x " ) * s) by A7, INTEGRA2: 39;

        s <= r by A8, XXREAL_2: 4;

        then (s / x) <= (r / x) by A1, XREAL_1: 72;

        hence thesis by A9;

      end;

    end;

    theorem :: URYSOHN2:18

    

     Th18: for A be non empty Subset of REAL , x be Real, y be R_eal st x = y & 0 <= y holds ( sup (x ** A)) = (y * ( sup A))

    proof

      let A be non empty Subset of REAL , x be Real, y be R_eal such that

       A1: x = y and

       A2: 0 <= y;

      reconsider Y = (x ** A) as non empty Subset of REAL ;

      per cases ;

        suppose

         A3: not A is bounded_above;

        per cases by A2;

          suppose

           A4: y = 0 ;

          then (x ** A) = { 0 } by A1, INTEGRA2: 40;

          

          hence ( sup (x ** A)) = 0 by XXREAL_2: 11

          .= (y * ( sup A)) by A4;

        end;

          suppose

           A5: y > 0 ;

          then not Y is bounded_above by A1, A3, Lm1;

          

          hence ( sup (x ** A)) = +infty by XXREAL_2: 73

          .= (y * +infty ) by A5, XXREAL_3:def 5

          .= (y * ( sup A)) by A3, XXREAL_2: 73;

        end;

      end;

        suppose A is bounded_above;

        then

        reconsider X = A as non empty bounded_above real-membered set;

        reconsider u = ( upper_bound X) as Real;

        (x ** X) is bounded_above by A1, A2, INTEGRA2: 9;

        then

        reconsider Y as non empty bounded_above real-membered set;

        

        thus ( sup (x ** A)) = ( upper_bound Y)

        .= (x * u) by A1, A2, INTEGRA2: 13

        .= (y * ( sup A)) by A1, EXTREAL1: 1;

      end;

    end;

    

     Lm2: for A be non empty Subset of REAL , x be Real st x > 0 & (x ** A) is bounded_below holds A is bounded_below

    proof

      let A be non empty Subset of REAL , x be Real such that

       A1: x > 0 and

       A2: (x ** A) is bounded_below;

      

       A3: ( inf (x ** A)) <> -infty by A2;

      consider r be Real such that

       A4: r in A by MEMBERED: 9;

      per cases by A3, XXREAL_0: 14;

        suppose

         A5: ( inf (x ** A)) = +infty ;

        take 0 ;

        

         A6: (x * r) in (x ** A) by A4, MEMBER_1: 193;

         +infty is LowerBound of (x ** A) by A5, XXREAL_2:def 4;

        hence thesis by A6, XXREAL_0: 4, XXREAL_2:def 2;

      end;

        suppose ( inf (x ** A)) in REAL ;

        then

        reconsider r = ( inf (x ** A)) as Real;

        take (r / x);

        let z be ExtReal;

        assume

         A7: z in A;

        ((x " ) ** (x ** A)) = A by A1, Th1;

        then

        consider s be Real such that

         A8: s in (x ** A) and

         A9: z = ((x " ) * s) by A7, INTEGRA2: 39;

        (r / x) <= (s / x) by A1, A8, XREAL_1: 72, XXREAL_2: 3;

        hence thesis by A9;

      end;

    end;

    theorem :: URYSOHN2:19

    

     Th19: for A be non empty Subset of REAL , x be Real, y be R_eal st x = y & 0 <= y holds ( inf (x ** A)) = (y * ( inf A))

    proof

      let A be non empty Subset of REAL , x be Real, y be R_eal such that

       A1: x = y and

       A2: 0 <= y;

      reconsider Y = (x ** A) as non empty Subset of REAL ;

      per cases ;

        suppose

         A3: not A is bounded_below;

        per cases by A2;

          suppose

           A4: y = 0 ;

          then (x ** A) = { 0 } by A1, INTEGRA2: 40;

          

          hence ( inf (x ** A)) = 0 by XXREAL_2: 13

          .= (y * ( inf A)) by A4;

        end;

          suppose

           A5: y > 0 ;

          then not Y is bounded_below by A1, A3, Lm2;

          

          hence ( inf (x ** A)) = -infty by XXREAL_2: 74

          .= (y * -infty ) by A5, XXREAL_3:def 5

          .= (y * ( inf A)) by A3, XXREAL_2: 74;

        end;

      end;

        suppose A is bounded_below;

        then

        reconsider X = A as non empty bounded_below real-membered set;

        reconsider u = ( lower_bound X) as Real;

        (x ** X) is bounded_below by A1, A2, INTEGRA2: 11;

        then

        reconsider Y as non empty bounded_below real-membered set;

        

        thus ( inf (x ** A)) = ( lower_bound Y)

        .= (x * u) by A1, A2, INTEGRA2: 15

        .= (y * ( inf A)) by A1, EXTREAL1: 1;

      end;

    end;

    theorem :: URYSOHN2:20

    for A be Interval, x,y be Real st 0 <= x & y = ( diameter A) holds (x * y) = ( diameter (x ** A))

    proof

      let A be Interval;

      let x,y be Real such that

       A1: 0 <= x and

       A2: y = ( diameter A);

      per cases ;

        suppose

         A3: A is empty;

        then

         A4: (x ** A) is empty;

        

        thus (x * y) = 0 by A2, A3, MEASURE5: 10

        .= ( diameter (x ** A)) by A4, MEASURE5: 10;

      end;

        suppose

         A5: A is non empty;

        then

        consider z be Real such that

         A6: z in A;

        reconsider z as Real;

        

         A7: (x * z) in (x ** A) by A6, MEMBER_1: 193;

        reconsider AA = A as non empty Subset of REAL by A5;

        reconsider u = x as R_eal by XXREAL_0:def 1;

        

         A8: ( inf (x ** AA)) = (u * ( inf AA)) by A1, Th19;

        reconsider z = x as R_eal by XXREAL_0:def 1;

        

        thus (x * y) = (z * ( diameter A)) by A2, EXTREAL1: 1

        .= (z * (( sup A) - ( inf A))) by A5, MEASURE5:def 6

        .= ((z * ( sup A)) - (z * ( inf A))) by XXREAL_3: 100

        .= (( sup (x ** A)) - ( inf (x ** A))) by A1, A8, Th18

        .= ( diameter (x ** A)) by A7, MEASURE5:def 6;

      end;

    end;

    theorem :: URYSOHN2:21

    

     Th21: for eps be Real st 0 < eps holds ex n be Nat st 1 < ((2 |^ n) * eps)

    proof

      let eps be Real;

      assume

       A1: 0 < eps;

      consider n be Nat such that

       A2: (1 / eps) < n by SEQ_4: 3;

      take n;

      n < (2 |^ n) by NEWTON: 86;

      then (1 / eps) < (2 |^ n) by A2, XXREAL_0: 2;

      then ((1 / eps) * eps) < ((2 |^ n) * eps) by A1, XREAL_1: 68;

      hence thesis by A1, XCMPLX_1: 87;

    end;

    theorem :: URYSOHN2:22

    

     Th22: for a,b be Real st 0 <= a & 1 < (b - a) holds ex n be Nat st a < n & n < b

    proof

      let a,b be Real;

      assume that

       A1: 0 <= a and

       A2: 1 < (b - a);

      a < ( [\a/] + 1) by INT_1: 29;

      then

      reconsider n = ( [\a/] + 1) as Element of NAT by A1, INT_1: 3;

      take n;

      thus a < n by INT_1: 29;

       [\a/] <= a by INT_1:def 6;

      then

       A3: ( [\a/] + 1) <= (a + 1) by XREAL_1: 6;

      (1 + a) < b by A2, XREAL_1: 20;

      hence thesis by A3, XXREAL_0: 2;

    end;

    theorem :: URYSOHN2:23

    for n be Nat holds ( dyadic n) c= DYADIC by URYSOHN1:def 2;

    theorem :: URYSOHN2:24

    

     Th24: for a,b be Real st a < b & 0 <= a & b <= 1 holds ex c be Real st c in DYADIC & a < c & c < b

    proof

      let a,b be Real;

      assume that

       A1: a < b and

       A2: 0 <= a and

       A3: b <= 1;

      set eps = (b - a);

      consider n be Nat such that

       A4: 1 < ((2 |^ n) * eps) by A1, Th21, XREAL_1: 50;

      set aa = ((2 |^ n) * a), bb = ((2 |^ n) * b);

      1 < (bb - aa) by A4;

      then

      consider m be Nat such that

       A5: aa < m and

       A6: m < bb by A2, Th22;

      set x = (m / (2 |^ n));

      take x;

      

       A7: 0 < (2 |^ n) by NEWTON: 83;

      (m / (2 |^ n)) < b by A6, NEWTON: 83, XREAL_1: 83;

      then (m / (2 |^ n)) < 1 by A3, XXREAL_0: 2;

      then m < (2 |^ n) by A7, XREAL_1: 181;

      then x in ( dyadic n) by URYSOHN1:def 1;

      hence thesis by A7, A5, A6, URYSOHN1:def 2, XREAL_1: 81, XREAL_1: 83;

    end;

    theorem :: URYSOHN2:25

    

     Th25: for a,b be Real st a < b holds ex c be Real st c in DOM & a < c & c < b

    proof

      let a,b be Real;

      assume

       A1: a < b;

      per cases ;

        suppose

         A2: a < 0 & b <= 1;

        now

          per cases ;

            case

             A3: b <= 0 ;

            consider c be Real such that

             A4: a < c and

             A5: c < b by A1, XREAL_1: 5;

            reconsider c as Real;

            ( halfline 0 ) = { g where g be Real : g < 0 } by XXREAL_1: 229;

            then c in ( halfline 0 ) by A3, A5;

            then c in (( halfline 0 ) \/ DYADIC ) by XBOOLE_0:def 3;

            then c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

            hence thesis by A4, A5;

          end;

            case

             A6: 0 < b;

            set a1 = 0 ;

            consider c be Real such that

             A7: c in DYADIC and

             A8: a1 < c & c < b by A2, A6, Th24;

            c in (( halfline 0 ) \/ DYADIC ) by A7, XBOOLE_0:def 3;

            then c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

            hence thesis by A2, A8;

          end;

        end;

        hence thesis;

      end;

        suppose

         A9: a < 0 & 1 < b;

        consider a1,b1 be Real such that

         A10: a1 = 0 & b1 = 1;

        consider c be Real such that

         A11: c in DYADIC and

         A12: a1 < c & c < b1 by A10, Th24;

        take c;

        c in (( halfline 0 ) \/ DYADIC ) by A11, XBOOLE_0:def 3;

        hence thesis by A9, A10, A12, URYSOHN1:def 3, XBOOLE_0:def 3, XXREAL_0: 2;

      end;

        suppose 0 <= a & b <= 1;

        then

        consider c be Real such that

         A13: c in DYADIC and

         A14: a < c & c < b by A1, Th24;

        take c;

        c in (( halfline 0 ) \/ DYADIC ) by A13, XBOOLE_0:def 3;

        hence thesis by A14, URYSOHN1:def 3, XBOOLE_0:def 3;

      end;

        suppose

         A15: 0 <= a & 1 < b;

        now

          per cases ;

            case

             A16: 1 <= a;

            consider c be Real such that

             A17: a < c and

             A18: c < b by A1, XREAL_1: 5;

            reconsider c as Real;

            ( right_open_halfline 1) = { g where g be Real : 1 < g } & 1 < c by A16, A17, XXREAL_0: 2, XXREAL_1: 230;

            then c in ( right_open_halfline 1);

            then c in ( DYADIC \/ ( right_open_halfline 1)) by XBOOLE_0:def 3;

            then c in (( halfline 0 ) \/ ( DYADIC \/ ( right_open_halfline 1))) by XBOOLE_0:def 3;

            then c in DOM by URYSOHN1:def 3, XBOOLE_1: 4;

            hence thesis by A17, A18;

          end;

            case

             A19: a < 1;

            set b1 = 1;

            consider c be Real such that

             A20: c in DYADIC and

             A21: a < c and

             A22: c < b1 by A15, A19, Th24;

            c in (( halfline 0 ) \/ DYADIC ) by A20, XBOOLE_0:def 3;

            then

             A23: c in DOM by URYSOHN1:def 3, XBOOLE_0:def 3;

            c < b by A15, A22, XXREAL_0: 2;

            hence thesis by A21, A23;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: URYSOHN2:26

    for A be non empty Subset of ExtREAL holds for a,b be R_eal st A c= [.a, b.] holds a <= ( inf A) & ( sup A) <= b

    proof

      let A be non empty Subset of ExtREAL ;

      let a,b be R_eal;

      assume

       A1: A c= [.a, b.];

      then

      reconsider B = [.a, b.] as non empty Subset of ExtREAL by MEMBERED: 2;

      for x be ExtReal st x in B holds x <= b by XXREAL_1: 1;

      then b is UpperBound of B by XXREAL_2:def 1;

      then

       A2: b is UpperBound of A by A1, XXREAL_2: 6;

      for x be ExtReal holds (x in B implies a <= x) by XXREAL_1: 1;

      then a is LowerBound of B by XXREAL_2:def 2;

      then a is LowerBound of A by A1, XXREAL_2: 5;

      hence thesis by A2, XXREAL_2:def 3, XXREAL_2:def 4;

    end;

    theorem :: URYSOHN2:27

     0 in DYADIC & 1 in DYADIC

    proof

       0 in ( dyadic 0 ) & 1 in ( dyadic 0 ) by URYSOHN1: 6;

      hence thesis by URYSOHN1:def 2;

    end;

    theorem :: URYSOHN2:28

     DYADIC c= [. 0 , 1.]

    proof

      let x be object;

      assume

       A1: x in DYADIC ;

      then

      reconsider x as Real;

      

       A2: ex n be Nat st x in ( dyadic n) by A1, URYSOHN1:def 2;

      reconsider x as R_eal by XXREAL_0:def 1;

       0 <= x & x <= 1 by A2, URYSOHN1: 1;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: URYSOHN2:29

    for n,k be Nat st n <= k holds ( dyadic n) c= ( dyadic k)

    proof

      let n,k be Nat;

      

       A1: for s be Nat holds ( dyadic n) c= ( dyadic (n + s))

      proof

        defpred P[ Nat] means ( dyadic n) c= ( dyadic (n + $1));

        

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

        proof

          let k be Nat;

          

           A3: ( dyadic (n + k)) c= ( dyadic ((n + k) + 1)) by URYSOHN1: 5;

          assume ( dyadic n) c= ( dyadic (n + k));

          hence thesis by A3, XBOOLE_1: 1;

        end;

        

         A4: P[ 0 ];

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

        hence thesis;

      end;

      assume n <= k;

      then

      consider s be Nat such that

       A5: k = (n + s) by NAT_1: 10;

      thus thesis by A1, A5;

    end;

    theorem :: URYSOHN2:30

    

     Th30: for a,b,c,d be Real st a < c & c < b & a < d & d < b holds |.(d - c) qua Complex.| < (b - a)

    proof

      let a,b,c,d be Real;

      assume that

       A1: a < c and

       A2: c < b & a < d and

       A3: d < b;

      

       A4: (c + a) < (b + d) by A2, XREAL_1: 8;

      then (c - d) <= (b - a) by XREAL_1: 21;

      then

       A5: ( - (b - a)) <= ( - (c - d)) by XREAL_1: 24;

      

       A6: (a + d) < (c + b) by A1, A3, XREAL_1: 8;

      

       A7: |.(d - c) qua Complex.| <> (b - a)

      proof

        assume

         A8: |.(d - c) qua Complex.| = (b - a);

        

         A9: (d - c) = (b - a) or (d - c) = ( - (b - a))

        proof

          per cases ;

            suppose 0 <= (d - c);

            hence thesis by A8, ABSVALUE:def 1;

          end;

            suppose not 0 <= (d - c);

            then (b - a) = ( - (d - c)) by A8, ABSVALUE:def 1;

            hence thesis;

          end;

        end;

        now

          per cases by A9;

            case (d - c) = (b - a);

            hence thesis by A6;

          end;

            case (d - c) = ( - (b - a));

            hence thesis by A4;

          end;

        end;

        hence thesis;

      end;

      (d - c) < (b - a) by A6, XREAL_1: 21;

      then |.(d - c) qua Complex.| <= (b - a) by A5, ABSVALUE: 5;

      hence thesis by A7, XXREAL_0: 1;

    end;

    theorem :: URYSOHN2:31

    for eps be Real st 0 < eps holds for d be Real st 0 < d holds ex r1,r2 be Real st r1 in ( DYADIC \/ ( right_open_halfline 1)) & r2 in ( DYADIC \/ ( right_open_halfline 1)) & 0 < r1 & r1 < d & d < r2 & (r2 - r1) < eps

    proof

      let eps be Real;

      assume 0 < eps;

      then

      consider eps1 be Real such that

       A1: 0 < eps1 and

       A2: eps1 < eps by XREAL_1: 5;

      reconsider eps1 as Real;

      let d be Real;

      assume

       A3: 0 < d;

      per cases ;

        suppose eps1 < d;

        then

         A4: 0 < (d - eps1) by XREAL_1: 50;

        (d - eps1) < (d - 0 ) by A1, XREAL_1: 15;

        then ex c be Real st c in DOM & (d - eps1) < c & c < d by Th25;

        then

        consider r1 be Real such that

         A5: (d - eps1) < r1 and

         A6: r1 < d and

         A7: r1 in DOM ;

        r1 in (( halfline 0 ) \/ DYADIC ) or r1 in ( right_open_halfline 1) by A7, URYSOHN1:def 3, XBOOLE_0:def 3;

        then

         A8: r1 in ( halfline 0 ) or r1 in DYADIC or r1 in ( right_open_halfline 1) by XBOOLE_0:def 3;

        (eps - eps) < (eps - eps1) by A2, XREAL_1: 15;

        then (d + 0 ) < (d + (eps - eps1)) by XREAL_1: 8;

        then ex c be Real st c in DOM & d < c & c < (d + (eps - eps1)) by Th25;

        then

        consider r2 be Real such that

         A9: d < r2 and

         A10: r2 < (d + (eps - eps1)) and

         A11: r2 in DOM ;

        r2 in (( halfline 0 ) \/ DYADIC ) or r2 in ( right_open_halfline 1) by A11, URYSOHN1:def 3, XBOOLE_0:def 3;

        then

         A12: r2 in ( halfline 0 ) or r2 in DYADIC or r2 in ( right_open_halfline 1) by XBOOLE_0:def 3;

        

         A13: r1 < r2 by A6, A9, XXREAL_0: 2;

        then

         A14: (d - eps1) < r2 by A5, XXREAL_0: 2;

        take r1, r2;

        

         A15: ((d + (eps - eps1)) - (d - eps1)) = eps;

        r1 < (d + (eps - eps1)) by A10, A13, XXREAL_0: 2;

        then

         A16: |.(r2 - r1) qua Complex.| < eps by A5, A10, A14, A15, Th30;

         0 <= (r2 - r1) by A13, XREAL_1: 48;

        hence thesis by A5, A6, A9, A4, A8, A12, A16, ABSVALUE:def 1, XBOOLE_0:def 3, XXREAL_1: 233;

      end;

        suppose

         A17: d <= eps1;

        consider r1 be Real such that

         A18: r1 in DOM and

         A19: 0 < r1 and

         A20: r1 < d by A3, Th25;

        

         A21: r1 in (( halfline 0 ) \/ DYADIC ) or r1 in ( right_open_halfline 1) by A18, URYSOHN1:def 3, XBOOLE_0:def 3;

        ( 0 + d) < (r1 + eps1) by A17, A19, XREAL_1: 8;

        then ex c be Real st c in DOM & d < c & c < (r1 + eps1) by Th25;

        then

        consider r2 be Real such that

         A22: d < r2 and

         A23: r2 < (r1 + eps1) and

         A24: r2 in DOM ;

        take r1, r2;

        

         A25: r2 in (( halfline 0 ) \/ DYADIC ) or r2 in ( right_open_halfline 1) by A24, URYSOHN1:def 3, XBOOLE_0:def 3;

         not r1 in ( halfline 0 ) by A19, XXREAL_1: 233;

        then

         A26: r1 in DYADIC or r1 in ( right_open_halfline 1) by A21, XBOOLE_0:def 3;

         not r2 in ( halfline 0 ) by A3, A22, XXREAL_1: 233;

        then

         A27: r2 in DYADIC or r2 in ( right_open_halfline 1) by A25, XBOOLE_0:def 3;

        (r2 - r1) < ((r1 + eps1) - r1) by A23, XREAL_1: 9;

        hence thesis by A2, A19, A20, A22, A26, A27, XBOOLE_0:def 3, XXREAL_0: 2;

      end;

    end;

    begin

    theorem :: URYSOHN2:32

    for A be non empty Subset of REAL , x be Real st x > 0 & (x ** A) is bounded_above holds A is bounded_above by Lm1;

    theorem :: URYSOHN2:33

    for A be non empty Subset of REAL , x be Real st x > 0 & (x ** A) is bounded_below holds A is bounded_below by Lm2;