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


begin

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

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

theorem :: REAL:1
for x, y being real number st x <= y &amp; x is positive holds
y is positive
proofend;

theorem :: REAL:2
for x, y being real number st x <= y &amp; y is negative holds
x is negative
proofend;

theorem :: REAL:3
for x, y being real number st x <= y &amp; not x is negative holds
not y is negative
proofend;

theorem :: REAL:4
for x, y being real number st x <= y &amp; not y is positive holds
not x is positive
proofend;

theorem :: REAL:5
for x, y being real number st x <= y &amp; not y is zero &amp; not x is negative holds
y is positive
proofend;

theorem :: REAL:6
for x, y being real number st x <= y &amp; not x is zero &amp; not y is positive holds
x is negative
proofend;

theorem :: REAL:7
for x, y being real number st not x <= y &amp; not x is positive holds
y is negative
proofend;

theorem :: REAL:8
for x, y being real number st not x <= y &amp; not y is negative holds
x is positive
proofend;