real_1.miz
begin
registration
cluster ->
real for
Element of
REAL ;
coherence ;
end
registration
cluster
positive for
Real;
existence
proof
take (1
/ 1);
thus thesis;
end;
end
registration
cluster
positive for
Element of
REAL ;
existence
proof
reconsider j = 1 as
Element of
REAL by
NUMBERS: 19;
take j;
thus thesis;
end;
end
definition
let x be
Element of
REAL ;
:: original:
-
redefine
func
- x ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
:: original:
"
redefine
func x
" ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
end
definition
let x,y be
Element of
REAL ;
:: original:
+
redefine
func x
+ y ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
:: original:
*
redefine
func x
* y ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
:: original:
-
redefine
func x
- y ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
:: original:
/
redefine
func x
/ y ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
end
reserve s,t for
Element of
RAT+ ;
theorem ::
REAL_1:1
REAL+
= { r where r be
Real :
0
<= r }
proof
set RP = { r where r be
Real :
0
<= r };
thus
REAL+
c= RP
proof
let e be
object;
assume
A1: e
in
REAL+ ;
then
reconsider r = e as
Real by
ARYTM_0: 1;
reconsider o =
0 , s = r as
Element of
REAL+ by
A1,
ARYTM_2: 20;
o
<=' s by
ARYTM_1: 6;
then
0
<= r by
ARYTM_2: 20,
XXREAL_0:def 5;
hence e
in RP;
end;
let e be
object;
assume e
in RP;
then
A2: ex r be
Real st e
= r &
0
<= r;
not
0
in
[:
{
0 },
REAL+ :] by
ARYTM_0: 5,
ARYTM_2: 20,
XBOOLE_0: 3;
hence e
in
REAL+ by
A2,
XXREAL_0:def 5;
end;