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