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

environ

vocabularies HIDDEN, NUMBERS, XREAL_0, SUBSET_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, REAL_1, ARYTM_2, CARD_1, TARSKI, ZFMISC_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems XREAL_0, XBOOLE_0, ARYTM_0, ARYTM_1, ARYTM_2, XXREAL_0, NUMBERS;
schemes ;
registrations XREAL_0, ORDINAL1;
constructors HIDDEN, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ARYTM_2, ARYTM_1;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities ORDINAL1;
expansions TARSKI;


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

registration
cluster V19() ext-real positive real for object ;
existence
ex b1 being Real st b1 is positive
proof end;
end;

registration
cluster V19() ext-real positive real for Element of REAL ;
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;