:: REAL semantic presentation

begin

theorem :: REAL:1
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & x : ( ( real ) ( ext-real real ) number ) is positive holds
y : ( ( real ) ( ext-real real ) number ) is positive ;

theorem :: REAL:2
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & y : ( ( real ) ( ext-real real ) number ) is negative holds
x : ( ( real ) ( ext-real real ) number ) is negative ;

theorem :: REAL:3
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not x : ( ( real ) ( ext-real real ) number ) is negative holds
not y : ( ( real ) ( ext-real real ) number ) is negative ;

theorem :: REAL:4
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not y : ( ( real ) ( ext-real real ) number ) is positive holds
not x : ( ( real ) ( ext-real real ) number ) is positive ;

theorem :: REAL:5
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not y : ( ( real ) ( ext-real real ) number ) is zero & not x : ( ( real ) ( ext-real real ) number ) is negative holds
y : ( ( real ) ( ext-real real ) number ) is positive ;

theorem :: REAL:6
for x, y being ( ( real ) ( ext-real real ) number ) st x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not x : ( ( real ) ( ext-real real ) number ) is zero & not y : ( ( real ) ( ext-real real ) number ) is positive holds
x : ( ( real ) ( ext-real real ) number ) is negative ;

theorem :: REAL:7
for x, y being ( ( real ) ( ext-real real ) number ) st not x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not x : ( ( real ) ( ext-real real ) number ) is positive holds
y : ( ( real ) ( ext-real real ) number ) is negative ;

theorem :: REAL:8
for x, y being ( ( real ) ( ext-real real ) number ) st not x : ( ( real ) ( ext-real real ) number ) <= y : ( ( real ) ( ext-real real ) number ) & not y : ( ( real ) ( ext-real real ) number ) is negative holds
x : ( ( real ) ( ext-real real ) number ) is positive ;