environ
vocabularies HIDDEN, NUMBERS, GRAPH_1, FINSEQ_1, STRUCT_0, TREES_2, SUBSET_1, REAL_1, GRAPH_4, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0, CARD_1, ZFMISC_1, MCART_1, ARYTM_1, NAT_1, RELAT_1, TARSKI, PARTFUN1, GLIB_000, FINSET_1, EUCLID, RLTOPSP1, TOPREAL1, GOBOARD5, PRE_TOPC, SUPINF_2, GOBOARD1, GOBOARD4, COMPLEX1, METRIC_1, SQUARE_1, RVSUM_1, CARD_3, PCOMPS_1, RCOMP_1, WEIERSTR, INT_1, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, MEASURE5, PSCOMP_1, XXREAL_2, JGRAPH_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, FINSET_1, NAT_1, NAT_D, SEQM_3, GRAPH_1, STRUCT_0, GRAPH_2, GRAPH_4, TOPREAL1, GOBOARD5, PRE_TOPC, GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, TOPS_2, METRIC_1, TBSP_1, RCOMP_1, SQUARE_1, PSCOMP_1, RVSUM_1, RLVECT_1, RLTOPSP1, EUCLID, FUNCT_3;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, FUNCT_1, FINSEQ_1, NAT_1, ZFMISC_1, SPPOL_1, FINSEQ_4, GRAPH_1, FUNCT_3, RELAT_1, GRAPH_4, FINSEQ_3, TOPREAL1, GOBOARD1, GOBOARD5, GOBOARD4, TOPREAL3, SQUARE_1, EUCLID, JORDAN7, UNIFORM1, WEIERSTR, JORDAN5A, TOPS_2, PRE_TOPC, TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1, BORSUK_1, ABSVALUE, METRIC_1, RVSUM_1, FUNCT_2, JORDAN6, XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_0, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, XXREAL_1, XXREAL_2, SEQM_3, XREAL_0, VALUED_1, RLTOPSP1, CARD_1, XTUPLE_0, RLVECT_4, RLVECT_1;
schemes FINSEQ_1;
registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, GRAPH_2, GRAPH_4, FINSET_1, VALUED_0, FUNCT_2, CARD_1, XXREAL_2, TOPREAL1, RELSET_1, SQUARE_1, ORDINAL1;
constructors HIDDEN, FUNCT_3, REAL_1, SQUARE_1, NAT_D, RCOMP_1, BINARITH, TOPS_2, COMPTS_1, TBSP_1, MONOID_0, GOBOARD1, GOBOARD4, GOBOARD5, PSCOMP_1, GRAPH_2, WEIERSTR, GRAPH_4, XXREAL_2, FUNCSDOM;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, EUCLID, SQUARE_1, BINOP_1, STRUCT_0, ALGSTR_0, RLTOPSP1;
expansions TARSKI, XBOOLE_0, FUNCT_1;