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

begin

Lm1: for x, y being real number st x <= y & y <= x holds
x = y

proof end;

Lm2: for x, y, z being real number st x <= y & y <= z holds
x <= z

proof end;

theorem :: REAL:1

for x, y being real number st x <= y & x is positive holds
y is positive

proof end;

theorem :: REAL:2

for x, y being real number st x <= y & y is negative holds
x is negative

proof end;

theorem :: REAL:3

for x, y being real number st x <= y & not x is negative holds
not y is negative

proof end;

theorem :: REAL:4

for x, y being real number st x <= y & not y is positive holds
not x is positive

proof end;

theorem :: REAL:5

for x, y being real number 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 number 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 number st not x <= y & not x is positive holds
y is negative

proof end;

theorem :: REAL:8

for x, y being real number st not x <= y & not y is negative holds
x is positive

proof end;