:: 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
cluster V11() ext-real positive real for Element of REAL ;
existence
ex b1 being Real st b1 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;