environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, ARYTM_3, REAL_1, XXREAL_0, COMPLEX1, ARYTM_1, CARD_1, FUNCT_1, MCART_1, ZFMISC_1, PRE_TOPC, RCOMP_1, TARSKI, STRUCT_0, SETFAM_1, SEQ_1, RELAT_1, VALUED_0, SEQ_2, ORDINAL2, RELAT_2, PSCOMP_1, LIMFUNC1, CONNSP_1, METRIC_1, SEQ_4, XXREAL_2, TOPMETR, NAT_1, VALUED_1, EUCLID, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, FUNCT_1, COMPLEX1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, XXREAL_1, XXREAL_2, NAT_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, MEASURE5, MEASURE6, PSCOMP_1, VALUED_0, METRIC_1, TBSP_1, TOPMETR, LIMFUNC1, CONNSP_1, RLTOPSP1, EUCLID, RECDEF_1, RCOMP_1;
definitions TARSKI, RCOMP_1, XBOOLE_0, XXREAL_2;
theorems ZFMISC_1, TARSKI, SUBSET_1, FUNCT_2, FUNCT_1, RCOMP_1, SEQ_4, SEQM_3, ABSVALUE, PSCOMP_1, GOBOARD7, BORSUK_1, TOPMETR, JORDAN6, UNIFORM1, RELAT_1, SEQ_2, TOPREAL6, TSP_1, SEQ_1, CONNSP_1, XREAL_0, TSEP_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, JORDAN2C, PRE_TOPC, TOPREAL3, METRIC_6, XXREAL_0, XXREAL_1, XXREAL_2, VALUED_0, MEASURE6, MEASURE5, JORDAN5A, XTUPLE_0, ORDINAL1;
schemes FUNCT_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, MEASURE6, JORDAN2C, BORSUK_3, INTEGRA1, VALUED_1, FUNCT_2, XXREAL_2, VALUED_0, FCONT_3, PSCOMP_1, MEASURE5, JORDAN5A, XTUPLE_0, NAT_1;
constructors HIDDEN, REAL_1, COMPLEX1, PROB_1, LIMFUNC1, BINARITH, CONNSP_1, COMPTS_1, TBSP_1, TOPMETR, MEASURE6, INTEGRA1, RECDEF_1, SEQ_4, PSCOMP_1, COMSEQ_2, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities RCOMP_1, XBOOLE_0, SUBSET_1, PROB_1, LIMFUNC1;
expansions TARSKI, XBOOLE_0, XXREAL_2;