environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, WAYBEL_0, XXREAL_0, ORDINAL2, RCOMP_1, LATTICE3, YELLOW_0, EQREL_1, TARSKI, STRUCT_0, LATTICES, REWRITE1, TREES_2, ORDERS_1, ZFMISC_1, ARYTM_3, FINSET_1, CARD_FIL, WAYBEL_2, FUNCT_1, RELAT_1, FUNCT_7, NUMBERS, CARD_1, NAT_1, YELLOW_1, PBOOLE, FUNCOP_1, CARD_3, RLVECT_2, MONOID_0, FUNCT_4, PRE_TOPC, SETFAM_1, WELLORD2, TOPS_1, CARD_5, COMPTS_1, WAYBEL_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FINSET_1, DOMAIN_1, ORDERS_1, SETFAM_1, STRUCT_0, FUNCT_1, FUNCT_4, PBOOLE, CARD_3, FUNCOP_1, PRALG_1, FUNCT_7, MONOID_0, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_4, WAYBEL_2, XXREAL_0;
definitions TARSKI, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_2, COMPTS_1, YELLOW_0, WAYBEL_0, WAYBEL_2, XBOOLE_0, STRUCT_0, SETFAM_1;
theorems TARSKI, ORDERS_2, ZFMISC_1, NAT_1, RELAT_1, FUNCT_1, FINSET_1, FUNCT_4, FUNCOP_1, CARD_3, PRALG_1, FUNCT_7, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, URYSOHN1, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2, YELLOW_4, XBOOLE_0, XBOOLE_1, MONOID_0, ORDINAL1, SETFAM_1, PARTFUN1;
schemes NAT_1, FINSET_1, SUBSET_1, CLASSES1, PBOOLE, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, CARD_3, STRUCT_0, TOPS_1, COMPTS_1, ORDERS_2, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, ORDINAL1, PRE_TOPC, FUNCT_7, NAT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, FUNCT_7, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, MONOID_0, PRALG_1, YELLOW_1, YELLOW_4, WAYBEL_2, RELSET_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities WAYBEL_0, SUBSET_1, STRUCT_0;
expansions TARSKI, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_2, COMPTS_1, YELLOW_0, WAYBEL_2;