environ
vocabularies HIDDEN, TREES_2, ORDERS_2, RELAT_2, XBOOLE_0, STRUCT_0, ZFMISC_1, CARD_3, FINSET_1, CAT_1, YELLOW_0, SUBSET_1, XXREAL_0, TARSKI, NAT_1, YELLOW_1, WELLORD2, WELLORD1, ARYTM_3, LATTICES, FUNCT_1, FUNCT_4, RELAT_1, CARD_1, FUNCOP_1, ARYTM_1, PBOOLE, ORDERS_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, PBOOLE, CARD_3, RELAT_2, ORDERS_1, ORDERS_2, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, DOMAIN_1, STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WELLORD1, XXREAL_0;
definitions TARSKI, WAYBEL_1;
theorems CARD_1, CARD_2, CARD_4, WAYBEL_0, YELLOW_0, YELLOW_1, ORDERS_2, TARSKI, WELLORD2, NAT_1, AXIOMS, FUNCT_1, FUNCT_2, FUNCT_4, RELAT_1, RELAT_2, FUNCOP_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XREAL_1, XXREAL_0, AFINSQ_1;
schemes NAT_1;
registrations XBOOLE_0, RELSET_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, YELLOW11, CARD_1, ORDERS_2;
constructors HIDDEN, DOMAIN_1, NAT_1, NAT_D, MEMBERED, TOLER_1, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1, CARD_3;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities WELLORD1, ORDINAL1, CARD_1;
expansions TARSKI, WAYBEL_1;