:: 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 b1 being Element of REAL holds b1 is real ;
end;

definition
mode Real is Element of REAL ;
end;

registration
clusterV11() ext-real positive real for Element of REAL ;
existence
 ex b1 being Real st b1 is positive
proofend;
end;

definition
let x be Real;
:: original:-
redefine func - x ->  Real;
coherence
 - x is Real by XREAL_0:def_1;
:: original:"
redefine funcx "  ->  Real;
coherence
 x " is Real by XREAL_0:def_1;
end;

definition
let x be real number ;
let y be Real;
:: original:+
redefine funcx + y ->  Real;
coherence
 x + y is Real by XREAL_0:def_1;
:: original:*
redefine funcx * y ->  Real;
coherence
 x * y is Real by XREAL_0:def_1;
:: original:-
redefine funcx - y ->  Real;
coherence
 x - y is Real by XREAL_0:def_1;
:: original:/
redefine funcx / 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 funcx + y ->  Real;
coherence
 x + y is Real by XREAL_0:def_1;
:: original:*
redefine funcx * y ->  Real;
coherence
 x * y is Real by XREAL_0:def_1;
:: original:-
redefine funcx - y ->  Real;
coherence
 x - y is Real by XREAL_0:def_1;
:: original:/
redefine funcx / 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  }
proofend;