xxreal_2.miz



    begin

    scheme :: XXREAL_2:sch1

    FinInter { m,n() -> Integer , F( object) -> object , P[ object] } :

{ F(i) where i be Element of INT : m() <= i & i <= n() & P[i] } is finite;

      set F = { F(i) where i be Element of INT : m() <= i & i <= n() & P[i] };

      per cases ;

        suppose

         A1: n() < m();

        now

          assume F <> {} ;

          then

          consider x be object such that

           A2: x in F by XBOOLE_0:def 1;

          ex i be Element of INT st x = F(i) & m() <= i & i <= n() & P[i] by A2;

          hence contradiction by A1, XXREAL_0: 2;

        end;

        then

        reconsider F as empty set;

        F is finite;

        hence thesis;

      end;

        suppose m() <= n();

        then

        reconsider k = (n() - m()) as Element of NAT by INT_1: 5;

        set F = { F(i) where i be Element of INT : m() <= i & i <= n() & P[i] };

        defpred Q[ object, object] means ex i be Integer st $1 = i & $2 = F(+);

        

         A3: for e be object st e in (k + 1) holds ex u be object st Q[e, u]

        proof

          let e be object;

          assume e in (k + 1);

          then e in ( Segm (k + 1));

          then

          reconsider i = e as Nat;

          take F(+), i;

          thus thesis;

        end;

        consider f be Function such that

         A4: ( dom f) = (k + 1) and

         A5: for i be object st i in (k + 1) holds Q[i, (f . i)] from CLASSES1:sch 1( A3);

        

         A6: F c= ( rng f)

        proof

          let x be object;

          assume x in F;

          then

          consider j be Element of INT such that

           A7: x = F(j) and

           A8: m() <= j and

           A9: j <= n() and P[j];

          reconsider l = (j - m()) as Element of NAT by A8, INT_1: 5;

          l <= k by A9, XREAL_1: 9;

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

          then

           A10: l in ( Segm (k + 1)) by NAT_1: 44;

          then Q[(j - m()), (f . (j - m()))] by A5;

          

          then (f . (j - m())) = F(-)

          .= F(j);

          hence thesis by A4, A7, A10, FUNCT_1:def 3;

        end;

        ( rng f) is finite by A4, FINSET_1: 8;

        hence thesis by A6;

      end;

    end;

    reserve x,y,z,r,s for ExtReal;

    definition

      let X be ext-real-membered set;

      :: XXREAL_2:def1

      mode UpperBound of X -> ExtReal means

      : Def1: x in X implies x <= it ;

      existence

      proof

        take +infty ;

        thus thesis by XXREAL_0: 4;

      end;

      :: XXREAL_2:def2

      mode LowerBound of X -> ExtReal means

      : Def2: x in X implies it <= x;

      existence

      proof

        take -infty ;

        thus thesis by XXREAL_0: 5;

      end;

    end

    definition

      let X be ext-real-membered set;

      :: XXREAL_2:def3

      func sup X -> ExtReal means

      : Def3: it is UpperBound of X & for x be UpperBound of X holds it <= x;

      existence

      proof

        defpred Q[ object] means $1 is UpperBound of X;

        defpred P[ object] means $1 in X;

        

         A1: for r, s st P[r] & Q[s] holds r <= s by Def1;

        consider s such that

         A2: for r st P[r] holds r <= s and

         A3: for r st Q[r] holds s <= r from XXREAL_1:sch 1( A1);

        take s;

        thus s is UpperBound of X by A2, Def1;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let y, z such that

         A4: y is UpperBound of X and

         A5: for x be UpperBound of X holds y <= x and

         A6: z is UpperBound of X and

         A7: for x be UpperBound of X holds z <= x;

        

         A8: y <= z by A5, A6;

        z <= y by A4, A7;

        hence thesis by A8, XXREAL_0: 1;

      end;

      :: XXREAL_2:def4

      func inf X -> ExtReal means

      : Def4: it is LowerBound of X & for x be LowerBound of X holds x <= it ;

      existence

      proof

        defpred Q[ object] means $1 in X;

        defpred P[ object] means $1 is LowerBound of X;

        

         A9: for r, s st P[r] & Q[s] holds r <= s by Def2;

        consider s such that

         A10: for r st P[r] holds r <= s and

         A11: for r st Q[r] holds s <= r from XXREAL_1:sch 1( A9);

        take s;

        thus s is LowerBound of X by A11, Def2;

        thus thesis by A10;

      end;

      uniqueness

      proof

        let y, z such that

         A12: y is LowerBound of X and

         A13: for x be LowerBound of X holds x <= y and

         A14: z is LowerBound of X and

         A15: for x be LowerBound of X holds x <= z;

        

         A16: z <= y by A13, A14;

        y <= z by A12, A15;

        hence thesis by A16, XXREAL_0: 1;

      end;

    end

    definition

      let X be ext-real-membered set;

      :: XXREAL_2:def5

      attr X is left_end means

      : Def5: ( inf X) in X;

      :: XXREAL_2:def6

      attr X is right_end means

      : Def6: ( sup X) in X;

    end

    theorem :: XXREAL_2:1

    

     Th1: y is UpperBound of {x} iff x <= y

    proof

      x in {x} by TARSKI:def 1;

      hence y is UpperBound of {x} implies x <= y by Def1;

      assume

       A1: x <= y;

      let z;

      assume z in {x};

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: XXREAL_2:2

    

     Th2: y is LowerBound of {x} iff y <= x

    proof

      x in {x} by TARSKI:def 1;

      hence y is LowerBound of {x} implies y <= x by Def2;

      assume

       A1: y <= x;

      let z;

      assume z in {x};

      hence thesis by A1, TARSKI:def 1;

    end;

    

     Lm1: ( sup {x}) = x

    proof

      

       A1: for z be UpperBound of {x} holds x <= z

      proof

        let z be UpperBound of {x};

        x in {x} by TARSKI:def 1;

        hence thesis by Def1;

      end;

      x is UpperBound of {x} by Th1;

      hence thesis by A1, Def3;

    end;

    

     Lm2: ( inf {x}) = x

    proof

      

       A1: for z be LowerBound of {x} holds z <= x

      proof

        let z be LowerBound of {x};

        x in {x} by TARSKI:def 1;

        hence thesis by Def2;

      end;

      x is LowerBound of {x} by Th2;

      hence thesis by A1, Def4;

    end;

    registration

      cluster -> ext-real-membered for Element of ( Fin ExtREAL );

      coherence

      proof

        let X be Element of ( Fin ExtREAL );

        X c= ExtREAL by FINSUB_1:def 5;

        hence thesis;

      end;

    end

    reserve A,B for ext-real-membered set;

    theorem :: XXREAL_2:3

    

     Th3: x in A implies ( inf A) <= x

    proof

      ( inf A) is LowerBound of A by Def4;

      hence thesis by Def2;

    end;

    theorem :: XXREAL_2:4

    

     Th4: x in A implies x <= ( sup A)

    proof

      ( sup A) is UpperBound of A by Def3;

      hence thesis by Def1;

    end;

    theorem :: XXREAL_2:5

    

     Th5: B c= A implies for x be LowerBound of A holds x is LowerBound of B

    proof

      assume

       A1: B c= A;

      let x be LowerBound of A;

      let y;

      assume y in B;

      hence thesis by A1, Def2;

    end;

    theorem :: XXREAL_2:6

    

     Th6: B c= A implies for x be UpperBound of A holds x is UpperBound of B

    proof

      assume

       A1: B c= A;

      let x be UpperBound of A;

      let y;

      assume y in B;

      hence thesis by A1, Def1;

    end;

    theorem :: XXREAL_2:7

    

     Th7: for x be LowerBound of A, y be LowerBound of B holds ( min (x,y)) is LowerBound of (A \/ B)

    proof

      let x be LowerBound of A, y be LowerBound of B;

      set m = ( min (x,y));

      let z;

      assume

       A1: z in (A \/ B);

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: z in A;

        

         A3: m <= x by XXREAL_0: 17;

        x <= z by A2, Def2;

        hence thesis by A3, XXREAL_0: 2;

      end;

        suppose

         A4: z in B;

        

         A5: m <= y by XXREAL_0: 17;

        y <= z by A4, Def2;

        hence thesis by A5, XXREAL_0: 2;

      end;

    end;

    theorem :: XXREAL_2:8

    

     Th8: for x be UpperBound of A, y be UpperBound of B holds ( max (x,y)) is UpperBound of (A \/ B)

    proof

      let x be UpperBound of A, y be UpperBound of B;

      set m = ( max (x,y));

      let z;

      assume

       A1: z in (A \/ B);

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: z in A;

        

         A3: x <= m by XXREAL_0: 25;

        z <= x by A2, Def1;

        hence thesis by A3, XXREAL_0: 2;

      end;

        suppose

         A4: z in B;

        

         A5: y <= m by XXREAL_0: 25;

        z <= y by A4, Def1;

        hence thesis by A5, XXREAL_0: 2;

      end;

    end;

    theorem :: XXREAL_2:9

    

     Th9: ( inf (A \/ B)) = ( min (( inf A),( inf B)))

    proof

      set m = ( min (( inf A),( inf B)));

      

       A1: ( inf B) is LowerBound of B by Def4;

      

       A2: for x be LowerBound of (A \/ B) holds x <= m

      proof

        let x be LowerBound of (A \/ B);

        x is LowerBound of B by Th5, XBOOLE_1: 7;

        then

         A3: x <= ( inf B) by Def4;

        x is LowerBound of A by Th5, XBOOLE_1: 7;

        then x <= ( inf A) by Def4;

        hence thesis by A3, XXREAL_0: 20;

      end;

      ( inf A) is LowerBound of A by Def4;

      then m is LowerBound of (A \/ B) by A1, Th7;

      hence thesis by A2, Def4;

    end;

    theorem :: XXREAL_2:10

    

     Th10: ( sup (A \/ B)) = ( max (( sup A),( sup B)))

    proof

      set m = ( max (( sup A),( sup B)));

      

       A1: ( sup B) is UpperBound of B by Def3;

      

       A2: for x be UpperBound of (A \/ B) holds m <= x

      proof

        let x be UpperBound of (A \/ B);

        x is UpperBound of B by Th6, XBOOLE_1: 7;

        then

         A3: ( sup B) <= x by Def3;

        x is UpperBound of A by Th6, XBOOLE_1: 7;

        then ( sup A) <= x by Def3;

        hence thesis by A3, XXREAL_0: 28;

      end;

      ( sup A) is UpperBound of A by Def3;

      then m is UpperBound of (A \/ B) by A1, Th8;

      hence thesis by A2, Def3;

    end;

    registration

      cluster finite -> left_end right_end for non empty ext-real-membered set;

      coherence

      proof

        let X be non empty ext-real-membered set;

        defpred P[ non empty ext-real-membered set] means $1 is left_end right_end;

        assume

         A1: X is finite;

        X c= ExtREAL by MEMBERED: 2;

        then

         A2: X is non empty Element of ( Fin ExtREAL ) by A1, FINSUB_1:def 5;

        

         A3: for B1,B2 be non empty Element of ( Fin ExtREAL ) holds P[B1] & P[B2] implies P[(B1 \/ B2)]

        proof

          let B1,B2 be non empty Element of ( Fin ExtREAL );

          assume

           A4: P[B1];

          ( inf (B1 \/ B2)) = ( min (( inf B1),( inf B2))) by Th9;

          then

           A5: ( inf (B1 \/ B2)) = ( inf B1) or ( inf (B1 \/ B2)) = ( inf B2) by XXREAL_0: 15;

          assume

           A6: P[B2];

          then

           A7: ( inf B2) in B2 by Def5;

          ( inf B1) in B1 by A4, Def5;

          hence ( inf (B1 \/ B2)) in (B1 \/ B2) by A7, A5, XBOOLE_0:def 3;

          ( sup (B1 \/ B2)) = ( max (( sup B1),( sup B2))) by Th10;

          then

           A8: ( sup (B1 \/ B2)) = ( sup B1) or ( sup (B1 \/ B2)) = ( sup B2) by XXREAL_0: 16;

          

           A9: ( sup B2) in B2 by A6, Def6;

          ( sup B1) in B1 by A4, Def6;

          hence ( sup (B1 \/ B2)) in (B1 \/ B2) by A9, A8, XBOOLE_0:def 3;

        end;

        

         A10: for x be Element of ExtREAL holds P[ {.x.}]

        proof

          let x be Element of ExtREAL ;

          ( sup {x}) = x by Lm1;

          then

           A11: ( sup {x}) in {x} by TARSKI:def 1;

          ( inf {x}) = x by Lm2;

          then ( inf {x}) in {x} by TARSKI:def 1;

          hence thesis by A11, Def5, Def6;

        end;

        for B be non empty Element of ( Fin ExtREAL ) holds P[B] from SETWISEO:sch 3( A10, A3);

        hence thesis by A2;

      end;

    end

    registration

      cluster -> left_end for non empty natural-membered set;

      coherence

      proof

        let X be non empty natural-membered set;

        defpred P[ set] means $1 in X;

        

         A1: ex k be Nat st P[k] by MEMBERED: 12;

        consider k be Nat such that

         A2: P[k] and

         A3: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A1);

        

         A4: k is LowerBound of X

        proof

          let y;

          assume y in X;

          hence thesis by A3;

        end;

        for x be LowerBound of X holds x <= k by A2, Def2;

        hence ( inf X) in X by A2, A4, Def4;

      end;

    end

    registration

      cluster right_end for non empty natural-membered set;

      existence

      proof

        take { 0 };

        thus thesis;

      end;

    end

    notation

      let X be left_end ext-real-membered set;

      synonym min X for inf X;

    end

    notation

      let X be right_end ext-real-membered set;

      synonym max X for sup X;

    end

    definition

      let X be left_end ext-real-membered set;

      :: original: min

      redefine

      :: XXREAL_2:def7

      func min X means

      : Def7: it in X & for x st x in X holds it <= x;

      compatibility

      proof

        let y;

        thus y = ( min X) implies y in X & for x st x in X holds y <= x by Def5, Th3;

        assume that

         A1: y in X and

         A2: for x st x in X holds y <= x;

        

         A3: for x be LowerBound of X holds x <= y by A1, Def2;

        y is LowerBound of X by A2, Def2;

        hence thesis by A3, Def4;

      end;

    end

    definition

      let X be right_end ext-real-membered set;

      :: original: max

      redefine

      :: XXREAL_2:def8

      func max X means

      : Def8: it in X & for x st x in X holds x <= it ;

      compatibility

      proof

        let y;

        thus y = ( max X) implies y in X & for x st x in X holds x <= y by Def6, Th4;

        assume that

         A1: y in X and

         A2: for x st x in X holds x <= y;

        

         A3: for x be UpperBound of X holds y <= x by A1, Def1;

        y is UpperBound of X by A2, Def1;

        hence thesis by A3, Def3;

      end;

    end

    theorem :: XXREAL_2:11

    ( max {x}) = x by Lm1;

    

     Lm3: x <= y implies y is UpperBound of {x, y}

    proof

      assume

       A1: x <= y;

      let z;

      assume z in {x, y};

      hence thesis by A1, TARSKI:def 2;

    end;

    

     Lm4: for z be UpperBound of {x, y} holds y <= z

    proof

      let z be UpperBound of {x, y};

      y in {x, y} by TARSKI:def 2;

      hence thesis by Def1;

    end;

    theorem :: XXREAL_2:12

    ( max (x,y)) = ( max {x, y})

    proof

      now

        per cases ;

          case

           A1: x <= y;

          

           A2: for z be UpperBound of {x, y} holds y <= z by Lm4;

          y is UpperBound of {x, y} by A1, Lm3;

          hence ( max {x, y}) = y by A2, Def3;

        end;

          case

           A3: y < x;

          

           A4: for z be UpperBound of {x, y} holds x <= z by Lm4;

          x is UpperBound of {x, y} by A3, Lm3;

          hence ( max {x, y}) = x by A4, Def3;

        end;

      end;

      hence thesis by XXREAL_0:def 10;

    end;

    theorem :: XXREAL_2:13

    ( min {x}) = x by Lm2;

    

     Lm5: y <= x implies y is LowerBound of {x, y}

    proof

      assume

       A1: y <= x;

      let z;

      assume z in {x, y};

      hence thesis by A1, TARSKI:def 2;

    end;

    

     Lm6: for z be LowerBound of {x, y} holds z <= y

    proof

      let z be LowerBound of {x, y};

      y in {x, y} by TARSKI:def 2;

      hence thesis by Def2;

    end;

    theorem :: XXREAL_2:14

    ( min {x, y}) = ( min (x,y))

    proof

      now

        per cases ;

          case

           A1: y <= x;

          

           A2: for z be LowerBound of {x, y} holds z <= y by Lm6;

          y is LowerBound of {x, y} by A1, Lm5;

          hence ( min {x, y}) = y by A2, Def4;

        end;

          case

           A3: x < y;

          

           A4: for z be LowerBound of {x, y} holds z <= x by Lm6;

          x is LowerBound of {x, y} by A3, Lm5;

          hence ( min {x, y}) = x by A4, Def4;

        end;

      end;

      hence thesis by XXREAL_0:def 9;

    end;

    definition

      let X be ext-real-membered set;

      :: XXREAL_2:def9

      attr X is bounded_below means

      : Def9: ex r be Real st r is LowerBound of X;

      :: XXREAL_2:def10

      attr X is bounded_above means

      : Def10: ex r be Real st r is UpperBound of X;

    end

    registration

      cluster non empty finite natural-membered for set;

      existence

      proof

        take { 0 };

        thus thesis;

      end;

    end

    definition

      let X be ext-real-membered set;

      :: XXREAL_2:def11

      attr X is real-bounded means X is bounded_below bounded_above;

    end

    registration

      cluster real-bounded -> bounded_above bounded_below for ext-real-membered set;

      coherence ;

      cluster bounded_above bounded_below -> real-bounded for ext-real-membered set;

      coherence ;

    end

    registration

      cluster finite -> real-bounded for real-membered set;

      coherence

      proof

        let X be real-membered set;

        assume

         A1: X is finite;

        per cases ;

          suppose

           A2: X is empty;

          thus X is bounded_below

          proof

            take 0 ;

            let x;

            thus thesis by A2;

          end;

          take 0 ;

          let x;

          thus thesis by A2;

        end;

          suppose X is non empty;

          then

          reconsider Y = X as non empty finite real-membered set by A1;

          ( inf Y) in X by Def5;

          then

          reconsider m = ( inf X) as Real;

          thus X is bounded_below

          proof

            take m;

            let x;

            assume x in X;

            hence thesis by Th3;

          end;

          ( sup Y) in X by Def6;

          then

          reconsider m = ( sup X) as Real;

          take m;

          let x;

          assume x in X;

          hence thesis by Th4;

        end;

      end;

    end

    registration

      cluster real-bounded for non empty natural-membered set;

      existence

      proof

        take { 0 };

        thus thesis;

      end;

    end

    theorem :: XXREAL_2:15

    

     Th15: for X be non empty real-membered set st X is bounded_below holds ( inf X) in REAL

    proof

      let X be non empty real-membered set;

      given r be Real such that

       A1: r is LowerBound of X;

      consider s be Real such that

       A2: s in X by MEMBERED: 9;

      

       A3: ( inf X) <= s by A2, Th3;

      

       A4: r in REAL by XREAL_0:def 1;

      

       A5: s in REAL by XREAL_0:def 1;

      r <= ( inf X) by A1, Def4;

      hence thesis by A4, A5, A3, XXREAL_0: 45;

    end;

    theorem :: XXREAL_2:16

    

     Th16: for X be non empty real-membered set st X is bounded_above holds ( sup X) in REAL

    proof

      let X be non empty real-membered set;

      given r be Real such that

       A1: r is UpperBound of X;

      consider s be Real such that

       A2: s in X by MEMBERED: 9;

      

       A3: s <= ( sup X) by A2, Th4;

      

       A4: r in REAL by XREAL_0:def 1;

      

       A5: s in REAL by XREAL_0:def 1;

      ( sup X) <= r by A1, Def3;

      hence thesis by A4, A5, A3, XXREAL_0: 45;

    end;

    registration

      let X be bounded_above non empty real-membered set;

      cluster ( sup X) -> real;

      coherence

      proof

        ( sup X) in REAL by Th16;

        hence thesis;

      end;

    end

    registration

      let X be bounded_below non empty real-membered set;

      cluster ( inf X) -> real;

      coherence

      proof

        ( inf X) in REAL by Th15;

        hence thesis;

      end;

    end

    registration

      cluster bounded_above -> right_end for non empty integer-membered set;

      coherence

      proof

        let X be non empty integer-membered set;

        assume X is bounded_above;

        then

        reconsider Y = X as bounded_above non empty integer-membered set;

        set s = ( sup Y);

        

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

         [\s/] is UpperBound of X

        proof

          let x;

          assume x in X;

          hence thesis by Th4, INT_1: 54;

        end;

        then s <= [\s/] by Def3;

        then

        reconsider s as Integer by A1, XXREAL_0: 1;

        assume

         A2: not ( sup X) in X;

        (s - 1) is UpperBound of X

        proof

          let x;

          assume

           A3: x in X;

          then

          reconsider i = x as Integer;

          i <= s by A3, Th4;

          then i < s by A2, A3, XXREAL_0: 1;

          hence thesis by INT_1: 52;

        end;

        then (s - 1) >= s by Def3;

        hence contradiction by XREAL_1: 146;

      end;

    end

    registration

      cluster bounded_below -> left_end for non empty integer-membered set;

      coherence

      proof

        let X be non empty integer-membered set;

        assume X is bounded_below;

        then

        reconsider Y = X as bounded_below non empty integer-membered set;

        set s = ( inf Y);

        

         A1: [/s\] >= s by INT_1:def 7;

         [/s\] is LowerBound of X

        proof

          let x;

          assume x in X;

          hence thesis by Th3, INT_1: 65;

        end;

        then [/s\] <= s by Def4;

        then

        reconsider s as Integer by A1, XXREAL_0: 1;

        assume

         A2: not ( inf X) in X;

        (s + 1) is LowerBound of X

        proof

          let x;

          assume

           A3: x in X;

          then

          reconsider i = x as Integer;

          i >= s by A3, Th3;

          then s < i by A2, A3, XXREAL_0: 1;

          hence thesis by INT_1: 7;

        end;

        then (s + 1) <= s by Def4;

        hence contradiction by XREAL_1: 145;

      end;

    end

    registration

      cluster -> bounded_below for natural-membered set;

      coherence

      proof

        let X be natural-membered set;

        take 0 ;

        let x;

        assume x in X;

        hence thesis;

      end;

    end

    registration

      let X be left_end real-membered set;

      cluster ( min X) -> real;

      coherence

      proof

        ( min X) in X by Def7;

        hence thesis;

      end;

    end

    registration

      let X be left_end rational-membered set;

      cluster ( min X) -> rational;

      coherence

      proof

        ( min X) in X by Def7;

        hence thesis;

      end;

    end

    registration

      let X be left_end integer-membered set;

      cluster ( min X) -> integer;

      coherence

      proof

        ( min X) in X by Def7;

        hence thesis;

      end;

    end

    registration

      let X be left_end natural-membered set;

      cluster ( min X) -> natural;

      coherence

      proof

        ( min X) in X by Def7;

        hence thesis;

      end;

    end

    registration

      let X be right_end real-membered set;

      cluster ( max X) -> real;

      coherence

      proof

        ( max X) in X by Def8;

        hence thesis;

      end;

    end

    registration

      let X be right_end rational-membered set;

      cluster ( max X) -> rational;

      coherence

      proof

        ( max X) in X by Def8;

        hence thesis;

      end;

    end

    registration

      let X be right_end integer-membered set;

      cluster ( max X) -> integer;

      coherence

      proof

        ( max X) in X by Def8;

        hence thesis;

      end;

    end

    registration

      let X be right_end natural-membered set;

      cluster ( max X) -> natural;

      coherence

      proof

        ( max X) in X by Def8;

        hence thesis;

      end;

    end

    registration

      cluster left_end -> bounded_below for real-membered set;

      coherence

      proof

        let X be real-membered set;

        assume ( inf X) in X;

        then

        reconsider r = ( inf X) as Real;

        take r;

        let x;

        thus thesis by Th3;

      end;

      cluster right_end -> bounded_above for real-membered set;

      coherence

      proof

        let X be real-membered set;

        assume ( sup X) in X;

        then

        reconsider r = ( sup X) as Real;

        take r;

        let x;

        thus thesis by Th4;

      end;

    end

    theorem :: XXREAL_2:17

    

     Th17: x is LowerBound of [.x, y.]

    proof

      let z;

      assume z in [.x, y.];

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: XXREAL_2:18

    

     Th18: x is LowerBound of ].x, y.]

    proof

      let z;

      assume z in ].x, y.];

      hence thesis by XXREAL_1: 2;

    end;

    theorem :: XXREAL_2:19

    

     Th19: x is LowerBound of [.x, y.[

    proof

      let z;

      assume z in [.x, y.[;

      hence thesis by XXREAL_1: 3;

    end;

    theorem :: XXREAL_2:20

    

     Th20: x is LowerBound of ].x, y.[

    proof

      let z;

      assume z in ].x, y.[;

      hence thesis by XXREAL_1: 4;

    end;

    theorem :: XXREAL_2:21

    

     Th21: y is UpperBound of [.x, y.]

    proof

      let z;

      assume z in [.x, y.];

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: XXREAL_2:22

    

     Th22: y is UpperBound of ].x, y.]

    proof

      let z;

      assume z in ].x, y.];

      hence thesis by XXREAL_1: 2;

    end;

    theorem :: XXREAL_2:23

    

     Th23: y is UpperBound of [.x, y.[

    proof

      let z;

      assume z in [.x, y.[;

      hence thesis by XXREAL_1: 3;

    end;

    theorem :: XXREAL_2:24

    

     Th24: y is UpperBound of ].x, y.[

    proof

      let z;

      assume z in ].x, y.[;

      hence thesis by XXREAL_1: 4;

    end;

    theorem :: XXREAL_2:25

    

     Th25: x <= y implies ( inf [.x, y.]) = x

    proof

      assume

       A1: x <= y;

      

       A2: for z be LowerBound of [.x, y.] holds z <= x

      proof

        let z be LowerBound of [.x, y.];

        x in [.x, y.] by A1, XXREAL_1: 1;

        hence thesis by Def2;

      end;

      x is LowerBound of [.x, y.] by Th17;

      hence thesis by A2, Def4;

    end;

    theorem :: XXREAL_2:26

    

     Th26: x < y implies ( inf [.x, y.[) = x

    proof

      assume

       A1: x < y;

      

       A2: for z be LowerBound of [.x, y.[ holds z <= x

      proof

        let z be LowerBound of [.x, y.[;

        x in [.x, y.[ by A1, XXREAL_1: 3;

        hence thesis by Def2;

      end;

      x is LowerBound of [.x, y.[ by Th19;

      hence thesis by A2, Def4;

    end;

    theorem :: XXREAL_2:27

    

     Th27: x < y implies ( inf ].x, y.]) = x

    proof

      assume

       A1: x < y;

      

       A2: for z be LowerBound of ].x, y.] holds z <= x

      proof

        let z be LowerBound of ].x, y.];

        for r st x < r & r < y holds z <= r

        proof

          let r;

          assume that

           A3: x < r and

           A4: r < y;

          r in ].x, y.] by A3, A4, XXREAL_1: 2;

          hence thesis by Def2;

        end;

        hence thesis by A1, XREAL_1: 228;

      end;

      x is LowerBound of ].x, y.] by Th18;

      hence thesis by A2, Def4;

    end;

    theorem :: XXREAL_2:28

    

     Th28: x < y implies ( inf ].x, y.[) = x

    proof

      assume

       A1: x < y;

      

       A2: for z be LowerBound of ].x, y.[ holds z <= x

      proof

        let z be LowerBound of ].x, y.[;

        for r st x < r & r < y holds z <= r by XXREAL_1: 4, Def2;

        hence thesis by A1, XREAL_1: 228;

      end;

      x is LowerBound of ].x, y.[ by Th20;

      hence thesis by A2, Def4;

    end;

    theorem :: XXREAL_2:29

    

     Th29: x <= y implies ( sup [.x, y.]) = y

    proof

      assume

       A1: x <= y;

      

       A2: for z be UpperBound of [.x, y.] holds y <= z

      proof

        let z be UpperBound of [.x, y.];

        y in [.x, y.] by A1, XXREAL_1: 1;

        hence thesis by Def1;

      end;

      y is UpperBound of [.x, y.] by Th21;

      hence thesis by A2, Def3;

    end;

    theorem :: XXREAL_2:30

    

     Th30: x < y implies ( sup ].x, y.]) = y

    proof

      assume

       A1: x < y;

      

       A2: for z be UpperBound of ].x, y.] holds y <= z

      proof

        let z be UpperBound of ].x, y.];

        y in ].x, y.] by A1, XXREAL_1: 2;

        hence thesis by Def1;

      end;

      y is UpperBound of ].x, y.] by Th22;

      hence thesis by A2, Def3;

    end;

    theorem :: XXREAL_2:31

    

     Th31: x < y implies ( sup [.x, y.[) = y

    proof

      assume

       A1: x < y;

      

       A2: for z be UpperBound of [.x, y.[ holds y <= z

      proof

        let z be UpperBound of [.x, y.[;

        for r st x < r & r < y holds r <= z

        proof

          let r;

          assume that

           A3: x < r and

           A4: r < y;

          r in [.x, y.[ by A3, A4, XXREAL_1: 3;

          hence thesis by Def1;

        end;

        hence thesis by A1, XREAL_1: 229;

      end;

      y is UpperBound of [.x, y.[ by Th23;

      hence thesis by A2, Def3;

    end;

    theorem :: XXREAL_2:32

    

     Th32: x < y implies ( sup ].x, y.[) = y

    proof

      assume

       A1: x < y;

      

       A2: for z be UpperBound of ].x, y.[ holds y <= z

      proof

        let z be UpperBound of ].x, y.[;

        for r st x < r & r < y holds r <= z by XXREAL_1: 4, Def1;

        hence thesis by A1, XREAL_1: 229;

      end;

      y is UpperBound of ].x, y.[ by Th24;

      hence thesis by A2, Def3;

    end;

    theorem :: XXREAL_2:33

    

     Th33: x <= y implies [.x, y.] is left_end right_end

    proof

      assume

       A1: x <= y;

      then x in [.x, y.] by XXREAL_1: 1;

      then ( inf [.x, y.]) in [.x, y.] by A1, Th25;

      hence [.x, y.] is left_end;

      y in [.x, y.] by A1, XXREAL_1: 1;

      hence ( sup [.x, y.]) in [.x, y.] by A1, Th29;

    end;

    theorem :: XXREAL_2:34

    

     Th34: x < y implies [.x, y.[ is left_end

    proof

      assume

       A1: x < y;

      then x in [.x, y.[ by XXREAL_1: 3;

      hence ( inf [.x, y.[) in [.x, y.[ by A1, Th26;

    end;

    theorem :: XXREAL_2:35

    

     Th35: x < y implies ].x, y.] is right_end

    proof

      assume

       A1: x < y;

      then y in ].x, y.] by XXREAL_1: 2;

      hence ( sup ].x, y.]) in ].x, y.] by A1, Th30;

    end;

    theorem :: XXREAL_2:36

    

     Th36: x is LowerBound of {}

    proof

      let y;

      thus thesis;

    end;

    theorem :: XXREAL_2:37

    

     Th37: x is UpperBound of {}

    proof

      let y;

      thus thesis;

    end;

    theorem :: XXREAL_2:38

    

     Th38: ( inf {} ) = +infty

    proof

      

       A1: for x be LowerBound of {} holds x <= +infty by XXREAL_0: 3;

       +infty is LowerBound of {} by Th36;

      hence thesis by A1, Def4;

    end;

    theorem :: XXREAL_2:39

    

     Th39: ( sup {} ) = -infty

    proof

      

       A1: for x be UpperBound of {} holds -infty <= x by XXREAL_0: 5;

       -infty is UpperBound of {} by Th37;

      hence thesis by A1, Def3;

    end;

    theorem :: XXREAL_2:40

    

     Th40: for X be ext-real-membered set holds X is non empty iff ( inf X) <= ( sup X)

    proof

      let X be ext-real-membered set;

      thus X is non empty implies ( inf X) <= ( sup X)

      proof

        assume X is non empty;

        then

        consider x such that

         A1: x in X by MEMBERED: 8;

        

         A2: x <= ( sup X) by A1, Th4;

        ( inf X) <= x by A1, Th3;

        hence thesis by A2, XXREAL_0: 2;

      end;

      assume ( inf X) <= ( sup X);

      hence thesis by Th38, Th39;

    end;

    registration

      cluster real-bounded -> finite for integer-membered set;

      coherence

      proof

        let X be integer-membered set;

        per cases ;

          suppose X is empty;

          hence thesis;

        end;

          suppose

           A1: X is non empty;

          assume X is bounded_below bounded_above;

          then

          reconsider Z = X as bounded_below bounded_above non empty integer-membered set by A1;

          set m = ( inf Z), n = ( sup Z);

          defpred P[ object] means $1 in X;

          deffunc F( object) = $1;

          set Y = { F(i) where i be Element of INT : m <= i & i <= n & P[i] };

          

           A2: X c= Y

          proof

            let i be Integer;

            

             A3: i in INT by INT_1:def 2;

            assume

             A4: P[i];

            then

             A5: i <= n by Th4;

            m <= i by A4, Th3;

            hence thesis by A3, A4, A5;

          end;

          Y is finite from FinInter;

          hence thesis by A2;

        end;

      end;

    end

    registration

      cluster -> finite for bounded_above natural-membered set;

      coherence ;

    end

    theorem :: XXREAL_2:41

    for X be ext-real-membered set holds +infty is UpperBound of X

    proof

      let X be ext-real-membered set;

      let x such that x in X;

      thus thesis by XXREAL_0: 3;

    end;

    theorem :: XXREAL_2:42

    for X be ext-real-membered set holds -infty is LowerBound of X

    proof

      let X be ext-real-membered set;

      let x such that x in X;

      thus thesis by XXREAL_0: 5;

    end;

    theorem :: XXREAL_2:43

    

     Th43: for X,Y be ext-real-membered set st X c= Y & Y is bounded_above holds X is bounded_above

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      given r be Real such that

       A2: r is UpperBound of Y;

      take r;

      thus thesis by A1, A2, Th6;

    end;

    theorem :: XXREAL_2:44

    

     Th44: for X,Y be ext-real-membered set st X c= Y & Y is bounded_below holds X is bounded_below

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      given r be Real such that

       A2: r is LowerBound of Y;

      take r;

      thus thesis by A1, A2, Th5;

    end;

    theorem :: XXREAL_2:45

    for X,Y be ext-real-membered set st X c= Y & Y is real-bounded holds X is real-bounded by Th43, Th44;

    theorem :: XXREAL_2:46

    

     Th46: REAL is non bounded_below non bounded_above

    proof

      thus REAL is non bounded_below

      proof

        given r be Real such that

         A1: r is LowerBound of REAL ;

        consider s be Real such that

         A2: s < r by XREAL_1: 2;

        s in REAL by XREAL_0:def 1;

        hence contradiction by A1, A2, Def2;

      end;

      given r be Real such that

       A3: r is UpperBound of REAL ;

      consider s be Real such that

       A4: r < s by XREAL_1: 1;

      s in REAL by XREAL_0:def 1;

      hence contradiction by A3, A4, Def1;

    end;

    registration

      cluster REAL -> non bounded_below non bounded_above;

      coherence by Th46;

    end

    theorem :: XXREAL_2:47

     { +infty } is bounded_below

    proof

      take 0 ;

      let x;

      assume x in { +infty };

      hence thesis by TARSKI:def 1;

    end;

    theorem :: XXREAL_2:48

     { -infty } is bounded_above

    proof

      take 0 ;

      let x;

      assume x in { -infty };

      hence thesis by TARSKI:def 1;

    end;

    theorem :: XXREAL_2:49

    

     Th49: for X be bounded_above non empty ext-real-membered set st X <> { -infty } holds ex x be Element of REAL st x in X

    proof

      let X be bounded_above non empty ext-real-membered set;

      assume X <> { -infty };

      then

      consider x be object such that

       A1: x in X and

       A2: x <> -infty by ZFMISC_1: 35;

      reconsider x as ExtReal by A1;

      consider r be Real such that

       A3: r is UpperBound of X by Def10;

      

       A4: r in REAL by XREAL_0:def 1;

      x <= r by A3, A1, Def1;

      then x in REAL by A4, A2, XXREAL_0: 13;

      hence thesis by A1;

    end;

    theorem :: XXREAL_2:50

    

     Th50: for X be bounded_below non empty ext-real-membered set st X <> { +infty } holds ex x be Element of REAL st x in X

    proof

      let X be bounded_below non empty ext-real-membered set;

      assume X <> { +infty };

      then

      consider x be object such that

       A1: x in X and

       A2: x <> +infty by ZFMISC_1: 35;

      reconsider x as ExtReal by A1;

      consider r be Real such that

       A3: r is LowerBound of X by Def9;

      

       A4: r in REAL by XREAL_0:def 1;

      r <= x by A3, A1, Def2;

      then x in REAL by A4, A2, XXREAL_0: 10;

      hence thesis by A1;

    end;

    theorem :: XXREAL_2:51

    

     Th51: for X be ext-real-membered set st -infty is UpperBound of X holds X c= { -infty }

    proof

      let X be ext-real-membered set such that

       A1: -infty is UpperBound of X;

      let x;

      assume x in X;

      then x = -infty by A1, Def1, XXREAL_0: 6;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: XXREAL_2:52

    

     Th52: for X be ext-real-membered set st +infty is LowerBound of X holds X c= { +infty }

    proof

      let X be ext-real-membered set such that

       A1: +infty is LowerBound of X;

      let x;

      assume x in X;

      then x = +infty by A1, Def2, XXREAL_0: 4;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: XXREAL_2:53

    for X be non empty ext-real-membered set st ex y be UpperBound of X st y <> +infty holds X is bounded_above

    proof

      let X be non empty ext-real-membered set;

      given y be UpperBound of X such that

       A1: y <> +infty ;

      per cases ;

        suppose

         A2: y = -infty ;

        take 0 ;

        let x;

        assume

         A3: x in X;

        X c= { -infty } by A2, Th51;

        hence thesis by A3, TARSKI:def 1;

      end;

        suppose y <> -infty ;

        then y in REAL by A1, XXREAL_0: 14;

        then

        reconsider y as Real;

        take y;

        thus thesis;

      end;

    end;

    theorem :: XXREAL_2:54

    for X be non empty ext-real-membered set st ex y be LowerBound of X st y <> -infty holds X is bounded_below

    proof

      let X be non empty ext-real-membered set;

      given y be LowerBound of X such that

       A1: y <> -infty ;

      per cases ;

        suppose

         A2: y = +infty ;

        take 0 ;

        let x;

        assume

         A3: x in X;

        X c= { +infty } by A2, Th52;

        hence thesis by A3, TARSKI:def 1;

      end;

        suppose y <> +infty ;

        then y in REAL by A1, XXREAL_0: 14;

        then

        reconsider y as Real;

        take y;

        thus thesis;

      end;

    end;

    theorem :: XXREAL_2:55

    for X be non empty ext-real-membered set, x be UpperBound of X st x in X holds x = ( sup X)

    proof

      let X be non empty ext-real-membered set, x be UpperBound of X;

      assume x in X;

      then for y be UpperBound of X holds x <= y by Def1;

      hence thesis by Def3;

    end;

    theorem :: XXREAL_2:56

    for X be non empty ext-real-membered set, x be LowerBound of X st x in X holds x = ( inf X)

    proof

      let X be non empty ext-real-membered set, x be LowerBound of X;

      assume x in X;

      then for y be LowerBound of X holds y <= x by Def2;

      hence thesis by Def4;

    end;

    theorem :: XXREAL_2:57

    

     Th57: for X be non empty ext-real-membered set st X is bounded_above & X <> { -infty } holds ( sup X) in REAL

    proof

      let X be non empty ext-real-membered set;

      assume

       A1: X is bounded_above;

      then

      consider r be Real such that

       A2: r is UpperBound of X;

      assume X <> { -infty };

      then

       A3: ex x be Element of REAL st x in X by A1, Th49;

      ( sup X) is UpperBound of X by Def3;

      then

       A4: not ( sup X) = -infty by A3, Def1, XXREAL_0: 12;

      

       A5: r in REAL by XREAL_0:def 1;

      ( sup X) <= r by A2, Def3;

      hence thesis by A5, A4, XXREAL_0: 13;

    end;

    theorem :: XXREAL_2:58

    

     Th58: for X be non empty ext-real-membered set st X is bounded_below & X <> { +infty } holds ( inf X) in REAL

    proof

      let X be non empty ext-real-membered set;

      assume

       A1: X is bounded_below;

      then

      consider r be Real such that

       A2: r is LowerBound of X;

      assume X <> { +infty };

      then

       A3: ex x be Element of REAL st x in X by A1, Th50;

      ( inf X) is LowerBound of X by Def4;

      then

       A4: ( inf X) <> +infty by A3, Def2, XXREAL_0: 9;

      

       A5: r in REAL by XREAL_0:def 1;

      r <= ( inf X) by A2, Def4;

      hence thesis by A5, A4, XXREAL_0: 10;

    end;

    theorem :: XXREAL_2:59

    for X,Y be ext-real-membered set st X c= Y holds ( sup X) <= ( sup Y)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      ( sup Y) is UpperBound of Y by Def3;

      then ( sup Y) is UpperBound of X by A1, Th6;

      hence thesis by Def3;

    end;

    theorem :: XXREAL_2:60

    for X,Y be ext-real-membered set st X c= Y holds ( inf Y) <= ( inf X)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      ( inf Y) is LowerBound of Y by Def4;

      then ( inf Y) is LowerBound of X by A1, Th5;

      hence thesis by Def4;

    end;

    theorem :: XXREAL_2:61

    for X be ext-real-membered set, x be ExtReal st (ex y be ExtReal st y in X & x <= y) holds x <= ( sup X)

    proof

      let X be ext-real-membered set;

      let x be ExtReal;

      given y be ExtReal such that

       A1: y in X and

       A2: x <= y;

      y <= ( sup X) by A1, Th4;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: XXREAL_2:62

    for X be ext-real-membered set, x be ExtReal st (ex y be ExtReal st y in X & y <= x) holds ( inf X) <= x

    proof

      let X be ext-real-membered set;

      let x be ExtReal;

      given y be ExtReal such that

       A1: y in X and

       A2: y <= x;

      ( inf X) <= y by A1, Th3;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: XXREAL_2:63

    for X,Y be ext-real-membered set st for x be ExtReal st x in X holds ex y be ExtReal st y in Y & x <= y holds ( sup X) <= ( sup Y)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: for x be ExtReal st x in X holds ex y be ExtReal st y in Y & x <= y;

      ( sup Y) is UpperBound of X

      proof

        let x be ExtReal;

        assume x in X;

        then

        consider y be ExtReal such that

         A2: y in Y and

         A3: x <= y by A1;

        y <= ( sup Y) by A2, Th4;

        hence thesis by A3, XXREAL_0: 2;

      end;

      hence thesis by Def3;

    end;

    theorem :: XXREAL_2:64

    for X,Y be ext-real-membered set st for y be ExtReal st y in Y holds ex x be ExtReal st x in X & x <= y holds ( inf X) <= ( inf Y)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: for y be ExtReal st y in Y holds ex x be ExtReal st x in X & x <= y;

      ( inf X) is LowerBound of Y

      proof

        let y be ExtReal;

        assume y in Y;

        then

        consider x be ExtReal such that

         A2: x in X and

         A3: x <= y by A1;

        ( inf X) <= x by A2, Th3;

        hence thesis by A3, XXREAL_0: 2;

      end;

      hence thesis by Def4;

    end;

    theorem :: XXREAL_2:65

    

     Th65: for X,Y be ext-real-membered set, x be UpperBound of X, y be UpperBound of Y holds ( min (x,y)) is UpperBound of (X /\ Y)

    proof

      let X,Y be ext-real-membered set, x be UpperBound of X, y be UpperBound of Y;

      let a be ExtReal;

      assume

       A1: a in (X /\ Y);

      then a in Y by XBOOLE_0:def 4;

      then

       A2: a <= y by Def1;

      a in X by A1, XBOOLE_0:def 4;

      then a <= x by Def1;

      hence thesis by A2, XXREAL_0: 20;

    end;

    theorem :: XXREAL_2:66

    

     Th66: for X,Y be ext-real-membered set, x be LowerBound of X, y be LowerBound of Y holds ( max (x,y)) is LowerBound of (X /\ Y)

    proof

      let X,Y be ext-real-membered set, x be LowerBound of X, y be LowerBound of Y;

      let a be ExtReal;

      assume

       A1: a in (X /\ Y);

      then a in Y by XBOOLE_0:def 4;

      then

       A2: y <= a by Def2;

      a in X by A1, XBOOLE_0:def 4;

      then x <= a by Def2;

      hence thesis by A2, XXREAL_0: 28;

    end;

    theorem :: XXREAL_2:67

    for X,Y be ext-real-membered set holds ( sup (X /\ Y)) <= ( min (( sup X),( sup Y)))

    proof

      let X,Y be ext-real-membered set;

      

       A1: ( sup Y) is UpperBound of Y by Def3;

      ( sup X) is UpperBound of X by Def3;

      then ( min (( sup X),( sup Y))) is UpperBound of (X /\ Y) by A1, Th65;

      hence thesis by Def3;

    end;

    theorem :: XXREAL_2:68

    for X,Y be ext-real-membered set holds ( max (( inf X),( inf Y))) <= ( inf (X /\ Y))

    proof

      let X,Y be ext-real-membered set;

      

       A1: ( inf Y) is LowerBound of Y by Def4;

      ( inf X) is LowerBound of X by Def4;

      then ( max (( inf X),( inf Y))) is LowerBound of (X /\ Y) by A1, Th66;

      hence thesis by Def4;

    end;

    registration

      cluster real-bounded -> real-membered for ext-real-membered set;

      coherence

      proof

        let X be ext-real-membered set such that

         A1: X is real-bounded;

        let x be object;

        assume

         A2: x in X;

        then

        reconsider X as non empty ext-real-membered set;

        consider s be Real such that

         A3: s is UpperBound of X by A1, Def10;

        reconsider x as ExtReal by A2;

        

         A4: s in REAL by XREAL_0:def 1;

        

         A5: x <= s by A2, A3, Def1;

        consider r be Real such that

         A6: r is LowerBound of X by A1, Def9;

        

         A7: r in REAL by XREAL_0:def 1;

        r <= x by A2, A6, Def2;

        then x in REAL by A5, A7, A4, XXREAL_0: 45;

        hence thesis;

      end;

    end

    theorem :: XXREAL_2:69

    

     Th69: A c= [.( inf A), ( sup A).]

    proof

      let x be ExtReal;

      assume

       A1: x in A;

      then

       A2: x <= ( sup A) by Th4;

      ( inf A) <= x by A1, Th3;

      hence thesis by A2, XXREAL_1: 1;

    end;

    theorem :: XXREAL_2:70

    ( sup A) = ( inf A) implies A = {( inf A)}

    proof

      assume

       A1: ( sup A) = ( inf A);

      then A c= [.( inf A), ( inf A).] by Th69;

      then

       A2: A c= {( inf A)} by XXREAL_1: 17;

      A <> {} by A1, Th38, Th39;

      hence thesis by A2, ZFMISC_1: 33;

    end;

    theorem :: XXREAL_2:71

    

     Th71: x <= y & x is UpperBound of A implies y is UpperBound of A

    proof

      assume that

       A1: x <= y and

       A2: x is UpperBound of A;

      let z;

      assume z in A;

      then z <= x by A2, Def1;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: XXREAL_2:72

    

     Th72: y <= x & x is LowerBound of A implies y is LowerBound of A

    proof

      assume that

       A1: y <= x and

       A2: x is LowerBound of A;

      let z;

      assume z in A;

      then x <= z by A2, Def2;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: XXREAL_2:73

    A is bounded_above iff ( sup A) <> +infty

    proof

      hereby

        assume

         A1: A is bounded_above;

        per cases by A1, Th57;

          suppose A = {} ;

          hence ( sup A) <> +infty by Th39;

        end;

          suppose A = { -infty };

          hence ( sup A) <> +infty by Lm1;

        end;

          suppose ( sup A) in REAL ;

          hence ( sup A) <> +infty ;

        end;

      end;

      assume

       A2: ( sup A) <> +infty ;

      per cases by A2, XXREAL_0: 14;

        suppose

         A3: ( sup A) = -infty ;

        take 0 ;

         -infty is UpperBound of A by A3, Def3;

        hence thesis by Th71;

      end;

        suppose ( sup A) in REAL ;

        then

        reconsider r = ( sup A) as Real;

        take r;

        thus thesis by Def3;

      end;

    end;

    theorem :: XXREAL_2:74

    A is bounded_below iff ( inf A) <> -infty

    proof

      hereby

        assume

         A1: A is bounded_below;

        per cases by A1, Th58;

          suppose A = {} ;

          hence ( inf A) <> -infty by Th38;

        end;

          suppose A = { +infty };

          hence ( inf A) <> -infty by Lm2;

        end;

          suppose ( inf A) in REAL ;

          hence ( inf A) <> -infty ;

        end;

      end;

      assume

       A2: ( inf A) <> -infty ;

      per cases by A2, XXREAL_0: 14;

        suppose

         A3: ( inf A) = +infty ;

        take 0 ;

         +infty is LowerBound of A by A3, Def4;

        hence thesis by Th72;

      end;

        suppose ( inf A) in REAL ;

        then

        reconsider r = ( inf A) as Real;

        take r;

        thus thesis by Def4;

      end;

    end;

    begin

    definition

      let A be ext-real-membered set;

      :: XXREAL_2:def12

      attr A is interval means

      : Def12: for r,s be ExtReal st r in A & s in A holds [.r, s.] c= A;

    end

    registration

      cluster ExtREAL -> interval;

      coherence by MEMBERED: 2;

      cluster empty -> interval for ext-real-membered set;

      coherence ;

      let r, s;

      cluster [.r, s.] -> interval;

      coherence

      proof

        let x, y;

        assume x in [.r, s.];

        then

         A1: r <= x by XXREAL_1: 1;

        assume y in [.r, s.];

        then

         A2: y <= s by XXREAL_1: 1;

        let z;

        assume

         A3: z in [.x, y.];

        then x <= z by XXREAL_1: 1;

        then

         A4: r <= z by A1, XXREAL_0: 2;

        z <= y by A3, XXREAL_1: 1;

        then z <= s by A2, XXREAL_0: 2;

        hence thesis by A4, XXREAL_1: 1;

      end;

      cluster ].r, s.] -> interval;

      coherence

      proof

        let x, y;

        assume x in ].r, s.];

        then

         A5: r < x by XXREAL_1: 2;

        assume y in ].r, s.];

        then

         A6: y <= s by XXREAL_1: 2;

        let z;

        assume

         A7: z in [.x, y.];

        then x <= z by XXREAL_1: 1;

        then

         A8: r < z by A5, XXREAL_0: 2;

        z <= y by A7, XXREAL_1: 1;

        then z <= s by A6, XXREAL_0: 2;

        hence thesis by A8, XXREAL_1: 2;

      end;

      cluster [.r, s.[ -> interval;

      coherence

      proof

        let x, y;

        assume x in [.r, s.[;

        then

         A9: r <= x by XXREAL_1: 3;

        assume y in [.r, s.[;

        then

         A10: y < s by XXREAL_1: 3;

        let z;

        assume

         A11: z in [.x, y.];

        then x <= z by XXREAL_1: 1;

        then

         A12: r <= z by A9, XXREAL_0: 2;

        z <= y by A11, XXREAL_1: 1;

        then z < s by A10, XXREAL_0: 2;

        hence thesis by A12, XXREAL_1: 3;

      end;

      cluster ].r, s.[ -> interval;

      coherence

      proof

        let x, y;

        assume x in ].r, s.[;

        then

         A13: r < x by XXREAL_1: 4;

        assume y in ].r, s.[;

        then

         A14: y < s by XXREAL_1: 4;

        let z;

        assume

         A15: z in [.x, y.];

        then x <= z by XXREAL_1: 1;

        then

         A16: r < z by A13, XXREAL_0: 2;

        z <= y by A15, XXREAL_1: 1;

        then z < s by A14, XXREAL_0: 2;

        hence thesis by A16, XXREAL_1: 4;

      end;

    end

    registration

      cluster REAL -> interval;

      coherence by XXREAL_1: 224;

    end

    registration

      cluster interval for non empty ext-real-membered set;

      existence

      proof

        take REAL ;

        thus thesis;

      end;

    end

    registration

      let A,B be interval ext-real-membered set;

      cluster (A /\ B) -> interval;

      coherence

      proof

        let r,s be ExtReal;

        assume that

         A1: r in (A /\ B) and

         A2: s in (A /\ B);

        

         A3: s in B by A2, XBOOLE_0:def 4;

        r in B by A1, XBOOLE_0:def 4;

        then

         A4: [.r, s.] c= B by A3, Def12;

        

         A5: s in A by A2, XBOOLE_0:def 4;

        r in A by A1, XBOOLE_0:def 4;

        then [.r, s.] c= A by A5, Def12;

        hence thesis by A4, XBOOLE_1: 19;

      end;

    end

    reserve A,B for ext-real-membered set;

    registration

      let r, s;

      cluster ].r, s.] -> non left_end;

      coherence

      proof

        assume ].r, s.] is left_end;

        then

         A1: ( inf ].r, s.]) in ].r, s.];

        then

         A2: ( inf ].r, s.]) <= s by XXREAL_1: 2;

        r < ( inf ].r, s.]) by A1, XXREAL_1: 2;

        then r < s by A2, XXREAL_0: 2;

        then r = ( inf ].r, s.]) by Th27;

        hence contradiction by A1, XXREAL_1: 2;

      end;

      cluster [.r, s.[ -> non right_end;

      coherence

      proof

        assume [.r, s.[ is right_end;

        then

         A3: ( sup [.r, s.[) in [.r, s.[;

        then

         A4: ( sup [.r, s.[) < s by XXREAL_1: 3;

        r <= ( sup [.r, s.[) by A3, XXREAL_1: 3;

        then r < s by A4, XXREAL_0: 2;

        then s = ( sup [.r, s.[) by Th31;

        hence contradiction by A3, XXREAL_1: 3;

      end;

      cluster ].r, s.[ -> non left_end non right_end;

      coherence

      proof

        thus ].r, s.[ is non left_end

        proof

          assume ].r, s.[ is left_end;

          then

           A5: ( inf ].r, s.[) in ].r, s.[;

          then

           A6: ( inf ].r, s.[) < s by XXREAL_1: 4;

          r < ( inf ].r, s.[) by A5, XXREAL_1: 4;

          then r < s by A6, XXREAL_0: 2;

          then r = ( inf ].r, s.[) by Th28;

          hence contradiction by A5, XXREAL_1: 4;

        end;

        assume ].r, s.[ is right_end;

        then

         A7: ( sup ].r, s.[) in ].r, s.[;

        then

         A8: ( sup ].r, s.[) < s by XXREAL_1: 4;

        r < ( sup ].r, s.[) by A7, XXREAL_1: 4;

        then r < s by A8, XXREAL_0: 2;

        then s = ( sup ].r, s.[) by Th32;

        hence contradiction by A7, XXREAL_1: 4;

      end;

    end

    registration

      cluster left_end right_end interval for ext-real-membered set;

      existence

      proof

        take [. 0 , 1.];

        thus thesis by Th33;

      end;

      cluster non left_end right_end interval for ext-real-membered set;

      existence

      proof

        take ]. 0 , 1.];

        thus thesis by Th35;

      end;

      cluster left_end non right_end interval for ext-real-membered set;

      existence

      proof

        take [. 0 , 1.[;

        thus thesis by Th34;

      end;

      cluster non left_end non right_end interval non empty for ext-real-membered set;

      existence

      proof

        take ]. 0 , 2.[;

        1 in ]. 0 , 2.[ by XXREAL_1: 4;

        hence thesis;

      end;

    end

    theorem :: XXREAL_2:75

    for A be left_end right_end interval ext-real-membered set holds A = [.( min A), ( max A).]

    proof

      let A be left_end right_end interval ext-real-membered set;

      let x;

      

       A1: ( max A) in A by Def6;

      thus x in A implies x in [.( min A), ( max A).]

      proof

        assume

         A2: x in A;

        then

         A3: x <= ( max A) by Th4;

        ( min A) <= x by A2, Th3;

        hence thesis by A3, XXREAL_1: 1;

      end;

      ( min A) in A by Def5;

      then [.( min A), ( max A).] c= A by A1, Def12;

      hence thesis;

    end;

    theorem :: XXREAL_2:76

    for A be non left_end right_end interval ext-real-membered set holds A = ].( inf A), ( max A).]

    proof

      let A be non left_end right_end interval ext-real-membered set;

      let x;

      defpred P[ ExtReal] means $1 in A & $1 < x;

      thus x in A implies x in ].( inf A), ( max A).]

      proof

        

         A1: not ( inf A) in A by Def5;

        assume

         A2: x in A;

        then

         A3: x <= ( max A) by Th4;

        ( inf A) <= x by A2, Th3;

        then ( inf A) < x by A2, A1, XXREAL_0: 1;

        hence thesis by A3, XXREAL_1: 2;

      end;

      assume

       A4: x in ].( inf A), ( max A).];

      per cases ;

        suppose not ex r st P[r];

        then x is LowerBound of A by Def2;

        then x <= ( inf A) by Def4;

        hence thesis by A4, XXREAL_1: 2;

      end;

        suppose ex r st P[r];

        then

        consider r such that

         A5: r in A and

         A6: r < x;

        x <= ( max A) by A4, XXREAL_1: 2;

        then

         A7: x in [.r, ( max A).] by A6, XXREAL_1: 1;

        ( max A) in A by Def6;

        then [.r, ( max A).] c= A by A5, Def12;

        hence thesis by A7;

      end;

    end;

    theorem :: XXREAL_2:77

    for A be left_end non right_end interval ext-real-membered set holds A = [.( min A), ( sup A).[

    proof

      let A be left_end non right_end interval ext-real-membered set;

      let x;

      defpred P[ ExtReal] means $1 in A & $1 > x;

      thus x in A implies x in [.( min A), ( sup A).[

      proof

        

         A1: not ( sup A) in A by Def6;

        assume

         A2: x in A;

        then

         A3: ( min A) <= x by Th3;

        x <= ( sup A) by A2, Th4;

        then x < ( sup A) by A2, A1, XXREAL_0: 1;

        hence thesis by A3, XXREAL_1: 3;

      end;

      assume

       A4: x in [.( min A), ( sup A).[;

      per cases ;

        suppose not ex r st P[r];

        then x is UpperBound of A by Def1;

        then ( sup A) <= x by Def3;

        hence thesis by A4, XXREAL_1: 3;

      end;

        suppose ex r st P[r];

        then

        consider r such that

         A5: r in A and

         A6: r > x;

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

        then

         A7: x in [.( inf A), r.] by A6, XXREAL_1: 1;

        ( min A) in A by Def5;

        then [.( inf A), r.] c= A by A5, Def12;

        hence thesis by A7;

      end;

    end;

    theorem :: XXREAL_2:78

    

     Th78: for A be non left_end non right_end non empty interval ext-real-membered set holds A = ].( inf A), ( sup A).[

    proof

      let A be non left_end non right_end non empty interval ext-real-membered set;

      let x;

      defpred P[ ExtReal] means $1 in A & $1 < x;

      defpred Q[ ExtReal] means $1 in A & $1 > x;

      thus x in A implies x in ].( inf A), ( sup A).[

      proof

        assume

         A1: x in A;

        then

         A2: x <> ( sup A) by Def6;

        x <= ( sup A) by A1, Th4;

        then

         A3: x < ( sup A) by A2, XXREAL_0: 1;

        

         A4: x <> ( inf A) by A1, Def5;

        ( inf A) <= x by A1, Th3;

        then ( inf A) < x by A4, XXREAL_0: 1;

        hence thesis by A3, XXREAL_1: 4;

      end;

      assume

       A5: x in ].( inf A), ( sup A).[;

      per cases ;

        suppose not ex r st P[r];

        then x is LowerBound of A by Def2;

        then x <= ( inf A) by Def4;

        hence thesis by A5, XXREAL_1: 4;

      end;

        suppose not ex r st Q[r];

        then x is UpperBound of A by Def1;

        then ( sup A) <= x by Def3;

        hence thesis by A5, XXREAL_1: 4;

      end;

        suppose that

         A6: ex r st P[r] and

         A7: ex r st Q[r];

        consider r such that

         A8: r in A and

         A9: r < x by A6;

        consider s such that

         A10: s in A and

         A11: s > x by A7;

        

         A12: x in [.r, s.] by A9, A11, XXREAL_1: 1;

         [.r, s.] c= A by A8, A10, Def12;

        hence thesis by A12;

      end;

    end;

    theorem :: XXREAL_2:79

    for A be non left_end non right_end interval ext-real-membered set holds ex r, s st r <= s & A = ].r, s.[

    proof

      let A be non left_end non right_end interval ext-real-membered set;

      per cases ;

        suppose

         A1: A is empty;

        take -infty , -infty ;

        thus thesis by A1;

      end;

        suppose

         A2: not A is empty;

        take ( inf A), ( sup A);

        thus ( inf A) <= ( sup A) by A2, Th40;

        thus thesis by A2, Th78;

      end;

    end;

    theorem :: XXREAL_2:80

    

     Th80: A is interval implies for x, y, r st x in A & y in A & x <= r & r <= y holds r in A

    proof

      assume

       A1: A is interval;

      let x, y, r such that

       A2: x in A and

       A3: y in A and

       A4: x <= r and

       A5: r <= y;

      

       A6: r in [.x, y.] by A4, A5, XXREAL_1: 1;

       [.x, y.] c= A by A1, A2, A3;

      hence thesis by A6;

    end;

    theorem :: XXREAL_2:81

    

     Th81: A is interval implies for x, r st x in A & x <= r & r < ( sup A) holds r in A

    proof

      assume

       A1: A is interval;

      let x, r such that

       A2: x in A and

       A3: x <= r and

       A4: r < ( sup A);

      per cases ;

        suppose ex y st y in A & r < y;

        hence thesis by A1, A2, A3, Th80;

      end;

        suppose not ex y st y in A & r < y;

        then r is UpperBound of A by Def1;

        hence thesis by A4, Def3;

      end;

    end;

    theorem :: XXREAL_2:82

    

     Th82: A is interval implies for x, r st x in A & ( inf A) < r & r <= x holds r in A

    proof

      assume

       A1: A is interval;

      let x, r such that

       A2: x in A and

       A3: ( inf A) < r and

       A4: r <= x;

      per cases ;

        suppose ex y st y in A & r > y;

        hence thesis by A1, A2, A4, Th80;

      end;

        suppose not ex y st y in A & r > y;

        then r is LowerBound of A by Def2;

        hence thesis by A3, Def4;

      end;

    end;

    theorem :: XXREAL_2:83

    A is interval implies for r st ( inf A) < r & r < ( sup A) holds r in A

    proof

      assume

       A1: A is interval;

      let r such that

       A2: ( inf A) < r and

       A3: r < ( sup A);

      per cases ;

        suppose ex y st y in A & r > y;

        hence thesis by A1, A3, Th81;

      end;

        suppose not ex y st y in A & r > y;

        then r is LowerBound of A by Def2;

        hence thesis by A2, Def4;

      end;

    end;

    theorem :: XXREAL_2:84

    

     Th84: (for x, y, r st x in A & y in A & x < r & r < y holds r in A) implies A is interval

    proof

      assume

       A1: for x, y, r st x in A & y in A & x < r & r < y holds r in A;

      let x, y such that

       A2: x in A and

       A3: y in A;

      let r;

      assume r in [.x, y.];

      then r in ( ].x, y.[ \/ {x, y}) by XXREAL_1: 29, XXREAL_1: 128;

      then

       A4: r in ].x, y.[ or r in {x, y} by XBOOLE_0:def 3;

      per cases by A4, TARSKI:def 2;

        suppose r = x;

        hence thesis by A2;

      end;

        suppose r = y;

        hence thesis by A3;

      end;

        suppose

         A5: r in ].x, y.[;

        then

         A6: r < y by XXREAL_1: 4;

        x < r by A5, XXREAL_1: 4;

        hence thesis by A1, A2, A3, A6;

      end;

    end;

    theorem :: XXREAL_2:85

    (for x, r st x in A & x < r & r < ( sup A) holds r in A) implies A is interval

    proof

      assume

       A1: for x, r st x in A & x < r & r < ( sup A) holds r in A;

      let x, y such that

       A2: x in A and

       A3: y in A;

      let r;

      assume r in [.x, y.];

      then r in ( ].x, y.[ \/ {x, y}) by XXREAL_1: 29, XXREAL_1: 128;

      then

       A4: r in ].x, y.[ or r in {x, y} by XBOOLE_0:def 3;

      per cases by A4, TARSKI:def 2;

        suppose r = x;

        hence thesis by A2;

      end;

        suppose r = y;

        hence thesis by A3;

      end;

        suppose

         A5: r in ].x, y.[;

        then

         A6: r < y by XXREAL_1: 4;

        y <= ( sup A) by A3, Th4;

        then

         A7: r < ( sup A) by A6, XXREAL_0: 2;

        x < r by A5, XXREAL_1: 4;

        hence thesis by A1, A2, A7;

      end;

    end;

    theorem :: XXREAL_2:86

    (for y, r st y in A & ( inf A) < r & r < y holds r in A) implies A is interval

    proof

      assume

       A1: for y, r st y in A & ( inf A) < r & r < y holds r in A;

      let x, y such that

       A2: x in A and

       A3: y in A;

      let r;

      assume r in [.x, y.];

      then r in ( ].x, y.[ \/ {x, y}) by XXREAL_1: 29, XXREAL_1: 128;

      then

       A4: r in ].x, y.[ or r in {x, y} by XBOOLE_0:def 3;

      per cases by A4, TARSKI:def 2;

        suppose r = x;

        hence thesis by A2;

      end;

        suppose r = y;

        hence thesis by A3;

      end;

        suppose

         A5: r in ].x, y.[;

        then

         A6: x < r by XXREAL_1: 4;

        ( inf A) <= x by A2, Th3;

        then

         A7: ( inf A) < r by A6, XXREAL_0: 2;

        r < y by A5, XXREAL_1: 4;

        hence thesis by A1, A3, A7;

      end;

    end;

    theorem :: XXREAL_2:87

    (for r st ( inf A) < r & r < ( sup A) holds r in A) implies A is interval

    proof

      assume

       A1: for r st ( inf A) < r & r < ( sup A) holds r in A;

      let x, y such that

       A2: x in A and

       A3: y in A;

      let r;

      assume r in [.x, y.];

      then r in ( ].x, y.[ \/ {x, y}) by XXREAL_1: 29, XXREAL_1: 128;

      then

       A4: r in ].x, y.[ or r in {x, y} by XBOOLE_0:def 3;

      per cases by A4, TARSKI:def 2;

        suppose r = x;

        hence thesis by A2;

      end;

        suppose r = y;

        hence thesis by A3;

      end;

        suppose

         A5: r in ].x, y.[;

        then

         A6: r < y by XXREAL_1: 4;

        y <= ( sup A) by A3, Th4;

        then

         A7: r < ( sup A) by A6, XXREAL_0: 2;

        

         A8: x < r by A5, XXREAL_1: 4;

        ( inf A) <= x by A2, Th3;

        then ( inf A) < r by A8, XXREAL_0: 2;

        hence thesis by A1, A7;

      end;

    end;

    theorem :: XXREAL_2:88

    

     Th88: (for x, y, r st x in A & y in A & x <= r & r <= y holds r in A) implies A is interval

    proof

      assume for x, y, r st x in A & y in A & x <= r & r <= y holds r in A;

      then for x, y, r st x in A & y in A & x < r & r < y holds r in A;

      hence thesis by Th84;

    end;

    theorem :: XXREAL_2:89

    A is interval & B is interval & A meets B implies (A \/ B) is interval

    proof

      assume that

       A1: A is interval and

       A2: B is interval;

      given z such that

       A3: z in A and

       A4: z in B;

      for x, y, r st x in (A \/ B) & y in (A \/ B) & x <= r & r <= y holds r in (A \/ B)

      proof

        let x, y, r such that

         A5: x in (A \/ B) and

         A6: y in (A \/ B) and

         A7: x <= r and

         A8: r <= y;

        per cases by A5, A6, XBOOLE_0:def 3;

          suppose x in A & y in A;

          then r in A by A1, A7, A8, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose that

           A9: x in A and

           A10: y in B;

          per cases ;

            suppose r <= z;

            then r in A by A1, A3, A7, A9, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose z <= r;

            then r in B by A2, A4, A8, A10, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

          suppose that

           A11: x in B and

           A12: y in A;

          per cases ;

            suppose z <= r;

            then r in A by A1, A3, A8, A12, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose r <= z;

            then r in B by A2, A4, A7, A11, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

          suppose x in B & y in B;

          then r in B by A2, A7, A8, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by Th88;

    end;

    theorem :: XXREAL_2:90

    A is interval & B is left_end interval & ( sup A) = ( inf B) implies (A \/ B) is interval

    proof

      assume that

       A1: A is interval and

       A2: B is left_end interval and

       A3: ( sup A) = ( inf B);

      set z = ( inf B);

      for x, y, r st x in (A \/ B) & y in (A \/ B) & x < r & r < y holds r in (A \/ B)

      proof

        let x, y, r such that

         A4: x in (A \/ B) and

         A5: y in (A \/ B) and

         A6: x < r and

         A7: r < y;

        per cases by A4, A5, XBOOLE_0:def 3;

          suppose x in A & y in A;

          then r in A by A1, A6, A7, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose that

           A8: x in A and

           A9: y in B;

          per cases ;

            suppose r < z;

            then r in A by A1, A3, A6, A8, Th81;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose z <= r;

            then r in B by A2, A7, A9, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

          suppose that

           A10: x in B and

           A11: y in A;

          per cases ;

            suppose

             A12: z < r;

            y <= z by A3, A11, Th4;

            hence thesis by A7, A12, XXREAL_0: 2;

          end;

            suppose r <= z;

            then r in B by A2, A6, A10, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

          suppose x in B & y in B;

          then r in B by A2, A6, A7, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by Th84;

    end;

    theorem :: XXREAL_2:91

    A is right_end interval & B is interval & ( sup A) = ( inf B) implies (A \/ B) is interval

    proof

      assume that

       A1: A is right_end interval and

       A2: B is interval and

       A3: ( sup A) = ( inf B);

      set z = ( inf B);

      

       A4: z in A by A1, A3;

      for x, y, r st x in (A \/ B) & y in (A \/ B) & x < r & r < y holds r in (A \/ B)

      proof

        let x, y, r such that

         A5: x in (A \/ B) and

         A6: y in (A \/ B) and

         A7: x < r and

         A8: r < y;

        per cases by A5, A6, XBOOLE_0:def 3;

          suppose x in A & y in A;

          then r in A by A1, A7, A8, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose that

           A9: x in A and

           A10: y in B;

          per cases ;

            suppose r <= z;

            then r in A by A1, A4, A7, A9, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose z < r;

            then r in B by A2, A8, A10, Th82;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

          suppose that

           A11: x in B and

           A12: y in A;

          per cases ;

            suppose z <= r;

            then r in A by A1, A4, A8, A12, Th80;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose

             A13: r < z;

            z <= x by A11, Th3;

            hence thesis by A7, A13, XXREAL_0: 2;

          end;

        end;

          suppose x in B & y in B;

          then r in B by A2, A7, A8, Th80;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by Th84;

    end;

    registration

      cluster left_end -> non empty for ext-real-membered set;

      coherence ;

      cluster right_end -> non empty for ext-real-membered set;

      coherence ;

    end

    theorem :: XXREAL_2:92

    for A be non empty Subset of ExtREAL st for r be Element of ExtREAL st r in A holds r <= -infty holds A = { -infty }

    proof

      let A be non empty Subset of ExtREAL such that

       A1: for r be Element of ExtREAL st r in A holds r <= -infty ;

      assume A <> { -infty };

      then ex a be Element of A st a <> -infty by SETFAM_1: 49;

      hence contradiction by A1, XXREAL_0: 6;

    end;

    theorem :: XXREAL_2:93

    for A be non empty Subset of ExtREAL st for r be Element of ExtREAL st r in A holds +infty <= r holds A = { +infty }

    proof

      let A be non empty Subset of ExtREAL such that

       A1: for r be Element of ExtREAL st r in A holds +infty <= r;

      assume A <> { +infty };

      then ex a be Element of A st a <> +infty by SETFAM_1: 49;

      hence contradiction by A1, XXREAL_0: 4;

    end;

    theorem :: XXREAL_2:94

    

     Th94: for A be non empty Subset of ExtREAL , r be ExtReal st r < ( sup A) holds ex s be Element of ExtREAL st s in A & r < s

    proof

      let A be non empty Subset of ExtREAL , r be ExtReal;

      assume

       A1: r < ( sup A);

      assume

       A2: for s be Element of ExtREAL st s in A holds not r < s;

      r is UpperBound of A

      proof

        let x be ExtReal;

        assume x in A;

        hence thesis by A2;

      end;

      hence contradiction by A1, Def3;

    end;

    theorem :: XXREAL_2:95

    

     Th95: for A be non empty Subset of ExtREAL , r be Element of ExtREAL st ( inf A) < r holds ex s be Element of ExtREAL st s in A & s < r

    proof

      let A be non empty Subset of ExtREAL , r be Element of ExtREAL ;

      assume

       A1: ( inf A) < r;

      assume

       A2: for s be Element of ExtREAL st s in A holds not s < r;

      r is LowerBound of A

      proof

        let x be ExtReal;

        thus thesis by A2;

      end;

      hence contradiction by A1, Def4;

    end;

    theorem :: XXREAL_2:96

    for A,B be non empty Subset of ExtREAL st for r,s be ExtReal st r in A & s in B holds r <= s holds ( sup A) <= ( inf B)

    proof

      let A,B be non empty Subset of ExtREAL ;

      assume

       A1: for r,s be ExtReal st r in A & s in B holds r <= s;

      assume not ( sup A) <= ( inf B);

      then

      consider s1 be Element of ExtREAL such that

       A2: s1 in A and

       A3: ( inf B) < s1 by Th94;

      ex s2 be Element of ExtREAL st s2 in B & s2 < s1 by A3, Th95;

      hence contradiction by A1, A2;

    end;