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, ORDINAL4, VALUED_1, COMPLEX1, PRE_TOPC, ORDINAL2, PSCOMP_1, STRUCT_0, TOPMETR, REAL_1, RCOMP_1, PARTFUN3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, SQUARE_1, FUNCT_1, RELSET_1, PSCOMP_1, VALUED_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCOP_1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPALG_2, PARTFUN3;
definitions PSCOMP_1;
theorems FUNCT_2, RELAT_1, FUNCT_1, ZFMISC_1, JGRAPH_2, XBOOLE_1, XBOOLE_0, FUNCOP_1, TOPMETR, RFUNCT_1, XCMPLX_0, JGRAPH_3, JGRAPH_4, VALUED_1, PARTFUN3, JORDAN5A, XREAL_0;
schemes ;
registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, TOPMETR, VALUED_0, FUNCT_2, PSCOMP_1, PARTFUN3, RELAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, FUNCOP_1, TOPALG_2, PSCOMP_1, PARTFUN3, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities STRUCT_0, ORDINAL1;
expansions ;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;