:: Basic Properties of Real Numbers :: by Krzysztof Hryniewiecki :: :: Received January 8, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XREAL_0, SUBSET_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, REAL_1, ARYTM_2, CARD_1, TARSKI, ZFMISC_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0; constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ARYTM_2, ARYTM_1; registrations XREAL_0, ORDINAL1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; begin registration cluster -> real for Element of REAL; end; registration cluster positive for Real; end; registration cluster positive for Element of REAL; end; definition let x be Element of REAL; redefine func -x -> Element of REAL; redefine func x" -> Element of REAL; end; definition let x, y be Element of REAL; redefine func x+y -> Element of REAL; redefine func x*y -> Element of REAL; redefine func x-y -> Element of REAL; redefine func x/y -> Element of REAL; end; :: 2011.05.09, A.T reserve s,t for Element of RAT+; theorem :: REAL_1:1 REAL+ = { r where r is Real: 0 <= r};