environ
vocabularies HIDDEN, NUMBERS, TARSKI, PRE_TOPC, SUBSET_1, BVFUNC_2, RCOMP_1, SETFAM_1, CLASSES1, FINSET_1, CARD_1, ARYTM_3, XBOOLE_0, STRUCT_0, ZFMISC_1, NAT_1, XXREAL_0, TAXONOM2, AOFA_000, ORDERS_1, FUNCT_1, RELAT_1, NATTRA_1, EQREL_1, VECTSP_1, RLVECT_3, CARD_3, RLVECT_2, SUPINF_2, REALSET1, ARYTM_1, RLVECT_5, JORDAN13, MATROID0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, ORDERS_1, TAXONOM2, XCMPLX_0, XXREAL_0, NAT_1, CARD_1, CLASSES1, AOFA_000, STRUCT_0, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7, PRE_TOPC, TDLAT_3, MATRLIN, PENCIL_1, RANKNULL;
definitions TARSKI, FUNCT_1, CLASSES1, TAXONOM2, XBOOLE_0, STRUCT_0, PENCIL_1, FINSET_1;
theorems TARSKI, XBOOLE_1, ZFMISC_1, CARD_1, COH_SP, PRE_TOPC, NAT_1, CLASSES1, TDLAT_3, XXREAL_0, XREAL_1, XBOOLE_0, TAXONOM2, ORDERS_1, FUNCT_2, FUNCT_1, EQREL_1, WELLORD2, VECTSP_7, VECTSP_9, MATRLIN, CARD_2, VECTSP_4, ORDINAL1, CARD_FIL, RANKNULL, VECTSP_1, VECTSP_6, ALGSTR_0, HALLMAR1;
schemes FUNCT_2, NAT_1;
registrations FINSET_1, CARD_1, RELSET_1, STRUCT_0, SUBSET_1, PENCIL_1, TDLAT_3, SETFAM_1, EQREL_1, MATRLIN, XREAL_0, ALGSTR_0, BINOM, RLVECT_1, VECTSP_1, VECTSP_7, ORDINAL1;
constructors HIDDEN, COH_SP, TDLAT_3, TAXONOM2, RANKNULL, VECTSP_7, PENCIL_1, REALSET1, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities XBOOLE_0, STRUCT_0, CARD_1, ORDINAL1;
expansions TARSKI, FUNCT_1, XBOOLE_0, STRUCT_0, PENCIL_1;