:: Basic Properties of Real Numbers
:: by Krzysztof Hryniewiecki
::
:: Received January 8, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

registration

cluster -> real for Element of REAL ;

coherence
for b₁ being Element of REAL holds b₁ is real ;

end;

registration

cluster V19() ext-real positive real for object ;

existence
ex b₁ being Real st b₁ is positive

proof end;

end;

registration

cluster V19() ext-real positive real for Element of REAL ;

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