environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2, ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1, COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, VALUED_1, ZFMISC_1, XXREAL_2, FCONT_1, NORMSP_1, STRUCT_0, PRE_TOPC, FINSEQ_1, CARD_3, FINSET_1, MEMBERED, BORSUK_1, REAL_NS1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, REAL_1, MEMBERED, COMPLEX1, XXREAL_2, FINSEQ_1, SEQ_1, SEQ_2, RCOMP_1, FCONT_1, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, EUCLID, NFCONT_1, REAL_NS1, PDIFF_1, INTEGR15, VALUED_2, NFCONT_3, VFUNCT_1;
definitions FCONT_1, NFCONT_3, TARSKI;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, PARTFUN1, XREAL_0, PARTFUN2, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, XXREAL_2, VALUED_0, FCONT_1, NFCONT_1, NORMSP_0, FINSEQ_1, FINSET_1, VFUNCT_1, REAL_NS1, SUBSET_1, PDIFF_8, NFCONT_3, VALUED_2;
schemes FUNCT_1, FINSEQ_1, PARTFUN2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, VALUED_0, FUNCT_2, XXREAL_2, FUNCT_1, STRUCT_0, EUCLID, FINSEQ_1, REAL_NS1, NFCONT_3, VALUED_2;
constructors HIDDEN, REAL_1, COMPLEX1, SEQ_2, SEQ_4, RELSET_1, FCONT_1, NFCONT_1, VFUNCT_1, BINOP_2, PDIFF_1, INTEGR15, NFCONT_3, VALUED_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE;
equalities VALUED_1, INTEGR15;
expansions FCONT_1, NFCONT_3, TARSKI;