environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, XBOOLE_0, TARSKI, RCOMP_1, RELAT_2, FUNCT_1, ORDINAL2, RELAT_1, STRUCT_0, TOPS_1, SETFAM_1, CONNSP_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1;
definitions XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, SUBSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, RELSET_1;
schemes SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, RELAT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOPS_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities SUBSET_1, STRUCT_0;
expansions XBOOLE_0;
:: Separated sets
::