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

begin

registration

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

proof end;

end;

definition

mode Real is Element of REAL ;

end;

registration

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