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


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;