environ
vocabularies HIDDEN, FUNCT_1, PARTFUN1, TARSKI, RELAT_1, SUBSET_1, CARD_1, XBOOLE_0, CARD_5, ORDINAL2, ORDERS_2, WELLORD1, STRUCT_0, WAYBEL_0, XXREAL_0, ZFMISC_1, SETFAM_1, ORDINAL1, CARD_2, FINSET_1, FUNCOP_1, FUNCT_4, NAT_1, ARYTM_3, NUMBERS, WELLFND1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, BINOP_1, SETFAM_1, DOMAIN_1, XCMPLX_0, NAT_1, STRUCT_0, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, WELLORD1, ORDINAL2, FINSET_1, CARD_2, ORDERS_2, CARD_5, RFUNCT_3, WAYBEL_0;
definitions TARSKI, RELAT_1, FUNCT_1, WELLORD1, WAYBEL_0, XBOOLE_0;
theorems TARSKI, ENUMSET1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, ORDINAL1, WELLORD1, GRFUNC_1, PARTFUN1, FUNCT_2, ORDINAL2, FUNCOP_1, CARD_1, ORDERS_2, FUNCT_4, CARD_5, XBOOLE_0, XBOOLE_1, BINOP_1, CARD_2, XTUPLE_0;
schemes NAT_1, SUBSET_1, DOMAIN_1, FUNCT_7, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, CARD_1, CARD_5, STRUCT_0, WAYBEL_0, FUNCT_1, ZFMISC_1, XCMPLX_0, NAT_1;
constructors HIDDEN, SETFAM_1, WELLORD1, BINOP_1, FUNCT_4, ORDINAL2, CARD_2, REALSET1, CARD_5, RFUNCT_3, WAYBEL_0, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities BINOP_1, FUNCOP_1;
expansions TARSKI, FUNCT_1, WELLORD1, WAYBEL_0, XBOOLE_0;