Journal of Formalized Mathematics
Reqmnts, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

Basic Properties of Real Numbers --- Requirements

by
Library Committee

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;
```