environ
vocabularies HIDDEN, FINSUB_1, TARSKI, SETFAM_1, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, CARD_3, CARD_1, ORDINAL1, STRUCT_0, PRE_TOPC, RCOMP_1, RLVECT_3, CANTOR_1, TOPS_1, TOPS_3, COMPTS_1, SETWISEO, FINSET_1, CARD_5, WAYBEL_3, YELLOW_8;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CANTOR_1, SETFAM_1, ORDINAL1, CARD_1, CARD_3, FINSET_1, FINSUB_1, SETWISEO, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TOPS_3, COMPTS_1, WAYBEL_3;
definitions TARSKI, CANTOR_1, PRE_TOPC, WELLORD2, FUNCT_1, CARD_3, WAYBEL_3, COMPTS_1, XBOOLE_0;
theorems TOPS_1, PRE_TOPC, PCOMPS_1, CANTOR_1, TARSKI, ZFMISC_1, TOPS_3, COMPTS_1, URYSOHN1, TSP_1, FINSUB_1, SETFAM_1, SUBSET_1, FUNCT_1, CARD_1, XBOOLE_0, XBOOLE_1, TOPS_2;
schemes DOMAIN_1, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, FINSUB_1, CARD_5, STRUCT_0, PRE_TOPC, TOPS_1, PCOMPS_1;
constructors HIDDEN, SETFAM_1, SETWISEO, REALSET1, TOPS_1, COMPTS_1, URYSOHN1, TOPS_3, T_0TOPSP, CANTOR_1, WAYBEL_3, TOPS_2;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0, SUBSET_1;
expansions TARSKI, PRE_TOPC, WAYBEL_3, XBOOLE_0;