environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, TOPS_1, XBOOLE_0, STRUCT_0, RCOMP_1, TARSKI, NATTRA_1, ZFMISC_1, SETFAM_1, TDLAT_1, REALSET1, LATTICES, FUNCT_1, EQREL_1, TDLAT_2, PBOOLE, TDLAT_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1, TDLAT_2;
definitions TARSKI, BORSUK_1, TSEP_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BORSUK_1, TSEP_1, LATTICES, TDLAT_1, TDLAT_2, SUBSET_1, XBOOLE_0, XBOOLE_1, RELSET_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1;
constructors HIDDEN, SETFAM_1, REALSET1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_1, TDLAT_2, TSEP_1, BINOP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities REALSET1, SUBSET_1, STRUCT_0, TDLAT_1;
expansions TARSKI, BORSUK_1, TSEP_1, XBOOLE_0, TDLAT_1;