:: Basic Properties of Real Numbers
:: by Krzysztof Hryniewiecki
::
:: Copyright (c) 1990-2021 Association of Mizar Users

registration
cluster -> real for Element of REAL ;
coherence
for b1 being Element of REAL holds b1 is real
;
end;

registration
existence
ex b1 being Real st b1 is positive
proof end;
end;

registration
existence
ex b1 being Element of REAL st b1 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;