environ
vocabularies HIDDEN, RELAT_1, EQREL_1, XBOOLE_0, SUBSET_1, TARSKI, SETFAM_1, ZFMISC_1, FUNCT_1, RELSET_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1;
definitions XBOOLE_0, TARSKI, RELAT_1;
theorems RELAT_1, TARSKI, SETFAM_1, ZFMISC_1, XBOOLE_1, SUBSET_1, RELSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, MSSUBFAM, EQREL_1, SYSREL, ORDERS_1, XTUPLE_0;
schemes CLASSES1, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, RELSET_1;
constructors HIDDEN, SETFAM_1, FUNCT_2, EQREL_1, RELSET_1, DOMAIN_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities EQREL_1, SUBSET_1, RELAT_1;
expansions XBOOLE_0, TARSKI;