environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, FUNCT_2, SUBSET_1, RELAT_1, TARSKI, PRE_TOPC, CONNSP_1, RELAT_2, XXREAL_0, EUCLID, XXREAL_2, STRUCT_0, REAL_1, METRIC_1, PCOMPS_1, WEIERSTR, CARD_1, SEQ_4, RCOMP_1, JORDAN2C, COMPLEX1, SQUARE_1, MCART_1, ARYTM_1, ARYTM_3, RLTOPSP1, JGRAPH_2, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_2, SEQ_4, DOMAIN_1, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, METRIC_1, METRIC_6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2;
definitions XBOOLE_0, TARSKI, FUNCT_2, XXREAL_2;
theorems XBOOLE_1, XBOOLE_0, SPRECT_1, JORDAN2C, SUBSET_1, GOBOARD9, TSEP_1, CONNSP_1, PRE_TOPC, ZFMISC_1, EUCLID, WEIERSTR, TOPREAL3, TBSP_1, SQUARE_1, ABSVALUE, FUNCT_1, METRIC_1, FUNCT_2, JGRAPH_2, RELAT_1, TOPMETR, PCOMPS_1, TARSKI, XREAL_0, TOPRNS_1, XCMPLX_1, COMPLEX1, SEQ_4, XREAL_1, XXREAL_0, TOPS_2, TOPREAL6, COMPTS_1, RLVECT_1;
schemes ;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, MONOID_0, EUCLID, TOPMETR, JORDAN2C, BORSUK_3, TOPREAL6, JGRAPH_2, RELSET_1, JORDAN1, VALUED_0, JORDAN5A, SQUARE_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_4, CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2, FUNCSDOM, BINOP_2, CONVEX1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities EUCLID, SQUARE_1, SUBSET_1, STRUCT_0, RLTOPSP1, RLVECT_1;
expansions XBOOLE_0, TARSKI, FUNCT_2;