environ
vocabularies HIDDEN, ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, FINANCE1, FINSEQ_1, FUNCT_1, INT_1, IRRAT_1, NAT_1, NEWTON, NUMBERS, PROB_1, PROB_3, RAT_1, REAL_1, REAL_3, RELAT_1, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, XXREAL_1, INT_2, ORDINAL1, SQUARE_1, ABIAN, FINSET_1, SEQ_1, ORDINAL2, SEQ_2, VALUED_1, DIOPHAN1, NAT_6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, XREAL_0, COMPLEX1, FINSEQ_1, XXREAL_1, PROB_1, FINANCE1, PROB_3, IRRAT_1, REAL_3, NEWTON, SQUARE_1, REAL_1, ABIAN, INT_2, FINSET_1, RAT_1, COMSEQ_2, SEQ_1, SEQ_2, VALUED_1, NAT_D, FUNCOP_1, NAT_6;
definitions NAT_6;
theorems AXIOMS, INT_1, INT_2, NAT_1, XXREAL_0, XREAL_1, FINSEQ_1, ORDINAL1, XBOOLE_1, FUNCT_1, FUNCT_2, ABSVALUE, NEWTON, XXREAL_1, CARD_1, FINSEQ_4, COMPLEX1, XCMPLX_0, XCMPLX_1, PROB_3, CARD_2, REAL_3, SERIES_2, SQUARE_1, WSIERP_1, RAT_1, SEQ_1, VALUED_1, SEQ_2;
schemes FUNCT_2, FINSEQ_1, NAT_1, FIB_NUM, SEQ_1;
registrations XREAL_0, NAT_1, INT_1, FINSET_1, XXREAL_0, NEWTON, CARD_1, VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, FUNCT_2, ABIAN, NAT_3, SQUARE_1, REAL_3, ZFMISC_1, FINANCE1, RAT_1, MEMBERED, VALUED_1, SEQ_1, SEQ_2, NAT_6;
constructors HIDDEN, REAL_1, SQUARE_1, SEQ_2, NEWTON, RELSET_1, COMSEQ_2, ABIAN, REAL_3, PROB_3, FINANCE1, NAT_6;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ORDINAL1, FINSEQ_1, SUBSET_1, CARD_3, XBOOLE_0, CARD_1, VALUED_1, XCMPLX_0;
expansions TARSKI, XBOOLE_0, PBOOLE, XREAL_0, SETFAM_1, ORDINAL1, NAT_6;