real.miz

    begin

    reserve x,y,z for Real;



     Lm1: x <= y & y <= x implies x = y

    proof

      assume that

       A1: x <= y and

       A2: y <= x;



       A3: x in REAL & y in REAL by XREAL_0:def 1;

      per cases by A3, NUMBERS:def 1, XBOOLE_0:def 3;

        suppose x in REAL+ & y in REAL+ ;

        then (ex x9,y9 be Element of REAL+ st x = x9 & y = y9 & x9 <=' y9) & ex y99,x99 be Element of REAL+ st y = y99 & x = x99 & y99 <=' x99 by A1, A2, XXREAL_0:def 5;

        hence thesis by ARYTM_1: 4;

      end;

        suppose

         A4: x in REAL+ & y in [: { 0 }, REAL+ :];

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

        hence thesis by A1, A4, XXREAL_0:def 5;

      end;

        suppose

         A5: y in REAL+ & x in [: { 0 }, REAL+ :];

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

        hence thesis by A2, A5, XXREAL_0:def 5;

      end;

        suppose that

         A6: x in [: { 0 }, REAL+ :] & y in [: { 0 }, REAL+ :];

        consider x9,y9 be Element of REAL+ such that

         A7: x = [ 0 , x9] & y = [ 0 , y9] and

         A8: y9 <=' x9 by A1, A6, XXREAL_0:def 5;

        consider y99,x99 be Element of REAL+ such that

         A9: y = [ 0 , y99] & x = [ 0 , x99] and

         A10: x99 <=' y99 by A2, A6, XXREAL_0:def 5;

        x9 = x99 & y9 = y99 by A7, A9, XTUPLE_0: 1;

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

      end;

    end;



     Lm2: x <= y & y <= z implies x <= z

    proof

      assume that

       A1: x <= y and

       A2: y <= z;



       A3: x in REAL & y in REAL by XREAL_0:def 1;



       A4: z in REAL by XREAL_0:def 1;

      per cases by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;

        suppose that

         A5: x in REAL+ and

         A6: y in REAL+ and

         A7: z in REAL+ ;

        consider y99,z9 be Element of REAL+ such that

         A8: y = y99 and

         A9: z = z9 and

         A10: y99 <=' z9 by A2, A6, A7, XXREAL_0:def 5;

        consider x9,y9 be Element of REAL+ such that

         A11: x = x9 and

         A12: y = y9 & x9 <=' y9 by A1, A5, A6, XXREAL_0:def 5;

        x9 <=' z9 by A12, A8, A10, ARYTM_1: 3;

        hence thesis by A11, A9, XXREAL_0:def 5;

      end;

        suppose

         A13: x in REAL+ & y in [: { 0 }, REAL+ :];

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

        hence thesis by A1, A13, XXREAL_0:def 5;

      end;

        suppose

         A14: y in REAL+ & z in [: { 0 }, REAL+ :];

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

        hence thesis by A2, A14, XXREAL_0:def 5;

      end;

        suppose that

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

         A16: z in REAL+ ;

        ( not (x in REAL+ & z in REAL+ )) & not (x in [: { 0 }, REAL+ :] & z in [: { 0 }, REAL+ :]) by A15, A16, ARYTM_0: 5, XBOOLE_0: 3;

        hence thesis by A16, XXREAL_0:def 5;

      end;

        suppose that

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

         A18: y in [: { 0 }, REAL+ :] and

         A19: z in [: { 0 }, REAL+ :];

        consider y99,z9 be Element of REAL+ such that

         A20: y = [ 0 , y99] and

         A21: z = [ 0 , z9] and

         A22: z9 <=' y99 by A2, A18, A19, XXREAL_0:def 5;

        consider x9,y9 be Element of REAL+ such that

         A23: x = [ 0 , x9] and

         A24: y = [ 0 , y9] and

         A25: y9 <=' x9 by A1, A17, A18, XXREAL_0:def 5;

        y9 = y99 by A24, A20, XTUPLE_0: 1;

        then z9 <=' x9 by A25, A22, ARYTM_1: 3;

        hence thesis by A17, A19, A23, A21, XXREAL_0:def 5;

      end;

    end;

    theorem :: REAL:1

    x <= y & x is positive implies y is positive

    proof

      assume that

       A1: x <= y and

       A2: x is positive;

      x > 0 by A2, XXREAL_0:def 6;

      then y > 0 by A1, Lm2;

      hence thesis by XXREAL_0:def 6;

    end;

    theorem :: REAL:2

    x <= y & y is negative implies x is negative

    proof

      assume that

       A1: x <= y and

       A2: y is negative;

      y < 0 by A2, XXREAL_0:def 7;

      then x < 0 by A1, Lm2;

      hence thesis by XXREAL_0:def 7;

    end;

    theorem :: REAL:3

    x <= y & x is non negative implies y is non negative

    proof

      assume that

       A1: x <= y and

       A2: x is non negative and

       A3: y is negative;

      y < 0 by A3, XXREAL_0:def 7;

      then x < 0 by A1, Lm2;

      hence thesis by A2, XXREAL_0:def 7;

    end;

    theorem :: REAL:4

    x <= y & y is non positive implies x is non positive

    proof

      assume that

       A1: x <= y and

       A2: y is non positive and

       A3: x is positive;

      x > 0 by A3, XXREAL_0:def 6;

      then y > 0 by A1, Lm2;

      hence thesis by A2, XXREAL_0:def 6;

    end;

    theorem :: REAL:5

    x <= y & y is non zero & x is non negative implies y is positive

    proof

      assume that

       A1: x <= y and

       A2: y is non zero and

       A3: x is non negative and

       A4: y is non positive;

      y <= 0 by A4, XXREAL_0:def 6;

      then

       A5: y < 0 by A2, Lm1;

      x >= 0 by A3, XXREAL_0:def 7;

      hence thesis by A1, A5, Lm2;

    end;

    theorem :: REAL:6

    x <= y & x is non zero & y is non positive implies x is negative

    proof

      assume that

       A1: x <= y and

       A2: x is non zero and

       A3: y is non positive and

       A4: x is non negative;

      x >= 0 by A4, XXREAL_0:def 7;

      then

       A5: x > 0 by A2, Lm1;

      y <= 0 by A3, XXREAL_0:def 6;

      hence thesis by A1, A5, Lm2;

    end;

    theorem :: REAL:7

     not x <= y & x is non positive implies y is negative

    proof

      assume that

       A1: x > y and

       A2: x is non positive & y is non negative;

      x <= 0 & y >= 0 by A2, XXREAL_0:def 6, XXREAL_0:def 7;

      hence thesis by A1, Lm2;

    end;

    theorem :: REAL:8

     not x <= y & y is non negative implies x is positive

    proof

      assume that

       A1: x > y and

       A2: y is non negative & x is non positive;

      x <= 0 & y >= 0 by A2, XXREAL_0:def 6, XXREAL_0:def 7;

      hence thesis by A1, Lm2;

    end;