:: Basic Properties of Real Numbers - Requirements
:: by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users

environ

vocabularies HIDDEN, XXREAL_0, NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XCMPLX_0, REAL_1;
notations HIDDEN, TARSKI, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0;
definitions ;
theorems XBOOLE_0, ARYTM_0, ARYTM_1, XREAL_0, NUMBERS, XXREAL_0, XTUPLE_0;
schemes ;
registrations ARYTM_2, XREAL_0, ORDINAL1;
constructors HIDDEN, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities ORDINAL1;
expansions ;


Lm1: for x, y being Real st x <= y & y <= x holds
x = y
proof end;

Lm2: for x, y, z being Real st x <= y & y <= z holds
x <= z
proof end;

theorem :: REAL:1
for x, y being Real st x <= y & x is positive holds
y is positive
proof end;

theorem :: REAL:2
for x, y being Real st x <= y & y is negative holds
x is negative
proof end;

theorem :: REAL:3
for x, y being Real st x <= y & not x is negative holds
not y is negative
proof end;

theorem :: REAL:4
for x, y being Real st x <= y & not y is positive holds
not x is positive
proof end;

theorem :: REAL:5
for x, y being Real st x <= y & not y is zero & not x is negative holds
y is positive
proof end;

theorem :: REAL:6
for x, y being Real st x <= y & not x is zero & not y is positive holds
x is negative
proof end;

theorem :: REAL:7
for x, y being Real st not x <= y & not x is positive holds
y is negative
proof end;

theorem :: REAL:8
for x, y being Real st not x <= y & not y is negative holds
x is positive
proof end;