The abstract of the Mizar article:

Basic Properties of Real Numbers --- Requirements

by

Library Committee

Received February 27, 2003

MML identifier: REAL

[ Mizar article, MML identifier index ]

environ

 vocabulary XREAL_0, ARYTM, ARYTM_3, ASYMPT_0, ZF_LANG, ARYTM_2, BOOLE;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0;
 constructors ARYTM_0, XREAL_0, ARYTM_2, XCMPLX_0, XBOOLE_0;
 clusters XREAL_0, ARYTM_2, NUMBERS, XCMPLX_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;


begin

:: This file contains statements which are obvious for Mizar checker if
:: "requirements REAL" is included in the environment description of an article.
:: They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Note that the checker needs also "requirements BOOLE" to accept
:: the statements with attribute 'zero'.

 reserve x, y, z for real number;

theorem :: REAL:1
   x <= y & x is positive implies y is positive;

theorem :: REAL:2
   x <= y & y is negative implies x is negative;

theorem :: REAL:3
   x <= y & x is non negative implies y is non negative;

theorem :: REAL:4
   x <= y & y is non positive implies x is non positive;

theorem :: REAL:5
   x <= y & y is non zero & x is non negative implies y is positive;

theorem :: REAL:6
   x <= y & x is non zero & y is non positive implies x is negative;

theorem :: REAL:7
   not x <= y & x is non positive implies y is negative;

theorem :: REAL:8
   not x <= y & y is non negative implies x is positive;