environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, PARTIT1, EQREL_1, TARSKI, ZFMISC_1, FUNCT_1, SETFAM_1, RELAT_1, PARTFUN1, MARGREL1, BVFUNC_1, XBOOLEAN, BVFUNC_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, EQREL_1, PARTIT1, BVFUNC_1;
definitions TARSKI, BVFUNC_1, FUNCT_2;
theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, ZFMISC_1, SUBSET_1, MARGREL1, BINARITH, PARTIT1, BVFUNC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XBOOLEAN, PARTFUN1;
schemes DOMAIN_1, PARTFUN2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XBOOLEAN, EQREL_1, MARGREL1, PARTIT1;
constructors HIDDEN, SETFAM_1, PARTIT1, BVFUNC_1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities XBOOLEAN;
expansions TARSKI;