environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, STRUCT_0, TARSKI, TOPS_1, RCOMP_1, TSEP_1, CONNSP_1, SETFAM_1, TSEP_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, STRUCT_0, TOPS_1, BORSUK_1, CONNSP_1, TSEP_1;
definitions BORSUK_1, TSEP_1, XBOOLE_0;
theorems PRE_TOPC, TOPS_1, CONNSP_1, TSEP_1, TDLAT_1, TDLAT_3, SUBSET_1, XBOOLE_1;
schemes ;
registrations STRUCT_0, PRE_TOPC;
constructors HIDDEN, TOPS_1, CONNSP_1, BORSUK_1, TSEP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions BORSUK_1, TSEP_1, XBOOLE_0;