environ
vocabularies HIDDEN, FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, XXREAL_0, RELAT_1, SUPINF_1, ORDINAL2, PROB_1, MEASURE2, MEASURE1, TARSKI, SETFAM_1, CARD_1, XBOOLE_0, ARYTM_3, NAT_1, ARYTM_1, REAL_1, XXREAL_2, ZFMISC_1, MEASURE3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1, XXREAL_2, SUPINF_1, SUPINF_2, MEASURE1, MEASURE2;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_2, MEASURE1, MEASURE2, PROB_2, XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_1, FINSUB_1, ORDINAL1, XXREAL_2, VALUED_0, XXREAL_3, RELAT_1, XREAL_0;
schemes NAT_1, FUNCT_2, XFAMILY;
registrations SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, MEASURE1, VALUED_0, XXREAL_3, RELSET_1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE1, MEASURE2, SUPINF_1, RELSET_1, XREAL_0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
:: Completeness of sigma_additive Measure
::