environ
vocabularies HIDDEN, NUMBERS, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, FUNCT_1, TARSKI, XBOOLE_0, FUNCOP_1, ARYTM_1, SUBSET_1, VALUED_0, ORDINAL4, PARTFUN1, VALUED_1, XCMPLX_0, PRALG_1, COMPLEX1, MEMBERED, PARTFUN3, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, MEMBERED, SQUARE_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MEASURE6, VALUED_0, VALUED_1, RFUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCOP_1;
definitions RELAT_1, VALUED_0;
theorems TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, FUNCOP_1, RFUNCT_1, SQUARE_1, XCMPLX_0, XREAL_1, COMPLEX1, VALUED_0, VALUED_1, RELSET_1, XREAL_0, ORDINAL1;
schemes FUNCT_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, RFUNCT_1, MEASURE6, FUNCOP_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities VALUED_1, ORDINAL1;
expansions RELAT_1;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;