environ
vocabularies HIDDEN, NUMBERS, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ZFMISC_1, PROB_1, FINSUB_1, FUNCT_1, SUPINF_2, XXREAL_0, MSSUBFAM, ARYTM_3, VALUED_0, FUNCOP_1, ARYTM_1, RELAT_1, CARD_3, CARD_1, NAT_1, EQREL_1, PROB_2, SUPINF_1, MEASURE1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, FUNCOP_1, PROB_1, PROB_2, VALUED_0, FUNCT_7, SUPINF_1, SUPINF_2;
definitions SUPINF_2, TARSKI, FINSUB_1, PROB_2, PROB_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ENUMSET1, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_2, RELAT_1, FUNCOP_1, FINSUB_1, PROB_2, PROB_1, SUBSET_1, XBOOLE_0, XBOOLE_1, XXREAL_0, CARD_3, ORDINAL1, VALUED_0, XXREAL_3, FUNCT_7;
schemes FUNCT_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, PROB_1, VALUED_0, FINSUB_1, RELAT_1, XXREAL_0;
constructors HIDDEN, ENUMSET1, PARTFUN1, FUNCOP_1, FINSUB_1, REAL_1, NAT_1, PROB_2, SUPINF_2, SUPINF_1, RELSET_1, FUNCT_7;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities PROB_1, SUBSET_1;
expansions TARSKI, FINSUB_1, PROB_1, XBOOLE_0;
scheme
DomsetFamEx{
F1()
-> set ,
P1[
set ] } :
provided
A1:
ex
B being
set st
(
B c= F1() &
P1[
B] )
:: Field Subset of X and nonnegative measure
::