:: 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 & 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;