environ
vocabularies HIDDEN, ZFMISC_1, CARD_1, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, STRUCT_0, RELAT_2, ORDERS_2, WAYBEL_0, FUNCOP_1, MONOID_0, YELLOW_6, XXREAL_0, SEQM_3, PRE_TOPC, WAYBEL_9, WAYBEL24, CAT_1, YELLOW_0, NEWTON, CARD_3, FUNCT_2, VALUED_1, WELLORD1, LATTICE3, XXREAL_2, LATTICES, TARSKI, T_0TOPSP, TOPS_2, ORDINAL2, WAYBEL11, RCOMP_1, CARD_FIL, YELLOW_8, SETFAM_1, FINSET_1, WAYBEL_3, TOPS_1, WAYBEL18, PBOOLE, RLVECT_2, FUNCT_4, CANTOR_1, WAYBEL_1, FUNCT_3, GROUP_6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, TOPS_2, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_4, FUNCOP_1, ORDINAL1, NUMBERS, FUNCT_7, CARD_3, MONOID_0, SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0, PRALG_1, PRE_TOPC, TOPS_1, COMPTS_1, T_0TOPSP, CANTOR_1, TMAP_1, ORDERS_2, LATTICE3, WAYBEL18, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_1, YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_9, WAYBEL11, WAYBEL24;
definitions TARSKI, MONOID_0, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, T_0TOPSP, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, YELLOW_8, FUNCT_2, XBOOLE_0, FUNCOP_1;
theorems TARSKI, PRE_TOPC, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_7, PRALG_1, FUNCOP_1, CARD_3, BORSUK_1, TOPS_2, TOPS_3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_9, WAYBEL11, WAYBEL10, WAYBEL13, WAYBEL18, WAYBEL24, YELLOW_8, TMAP_1, TSP_1, FUNCT_4, URYSOHN1, XBOOLE_0, XBOOLE_1, SETFAM_1, CARD_1, PARTFUN1, RELSET_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_1, YELLOW_0, TEX_4, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_8, WAYBEL18, WAYBEL19, TOPGRP_1, BORSUK_3, WAYBEL24, RELSET_1, FINSET_1;
constructors HIDDEN, FINSUB_1, REALSET1, FUNCT_7, TOPS_1, TOPS_2, LATTICE3, TMAP_1, T_0TOPSP, CANTOR_1, MONOID_0, ORDERS_3, WAYBEL_1, YELLOW_8, WAYBEL11, WAYBEL18, WAYBEL24, COMPTS_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities ORDINAL1, STRUCT_0, FUNCOP_1;
expansions TARSKI, PRE_TOPC, TOPS_2, T_0TOPSP, WAYBEL_0, FUNCT_2, XBOOLE_0;