xxreal_0.miz



    begin

    

     Lm0: not REAL in REAL ;

    reserve x for set;

    definition

      let x be object;

      :: XXREAL_0:def1

      attr x is ext-real means

      : Def1: x in ExtREAL ;

    end

    registration

      cluster ext-real for object;

      existence

      proof

        take 0 ;

         NAT c= ExtREAL by NUMBERS: 19, NUMBERS: 31;

        hence 0 in ExtREAL ;

      end;

      cluster ext-real for number;

      existence

      proof

        take 0 ;

         NAT c= ExtREAL by NUMBERS: 19, NUMBERS: 31;

        hence 0 in ExtREAL ;

      end;

      cluster -> ext-real for Element of ExtREAL ;

      coherence ;

    end

    definition

      mode ExtReal is ext-real Number;

    end

    registration

      sethood of ExtReal

      proof

        take ExtREAL ;

        thus thesis by Def1;

      end;

    end

    definition

      :: XXREAL_0:def2

      func +infty -> object equals REAL ;

      coherence ;

      :: XXREAL_0:def3

      func -infty -> object equals [ 0 , REAL ];

      coherence ;

    end

    definition

      :: original: ExtREAL

      redefine

      :: XXREAL_0:def4

      func ExtREAL equals ( REAL \/ { +infty , -infty });

      compatibility ;

    end

    registration

      cluster +infty -> ext-real;

      coherence

      proof

         +infty in { REAL , [ 0 , REAL ]} by TARSKI:def 2;

        then +infty in ExtREAL by XBOOLE_0:def 3;

        hence thesis;

      end;

      cluster -infty -> ext-real;

      coherence

      proof

         -infty in { REAL , [ 0 , REAL ]} by TARSKI:def 2;

        then -infty in ExtREAL by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    definition

      let x,y be ExtReal;

      :: XXREAL_0:def5

      pred x <= y means

      : Def5: ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & x9 <=' y9 if x in REAL+ & y in REAL+ ,

ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & y = [ 0 , y9] & y9 <=' x9 if x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :]

      otherwise y in REAL+ & x in [: { 0 }, REAL+ :] or x = -infty or y = +infty ;

      consistency by ARYTM_0: 5, XBOOLE_0: 3;

      reflexivity

      proof

        let x be ExtReal such that

         A1: not ((x in REAL+ & x in REAL+ implies ex x9,y9 be Element of REAL+ st x = x9 & x = y9 & x9 <=' y9) & (x in [: { 0 }, REAL+ :] & x in [: { 0 }, REAL+ :] implies ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & x = [ 0 , y9] & y9 <=' x9) & ( not (x in REAL+ & x in REAL+ ) & not (x in [: { 0 }, REAL+ :] & x in [: { 0 }, REAL+ :]) implies x in REAL+ & x in [: { 0 }, REAL+ :] or x = -infty or x = +infty ));

        x in ExtREAL by Def1;

        then

         A2: x in (( REAL+ \/ [: { 0 }, REAL+ :]) \ { [ 0 , 0 ]}) or x in { +infty , -infty } by XBOOLE_0:def 3;

        per cases by A1;

          suppose that

           A3: x in REAL+ and

           A4: not ex x9,y9 be Element of REAL+ st x = x9 & x = y9 & x9 <=' y9;

          reconsider x9 = x as Element of REAL+ by A3;

           not x9 <=' x9 by A4;

          hence thesis;

        end;

          suppose that

           A5: x in [: { 0 }, REAL+ :] and

           A6: not ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & x = [ 0 , y9] & y9 <=' x9;

          consider z,x9 be object such that

           A7: z in { 0 } and

           A8: x9 in REAL+ and

           A9: x = [z, x9] by A5, ZFMISC_1: 84;

          reconsider x9 as Element of REAL+ by A8;

          x = [ 0 , x9] by A7, A9, TARSKI:def 1;

          then not x9 <=' x9 by A6;

          hence thesis;

        end;

          suppose not ( not x in REAL+ & not x in [: { 0 }, REAL+ :] implies x in REAL+ & x in [: { 0 }, REAL+ :] or x = -infty or x = +infty );

          hence thesis by A2, TARSKI:def 2, XBOOLE_0:def 3;

        end;

      end;

      connectedness

      proof

        let x,y be ExtReal such that

         A10: not ((x in REAL+ & y in REAL+ implies ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & x9 <=' y9) & (x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :] implies ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & y = [ 0 , y9] & y9 <=' x9) & ( not (x in REAL+ & y in REAL+ ) & not (x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :]) implies y in REAL+ & x in [: { 0 }, REAL+ :] or x = -infty or y = +infty ));

        x in ExtREAL by Def1;

        then

         A11: x in (( REAL+ \/ [: { 0 }, REAL+ :]) \ { [ 0 , 0 ]}) or x in { +infty , -infty } by XBOOLE_0:def 3;

        y in ExtREAL by Def1;

        then

         A12: y in (( REAL+ \/ [: { 0 }, REAL+ :]) \ { [ 0 , 0 ]}) or y in { +infty , -infty } by XBOOLE_0:def 3;

        per cases by A10;

          suppose that

           A13: x in REAL+ & y in REAL+ and

           A14: not ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & x9 <=' y9;

          hereby

            assume y in REAL+ & x in REAL+ ;

            then

            reconsider x9 = x, y9 = y as Element of REAL+ ;

            take y9, x9;

            thus y = y9 & x = x9;

            thus y9 <=' x9 by A14;

          end;

          thus thesis by A13, ARYTM_0: 5, XBOOLE_0: 3;

        end;

          suppose that

           A15: x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :] and

           A16: not ex x9,y9 be Element of REAL+ st x = [ 0 , x9] & y = [ 0 , y9] & y9 <=' x9;

          now

            assume y in [: { 0 }, REAL+ :];

            then

            consider z,y9 be object such that

             A17: z in { 0 } and

             A18: y9 in REAL+ and

             A19: y = [z, y9] by ZFMISC_1: 84;

            

             A20: z = 0 by A17, TARSKI:def 1;

            assume x in [: { 0 }, REAL+ :];

            then

            consider z,x9 be object such that

             A21: z in { 0 } and

             A22: x9 in REAL+ and

             A23: x = [z, x9] by ZFMISC_1: 84;

            reconsider x9, y9 as Element of REAL+ by A18, A22;

            take y9, x9;

            thus y = [ 0 , y9] & x = [ 0 , x9] by A17, A19, A21, A23, TARSKI:def 1;

            z = 0 by A21, TARSKI:def 1;

            hence x9 <=' y9 by A16, A19, A20, A23;

          end;

          hence thesis by A15, ARYTM_0: 5, XBOOLE_0: 3;

        end;

          suppose not ( not (x in REAL+ & y in REAL+ ) & not (x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :]) implies y in REAL+ & x in [: { 0 }, REAL+ :] or x = -infty or y = +infty );

          hence thesis by A11, A12, TARSKI:def 2, XBOOLE_0:def 3;

        end;

      end;

    end

    reserve a,b,c,d for ExtReal;

    notation

      let a,b be ExtReal;

      synonym b >= a for a <= b;

      antonym b < a for a <= b;

      antonym a > b for a <= b;

    end

    

     Lm1: 0 in REAL by NUMBERS: 19;

    

     Lm2: +infty <> [ 0 , 0 ]

    proof

      assume +infty = [ 0 , 0 ];

      

      then +infty = { { 0 }, { 0 }} by ENUMSET1: 29

      .= { { 0 }} by ENUMSET1: 29;

      hence contradiction by TARSKI:def 1, Lm1;

    end;

    

     Lm3: not +infty in REAL+ by ARYTM_0: 1, ORDINAL1: 5;

    

     Lm4: not -infty in REAL+

    proof

       { 0 , REAL } in { { 0 , REAL }, { 0 }} & REAL in { 0 , REAL } by TARSKI:def 2;

      hence thesis by ARYTM_0: 1, XREGULAR: 7;

    end;

    

     Lm5: not +infty in [: { 0 }, REAL+ :]

    proof

      assume +infty in [: { 0 }, REAL+ :];

      then +infty in ( REAL+ \/ [: { 0 }, REAL+ :]) by XBOOLE_0:def 3;

      then +infty in REAL by Lm2, ZFMISC_1: 56;

      hence contradiction by Lm0;

    end;

    

     Lm6: not -infty in [: { 0 }, REAL+ :]

    proof

      assume -infty in [: { 0 }, REAL+ :];

      then REAL in REAL+ by ZFMISC_1: 87;

      hence contradiction by ARYTM_0: 1, ORDINAL1: 5;

    end;

    

     Lm7: -infty < +infty

    proof

       -infty <> +infty by TARSKI:def 2, Lm1;

      hence thesis by Def5, Lm4, Lm6;

    end;

    theorem :: XXREAL_0:1

    

     Th1: for a,b be ExtReal holds a <= b & b <= a implies a = b

    proof

      let a,b be ExtReal;

      assume that

       A1: a <= b and

       A2: b <= a;

      per cases ;

        suppose a in REAL+ & b in REAL+ ;

        then (ex a9,b9 be Element of REAL+ st a = a9 & b = b9 & a9 <=' b9) & ex b99,a99 be Element of REAL+ st b = b99 & a = a99 & b99 <=' a99 by A1, A2, Def5;

        hence thesis by ARYTM_1: 4;

      end;

        suppose

         A3: a in REAL+ & b in [: { 0 }, REAL+ :];

        then ( not b in REAL+ ) & not a in [: { 0 }, REAL+ :] by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A1, A3, Def5, Lm4, Lm5;

      end;

        suppose

         A4: b in REAL+ & a in [: { 0 }, REAL+ :];

        then ( not a in REAL+ ) & not b in [: { 0 }, REAL+ :] by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A2, A4, Def5, Lm4, Lm5;

      end;

        suppose that

         A5: a in [: { 0 }, REAL+ :] & b in [: { 0 }, REAL+ :];

        consider a9,b9 be Element of REAL+ such that

         A6: a = [ 0 , a9] & b = [ 0 , b9] and

         A7: b9 <=' a9 by A1, A5, Def5;

        consider b99,a99 be Element of REAL+ such that

         A8: b = [ 0 , b99] & a = [ 0 , a99] and

         A9: a99 <=' b99 by A2, A5, Def5;

        a9 = a99 & b9 = b99 by A6, A8, XTUPLE_0: 1;

        hence thesis by A7, A8, A9, ARYTM_1: 4;

      end;

        suppose (a = -infty or a = +infty ) & (b = -infty or b = +infty );

        hence thesis by A1, A2, Lm7;

      end;

        suppose that

         A10: ( not (a in REAL+ & b in REAL+ )) & not (a in [: { 0 }, REAL+ :] & b in [: { 0 }, REAL+ :]) and

         A11: not (b in REAL+ & a in [: { 0 }, REAL+ :]) and

         A12: not (a in REAL+ & b in [: { 0 }, REAL+ :]);

        a = -infty or b = +infty by A1, A10, A11, Def5;

        hence thesis by A2, A10, A12, Def5, Lm7;

      end;

    end;

    

     Lm8: for a be ExtReal holds -infty >= a implies a = -infty

    proof

      let a be ExtReal;

      a >= -infty by Def5, Lm4, Lm6;

      hence thesis by Th1;

    end;

    

     Lm9: for a be ExtReal holds +infty <= a implies a = +infty

    proof

      let a be ExtReal;

      a <= +infty by Def5, Lm3, Lm5;

      hence thesis by Th1;

    end;

    theorem :: XXREAL_0:2

    

     Th2: for a,b,c be ExtReal holds a <= b & b <= c implies a <= c

    proof

      let a,b,c be ExtReal;

      assume that

       A1: a <= b and

       A2: b <= c;

      per cases ;

        suppose that

         A3: a in REAL+ and

         A4: b in REAL+ and

         A5: c in REAL+ ;

        consider b99,c9 be Element of REAL+ such that

         A6: b = b99 and

         A7: c = c9 and

         A8: b99 <=' c9 by A2, A4, A5, Def5;

        consider a9,b9 be Element of REAL+ such that

         A9: a = a9 and

         A10: b = b9 & a9 <=' b9 by A1, A3, A4, Def5;

        a9 <=' c9 by A10, A6, A8, ARYTM_1: 3;

        hence thesis by A5, A9, A7, Def5;

      end;

        suppose

         A11: a in REAL+ & b in [: { 0 }, REAL+ :];

        then ( not (a in REAL+ & b in REAL+ )) & not (a in [: { 0 }, REAL+ :] & b in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A1, A11, Def5, Lm4, Lm5;

      end;

        suppose

         A12: b in REAL+ & c in [: { 0 }, REAL+ :];

        then ( not (c in REAL+ & b in REAL+ )) & not (c in [: { 0 }, REAL+ :] & b in [: { 0 }, REAL+ :]) by ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A2, A12, Def5, Lm4, Lm5;

      end;

        suppose that

         A13: a in [: { 0 }, REAL+ :] & c in REAL+ ;

        ( not (a in REAL+ & c in REAL+ )) & not (a in [: { 0 }, REAL+ :] & c in [: { 0 }, REAL+ :]) by A13, ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A13, Def5;

      end;

        suppose that

         A14: a in [: { 0 }, REAL+ :] and

         A15: b in [: { 0 }, REAL+ :] and

         A16: c in [: { 0 }, REAL+ :];

        consider b99,c9 be Element of REAL+ such that

         A17: b = [ 0 , b99] and

         A18: c = [ 0 , c9] and

         A19: c9 <=' b99 by A2, A15, A16, Def5;

        consider a9,b9 be Element of REAL+ such that

         A20: a = [ 0 , a9] and

         A21: b = [ 0 , b9] and

         A22: b9 <=' a9 by A1, A14, A15, Def5;

        b9 = b99 by A21, A17, XTUPLE_0: 1;

        then c9 <=' a9 by A22, A19, ARYTM_1: 3;

        hence thesis by A14, A16, A20, A18, Def5;

      end;

        suppose that

         A23: not (a in REAL+ & b in REAL+ & c in REAL+ ) and

         A24: not (a in REAL+ & b in [: { 0 }, REAL+ :]) and

         A25: not (b in REAL+ & c in [: { 0 }, REAL+ :]) and

         A26: not (a in [: { 0 }, REAL+ :] & c in REAL+ ) and

         A27: not (a in [: { 0 }, REAL+ :] & b in [: { 0 }, REAL+ :] & c in [: { 0 }, REAL+ :]);

        

         A28: b = +infty implies c = +infty by A2, Lm9;

        

         A29: b = -infty implies a = -infty by A1, Lm8;

        a = -infty or b = +infty or b = -infty or c = +infty by A1, A2, A23, A25, A26, A27, Def5;

        hence thesis by A1, A2, A23, A24, A25, A27, A28, A29, Def5;

      end;

    end;

    theorem :: XXREAL_0:3

    a <= +infty by Def5, Lm3, Lm5;

    theorem :: XXREAL_0:4

     +infty <= a implies a = +infty by Lm9;

    theorem :: XXREAL_0:5

    a >= -infty by Def5, Lm4, Lm6;

    theorem :: XXREAL_0:6

     -infty >= a implies a = -infty by Lm8;

    theorem :: XXREAL_0:7

     -infty < +infty by Lm7;

    theorem :: XXREAL_0:8

     not +infty in REAL by Lm0;

    

     Lm10: a in REAL or a = +infty or a = -infty

    proof

      a in ExtREAL by Def1;

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

      hence thesis by TARSKI:def 2;

    end;

    theorem :: XXREAL_0:9

    

     Th9: a in REAL implies +infty > a

    proof

      assume a in REAL ;

      then

       A1: a <> +infty by Lm0;

       +infty >= a by Def5, Lm3, Lm5;

      hence thesis by A1, Th1;

    end;

    theorem :: XXREAL_0:10

    

     Th10: a in REAL & b >= a implies b in REAL or b = +infty

    proof

      assume that

       A1: a in REAL and

       A2: b >= a;

      assume

       A3: not b in REAL ;

      b = -infty implies a = -infty by A2, Lm8;

      hence thesis by A1, A3, Lm10;

    end;

    theorem :: XXREAL_0:11

    

     Th11: not -infty in REAL

    proof

      

       A1: { 0 , REAL } in { { 0 , REAL }, { 0 }} & REAL in { 0 , REAL } by TARSKI:def 2;

      assume -infty in REAL ;

      hence contradiction by A1, XREGULAR: 7;

    end;

    theorem :: XXREAL_0:12

    

     Th12: a in REAL implies -infty < a

    proof

       -infty <= a by Def5, Lm4, Lm6;

      hence thesis by Th1, Th11;

    end;

    theorem :: XXREAL_0:13

    

     Th13: a in REAL & b <= a implies b in REAL or b = -infty

    proof

      assume that

       A1: a in REAL and

       A2: b <= a;

      assume

       A3: not b in REAL ;

      b = +infty implies a = +infty by A2, Lm9;

      hence thesis by A1, A3, Lm10;

    end;

    theorem :: XXREAL_0:14

    a in REAL or a = +infty or a = -infty by Lm10;

    begin

    registration

      cluster natural -> ext-real for object;

      coherence by NUMBERS: 19, XBOOLE_0:def 3;

    end

    definition

      let a be ExtReal;

      :: XXREAL_0:def6

      attr a is positive means a > 0 ;

      :: XXREAL_0:def7

      attr a is negative means a < 0 ;

      ::$Canceled

    end

    registration

      cluster positive -> non negative non zero for ExtReal;

      coherence ;

      cluster non negative non zero -> positive for ExtReal;

      coherence by Th1;

      cluster negative -> non positive non zero for ExtReal;

      coherence ;

      cluster non positive non zero -> negative for ExtReal;

      coherence ;

      cluster zero -> non negative non positive for ExtReal;

      coherence ;

      cluster non negative non positive -> zero for ExtReal;

      coherence ;

    end

    registration

      cluster +infty -> positive;

      coherence by Th9, Lm1;

      cluster -infty -> negative;

      coherence by Th12, Lm1;

    end

    registration

      cluster positive for ExtReal;

      existence

      proof

        take +infty ;

        thus thesis;

      end;

      cluster negative for ExtReal;

      existence

      proof

        take -infty ;

        thus thesis;

      end;

      cluster zero for ExtReal;

      existence

      proof

        reconsider z = 0 as ExtReal;

        take z;

        thus z = 0 ;

      end;

    end

    begin

    definition

      let a,b be ExtReal;

      :: XXREAL_0:def9

      func min (a,b) -> ExtReal equals

      : Def8: a if a <= b

      otherwise b;

      correctness ;

      commutativity by Th1;

      idempotence ;

      :: XXREAL_0:def10

      func max (a,b) -> ExtReal equals

      : Def9: a if b <= a

      otherwise b;

      correctness ;

      commutativity by Th1;

      idempotence ;

    end

    theorem :: XXREAL_0:15

    ( min (a,b)) = a or ( min (a,b)) = b by Def8;

    theorem :: XXREAL_0:16

    ( max (a,b)) = a or ( max (a,b)) = b by Def9;

    registration

      let a, b;

      cluster ( min (a,b)) -> ext-real;

      coherence ;

      cluster ( max (a,b)) -> ext-real;

      coherence ;

    end

    theorem :: XXREAL_0:17

    

     Th17: ( min (a,b)) <= a

    proof

      a <= b or not a <= b;

      hence thesis by Def8;

    end;

    theorem :: XXREAL_0:18

    

     Th18: a <= b & c <= d implies ( min (a,c)) <= ( min (b,d))

    proof

      assume that

       A1: a <= b and

       A2: c <= d;

      ( min (a,c)) <= c by Th17;

      then

       A3: ( min (a,c)) <= d by A2, Th2;

      ( min (a,c)) <= a by Th17;

      then ( min (a,c)) <= b by A1, Th2;

      hence thesis by A3, Def8;

    end;

    theorem :: XXREAL_0:19

    a < b & c < d implies ( min (a,c)) < ( min (b,d))

    proof

      assume that

       A1: a < b and

       A2: c < d;

      ( min (a,c)) <= c by Th17;

      then

       A3: ( min (a,c)) < d by A2, Th2;

      ( min (a,c)) <= a by Th17;

      then ( min (a,c)) < b by A1, Th2;

      hence thesis by A3, Def8;

    end;

    theorem :: XXREAL_0:20

    a <= b & a <= c implies a <= ( min (b,c)) by Def8;

    theorem :: XXREAL_0:21

    a < b & a < c implies a < ( min (b,c)) by Def8;

    theorem :: XXREAL_0:22

    a <= ( min (b,c)) implies a <= b

    proof

      ( min (b,c)) <= b by Th17;

      hence thesis by Th2;

    end;

    theorem :: XXREAL_0:23

    a < ( min (b,c)) implies a < b

    proof

      ( min (b,c)) <= b by Th17;

      hence thesis by Th2;

    end;

    theorem :: XXREAL_0:24

    c <= a & c <= b & (for d st d <= a & d <= b holds d <= c) implies c = ( min (a,b))

    proof

      assume that

       A1: c <= a & c <= b and

       A2: for d st d <= a & d <= b holds d <= c;

      ( min (a,b)) <= a & ( min (a,b)) <= b by Th17;

      then

       A3: ( min (a,b)) <= c by A2;

      c <= ( min (a,b)) by A1, Def8;

      hence thesis by A3, Th1;

    end;

    theorem :: XXREAL_0:25

    

     Th25: a <= ( max (a,b))

    proof

      a <= b or not a <= b;

      hence thesis by Def9;

    end;

    theorem :: XXREAL_0:26

    

     Th26: a <= b & c <= d implies ( max (a,c)) <= ( max (b,d))

    proof

      assume that

       A1: a <= b and

       A2: c <= d;

      d <= ( max (b,d)) by Th25;

      then

       A3: c <= ( max (b,d)) by A2, Th2;

      b <= ( max (b,d)) by Th25;

      then a <= ( max (b,d)) by A1, Th2;

      hence thesis by A3, Def9;

    end;

    theorem :: XXREAL_0:27

    a < b & c < d implies ( max (a,c)) < ( max (b,d))

    proof

      assume that

       A1: a < b and

       A2: c < d;

      d <= ( max (b,d)) by Th25;

      then

       A3: c < ( max (b,d)) by A2, Th2;

      b <= ( max (b,d)) by Th25;

      then a < ( max (b,d)) by A1, Th2;

      hence thesis by A3, Def9;

    end;

    theorem :: XXREAL_0:28

    b <= a & c <= a implies ( max (b,c)) <= a by Def9;

    theorem :: XXREAL_0:29

    b < a & c < a implies ( max (b,c)) < a by Def9;

    theorem :: XXREAL_0:30

    ( max (b,c)) <= a implies b <= a

    proof

      b <= ( max (b,c)) by Th25;

      hence thesis by Th2;

    end;

    theorem :: XXREAL_0:31

    ( max (b,c)) < a implies b < a

    proof

      b <= ( max (b,c)) by Th25;

      hence thesis by Th2;

    end;

    theorem :: XXREAL_0:32

    a <= c & b <= c & (for d st a <= d & b <= d holds c <= d) implies c = ( max (a,b))

    proof

      assume that

       A1: a <= c & b <= c and

       A2: for d st a <= d & b <= d holds c <= d;

      a <= ( max (a,b)) & b <= ( max (a,b)) by Th25;

      then

       A3: c <= ( max (a,b)) by A2;

      ( max (a,b)) <= c by A1, Def9;

      hence thesis by A3, Th1;

    end;

    theorem :: XXREAL_0:33

    ( min (( min (a,b)),c)) = ( min (a,( min (b,c))))

    proof

      per cases by Th2;

        suppose a <= b & a <= c;

        then ( min (a,b)) = a & ( min (a,c)) = a by Def8;

        hence thesis by Def8;

      end;

        suppose b <= a & b <= c;

        then ( min (a,b)) = b & ( min (b,c)) = b by Def8;

        hence thesis;

      end;

        suppose c <= b & c <= a;

        then ( min (b,c)) = c & ( min (a,c)) = c by Def8;

        hence thesis by Def8;

      end;

    end;

    theorem :: XXREAL_0:34

    ( max (( max (a,b)),c)) = ( max (a,( max (b,c))))

    proof

      per cases by Th2;

        suppose

         A1: a <= b & a <= c;

        

         A2: ( max (b,c)) = b or ( max (b,c)) = c by Def9;

        ( max (a,b)) = b by A1, Def9;

        hence thesis by A1, A2, Def9;

      end;

        suppose

         A3: b <= a & b <= c;

        then ( max (a,b)) = a by Def9;

        hence thesis by A3, Def9;

      end;

        suppose

         A4: c <= b & c <= a;

        

         A5: ( max (a,b)) = b or ( max (a,b)) = a by Def9;

        ( max (b,c)) = b by A4, Def9;

        hence thesis by A4, A5, Def9;

      end;

    end;

    theorem :: XXREAL_0:35

    ( min (( max (a,b)),b)) = b by Th25, Def8;

    theorem :: XXREAL_0:36

    ( max (( min (a,b)),b)) = b by Th17, Def9;

    theorem :: XXREAL_0:37

    

     Th37: a <= c implies ( max (a,( min (b,c)))) = ( min (( max (a,b)),c))

    proof

      assume

       A1: a <= c;

      per cases ;

        suppose

         A2: a <= b;

        then a <= ( min (b,c)) by A1, Def8;

        

        hence ( max (a,( min (b,c)))) = ( min (b,c)) by Def9

        .= ( min (( max (a,b)),c)) by A2, Def9;

      end;

        suppose

         A3: b <= a;

        then b <= c by A1, Th2;

        

        hence ( max (a,( min (b,c)))) = ( max (a,b)) by Def8

        .= a by A3, Def9

        .= ( min (a,c)) by A1, Def8

        .= ( min (( max (a,b)),c)) by A3, Def9;

      end;

    end;

    theorem :: XXREAL_0:38

    ( min (a,( max (b,c)))) = ( max (( min (a,b)),( min (a,c))))

    proof

      per cases ;

        suppose

         A1: b <= c;

        then

         A2: ( min (a,b)) <= ( min (a,c)) by Th18;

        

        thus ( min (a,( max (b,c)))) = ( min (a,c)) by A1, Def9

        .= ( max (( min (a,b)),( min (a,c)))) by A2, Def9;

      end;

        suppose

         A3: c <= b;

        then

         A4: ( min (a,c)) <= ( min (a,b)) by Th18;

        

        thus ( min (a,( max (b,c)))) = ( min (a,b)) by A3, Def9

        .= ( max (( min (a,b)),( min (a,c)))) by A4, Def9;

      end;

    end;

    theorem :: XXREAL_0:39

    ( max (a,( min (b,c)))) = ( min (( max (a,b)),( max (a,c))))

    proof

      per cases ;

        suppose

         A1: b <= c;

        then

         A2: ( max (a,b)) <= ( max (a,c)) by Th26;

        

        thus ( max (a,( min (b,c)))) = ( max (a,b)) by A1, Def8

        .= ( min (( max (a,b)),( max (a,c)))) by A2, Def8;

      end;

        suppose

         A3: c <= b;

        then

         A4: ( max (a,c)) <= ( max (a,b)) by Th26;

        

        thus ( max (a,( min (b,c)))) = ( max (a,c)) by A3, Def8

        .= ( min (( max (a,b)),( max (a,c)))) by A4, Def8;

      end;

    end;

    theorem :: XXREAL_0:40

    ( max (( max (( min (a,b)),( min (b,c)))),( min (c,a)))) = ( min (( min (( max (a,b)),( max (b,c)))),( max (c,a))))

    proof

      per cases ;

        suppose

         A1: a <= c;

        then

         A2: ( max (a,b)) <= ( max (b,c)) by Th26;

        ( min (a,b)) <= ( min (b,c)) by A1, Th18;

        

        hence ( max (( max (( min (a,b)),( min (b,c)))),( min (c,a)))) = ( max (( min (b,c)),( min (c,a)))) by Def9

        .= ( max (( min (b,c)),a)) by A1, Def8

        .= ( min (( max (a,b)),c)) by A1, Th37

        .= ( min (( max (a,b)),( max (c,a)))) by A1, Def9

        .= ( min (( min (( max (a,b)),( max (b,c)))),( max (c,a)))) by A2, Def8;

      end;

        suppose

         A3: c <= a;

        then

         A4: ( max (a,b)) >= ( max (b,c)) by Th26;

        ( min (a,b)) >= ( min (b,c)) by A3, Th18;

        

        hence ( max (( max (( min (a,b)),( min (b,c)))),( min (c,a)))) = ( max (( min (a,b)),( min (c,a)))) by Def9

        .= ( max (( min (a,b)),c)) by A3, Def8

        .= ( min (( max (c,b)),a)) by A3, Th37

        .= ( min (( max (c,b)),( max (c,a)))) by A3, Def9

        .= ( min (( min (( max (a,b)),( max (b,c)))),( max (c,a)))) by A4, Def8;

      end;

    end;

    theorem :: XXREAL_0:41

    ( max (a, +infty )) = +infty

    proof

      a <= +infty by Def5, Lm3, Lm5;

      hence thesis by Def9;

    end;

    theorem :: XXREAL_0:42

    ( min (a, +infty )) = a

    proof

      a <= +infty by Def5, Lm3, Lm5;

      hence thesis by Def8;

    end;

    theorem :: XXREAL_0:43

    ( max (a, -infty )) = a

    proof

      a >= -infty by Def5, Lm4, Lm6;

      hence thesis by Def9;

    end;

    theorem :: XXREAL_0:44

    ( min (a, -infty )) = -infty

    proof

      a >= -infty by Def5, Lm4, Lm6;

      hence thesis by Def8;

    end;

    begin

    theorem :: XXREAL_0:45

    a in REAL & c in REAL & a <= b & b <= c implies b in REAL

    proof

      assume that

       A1: a in REAL and

       A2: c in REAL and

       A3: a <= b and

       A4: b <= c;

      b in REAL or b = +infty by A1, A3, Th10;

      hence thesis by A2, A4, Th13;

    end;

    theorem :: XXREAL_0:46

    a in REAL & a <= b & b < c implies b in REAL

    proof

      assume that

       A1: a in REAL & a <= b and

       A2: b < c;

      b in REAL or b = +infty by A1, Th10;

      hence thesis by A2, Lm9;

    end;

    theorem :: XXREAL_0:47

    c in REAL & a < b & b <= c implies b in REAL

    proof

      assume that

       A1: c in REAL and

       A2: a < b and

       A3: b <= c;

      b in REAL or b = -infty by A1, A3, Th13;

      hence thesis by A2, Lm8;

    end;

    theorem :: XXREAL_0:48

    a < b & b < c implies b in REAL

    proof

      assume

       A1: a < b & b < c;

      b in REAL or b = +infty or b = -infty by Lm10;

      hence thesis by A1, Lm8, Lm9;

    end;

    definition

      let x,y be ExtReal, a,b be object;

      :: XXREAL_0:def11

      func IFGT (x,y,a,b) -> object equals

      : Def10: a if x > y

      otherwise b;

      correctness ;

    end

    registration

      let x,y be ExtReal, a,b be natural Number;

      cluster ( IFGT (x,y,a,b)) -> natural;

      coherence by Def10;

    end

    theorem :: XXREAL_0:49

    ( max (a,b)) <= a implies ( max (a,b)) = a

    proof

      assume ( max (a,b)) <= a;

      then ( max (a,b)) < a or ( max (a,b)) = a by Th1;

      hence thesis by Th25;

    end;

    theorem :: XXREAL_0:50

    a <= ( min (a,b)) implies ( min (a,b)) = a

    proof

      assume ( min (a,b)) >= a;

      then ( min (a,b)) > a or ( min (a,b)) = a by Th1;

      hence thesis by Th17;

    end;

    registration

      let x be ExtReal;

      reduce ( In (x, ExtREAL )) to x;

      reducibility by Def1, SUBSET_1:def 8;

    end