:: Basic Properties of Real Numbers
:: by Krzysztof Hryniewiecki
::
:: Received January 8, 1989
:: Copyright (c) 1990-2015 Association of Mizar Users
registration
cluster
->
real
for
Element
of
REAL
;
coherence
for
b
1
being
Element
of
REAL
holds
b
1
is
real
;
end;
registration
cluster
V19
()
ext-real
positive
real
for
object
;
existence
ex
b
1
being
Real
st
b
1
is
positive
proof
end;
end;
registration
cluster
V19
()
ext-real
positive
real
for
Element
of
REAL
;
existence
ex
b
1
being
Element
of
REAL
st
b
1
is
positive
proof
end;
end;
definition
let
x
be
Element
of
REAL
;
:: original:
-
redefine
func
-
x
->
Element
of
REAL
;
coherence
-
x
is
Element
of
REAL
by
XREAL_0:def 1
;
:: original:
"
redefine
func
x
"
->
Element
of
REAL
;
coherence
x
"
is
Element
of
REAL
by
XREAL_0:def 1
;
end;
definition
let
x
,
y
be
Element
of
REAL
;
:: original:
+
redefine
func
x
+
y
->
Element
of
REAL
;
coherence
x
+
y
is
Element
of
REAL
by
XREAL_0:def 1
;
:: original:
*
redefine
func
x
*
y
->
Element
of
REAL
;
coherence
x
*
y
is
Element
of
REAL
by
XREAL_0:def 1
;
:: original:
-
redefine
func
x
-
y
->
Element
of
REAL
;
coherence
x
-
y
is
Element
of
REAL
by
XREAL_0:def 1
;
:: original:
/
redefine
func
x
/
y
->
Element
of
REAL
;
coherence
x
/
y
is
Element
of
REAL
by
XREAL_0:def 1
;
end;
theorem
:: REAL_1:1
REAL+
=
{
r
where
r
is
Real
:
0
<=
r
}
proof
end;