environ
vocabularies HIDDEN, NUMBERS, NAT_1, SUBSET_1, REAL_1, CARD_1, XXREAL_0, NEWTON, ARYTM_3, CARD_3, PROB_1, XBOOLE_0, LIMFUNC1, PRE_TOPC, FUNCT_1, ZFMISC_1, STRUCT_0, FINSEQ_1, RELAT_1, ARYTM_1, TARSKI, CONNSP_2, RCOMP_1, TOPS_1, SETFAM_1, CARD_5, URYSOHN1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1, FUNCT_1, ENUMSET1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, NAT_1, PROB_1, LIMFUNC1, NEWTON, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, XXREAL_0;
definitions TARSKI, CONNSP_2, XBOOLE_0, PRE_TOPC;
theorems TARSKI, SUBSET_1, FUNCT_1, NAT_1, FINSEQ_1, ZFMISC_1, PRE_TOPC, TOPS_1, ENUMSET1, COMPTS_1, NEWTON, CONNSP_2, XBOOLE_0, XBOOLE_1, SCHEME1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, XREAL_0;
schemes SUBSET_1, NAT_1, FINSEQ_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, NEWTON, NAT_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, REAL_1, NAT_1, MEMBERED, XXREAL_1, PROB_1, LIMFUNC1, NEWTON, TOPS_1, COMPTS_1, CONNSP_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, PRE_TOPC;
:: Some increasing family of sets in normal space
::