environ
vocabularies HIDDEN, PRE_TOPC, SETFAM_1, RCOMP_1, SUBSET_1, XBOOLE_0, WAYBEL_3, YELLOW13, CONNSP_2, TARSKI, ZFMISC_1, TOPS_1, CARD_5, COMPTS_1, NATTRA_1, RELAT_1, FUNCT_3, FUNCT_1, QUOFIELD, TOPS_2, ORDINAL2, STRUCT_0, ORDINAL1, FINSET_1, COMPACT1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, SETFAM_1, ORDINAL1, FINSET_1, FINSUB_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TDLAT_3, TSEP_1, TEX_3, COMPTS_1, CONNSP_2, WAYBEL_3, YELLOW_9, YELLOW13;
definitions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, WAYBEL_3, YELLOW13, SETFAM_1;
theorems XBOOLE_1, ZFMISC_1, YELLOW_8, YELLOW_9, XBOOLE_0, CONNSP_2, TEX_3, TEX_4, PRE_TOPC, TOPS_1, TOPS_2, TSEP_1, TARSKI, FUNCT_1, FINSET_1, TDLAT_3, FUNCT_2, SUBSET_1, COMPTS_1, TOPMETR, YELLOW13, SETFAM_1;
schemes FUNCT_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, FINSUB_1, RELAT_1, TOPS_1, BORSUK_2, FUNCT_1, PRE_TOPC, TEX_1, YELLOW13, COMPTS_1, RELSET_1;
constructors HIDDEN, FINSOP_1, DOMAIN_1, TOPS_1, TOPS_2, YELLOW_9, YELLOW13, TDLAT_3, CONNSP_2, T_0TOPSP, WAYBEL_3, TSEP_1, TEX_3, COMPTS_1, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities ORDINAL1, STRUCT_0, SUBSET_1;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, WAYBEL_3;