environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, SUBSET_1, FIN_TOPO, TARSKI, PRE_TOPC, FUNCT_1, NUMBERS, ZFMISC_1, STRUCT_0, ARYTM_3, CARD_1, RELAT_1, NAT_1, FINTOPO3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FIN_TOPO, PRE_TOPC, STRUCT_0, ORDERS_2;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, FIN_TOPO, FINTOPO2, ORDINAL1;
schemes RECDEF_1, NAT_1, DOMAIN_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, FIN_TOPO, XCMPLX_0, NAT_1;
constructors HIDDEN, NAT_1, FIN_TOPO, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities XBOOLE_0, SUBSET_1;
expansions TARSKI;
:: (A^f is an inflation of A).