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