environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, FIN_TOPO, RCOMP_1, MARGREL1, XBOOLEAN, STRUCT_0, FUNCT_1, ZFMISC_1, PRE_TOPC, SETFAM_1, FINTOPO2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1, FUNCT_2, FIN_TOPO, ORDERS_2, PRE_TOPC, MARGREL1;
definitions TARSKI, STRUCT_0, XBOOLE_0;
theorems TARSKI, SUBSET_1, FIN_TOPO, FUNCT_2, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, FIN_TOPO;
constructors HIDDEN, DOMAIN_1, MARGREL1, PRE_TOPC, FIN_TOPO, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities SUBSET_1, XBOOLEAN, FIN_TOPO;
expansions TARSKI, XBOOLE_0, FIN_TOPO;
:: SECTION2: Formal Topological Spaces
::