environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, WELLORD1, RELAT_2, TARSKI;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1;
definitions TARSKI, WELLORD1;
theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes TARSKI, FUNCT_1, RELAT_1, XBOOLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1;
constructors HIDDEN, TARSKI, SUBSET_1, RELAT_2, WELLORD1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, WELLORD1;
expansions TARSKI, WELLORD1;