:: REAL semantic presentation

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