environ
vocabularies HIDDEN, NUMBERS, SUPINF_1, PROB_1, XBOOLE_0, SETFAM_1, FUNCT_1, SUBSET_1, TARSKI, RELAT_1, CARD_1, ARYTM_3, NAT_1, XXREAL_0, ZFMISC_1, MEASURE1, SUPINF_2, VALUED_0, FUNCOP_1, XREAL_0, ARYTM_1, MEASURE3, MEASURE4;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0, XCMPLX_0, FUNCOP_1, REAL_1, NAT_1, SETFAM_1, PROB_1, SUPINF_1, SUPINF_2, MEASURE1, MEASURE3;
definitions TARSKI, MEASURE3, XBOOLE_0;
theorems TARSKI, ENUMSET1, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SUPINF_2, MEASURE1, MEASURE2, MEASURE3, XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_1, ORDINAL1, VALUED_0, XXREAL_3, FUNCOP_1;
schemes NAT_1, FUNCT_2, XFAMILY;
registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEASURE1, VALUED_0;
constructors HIDDEN, ENUMSET1, PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE3, SUPINF_1, FUNCOP_1, RELSET_1, XREAL_0;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, SUPINF_2;
expansions TARSKI, XBOOLE_0;