environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, EQREL_1, STRUCT_0, SUBSET_1, BORSUK_1, RELAT_1, TARSKI, CARD_3, RCOMP_1, ZFMISC_1, SETFAM_1, ORDINAL2, FUNCT_1, T_1TOPSP;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, EQREL_1, TOPS_2, BORSUK_1;
definitions TARSKI, PRE_TOPC, XBOOLE_0;
theorems PRE_TOPC, TARSKI, SETFAM_1, EQREL_1, URYSOHN1, BORSUK_1, FUNCT_2, FUNCT_1, TOPS_2, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes CLASSES1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, STRUCT_0, PRE_TOPC, BORSUK_1;
constructors HIDDEN, TOPS_2, BORSUK_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, PRE_TOPC, XBOOLE_0;