environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, FINSEQ_1, TARSKI, RELAT_1, NAT_1, ORDINAL4, ARYTM_3, FINSET_1, CARD_1, XXREAL_0, ORDINAL1, TREES_1, AMISTD_3, FINSEQ_2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, XCMPLX_0, ORDINAL1, NAT_1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FUNCT_2, FINSET_1, XXREAL_0;
definitions TARSKI, FINSET_1, FUNCT_1, WELLORD2, XBOOLE_0;
theorems TARSKI, NAT_1, FINSEQ_1, FINSET_1, FUNCT_1, CARD_1, RELAT_1, GRFUNC_1, CARD_2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, ENUMSET1, FINSEQ_2, FINSEQ_3, FUNCT_2;
schemes NAT_1, CLASSES1, XBOOLE_0, FUNCT_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, FINSEQ_2;
constructors HIDDEN, ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCOP_1, FUNCT_2, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
set D = {{}};