environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, TARSKI, TOPS_1, XBOOLE_0, SETFAM_1, RCOMP_1, FUNCT_1, RELAT_1, ORDINAL2, DECOMP_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1;
definitions TARSKI, XBOOLE_0;
theorems TOPS_1, PRE_TOPC, TOPS_2, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1;
registrations SUBSET_1, PRE_TOPC, TOPS_1;
constructors HIDDEN, TOPS_1, RELSET_1;
requirements HIDDEN, SUBSET;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, XBOOLE_0;