environ
vocabularies HIDDEN, NUMBERS, GROUP_1, GROUP_2, GRAPH_1, GROUP_6, SUBSET_1, INT_1, GR_CY_1, XXREAL_0, NEWTON, CARD_1, GROUP_4, STRUCT_0, FINSET_1, RELAT_1, ARYTM_3, NAT_1, INT_2, ALGSTR_0, ARYTM_1, FINSEQ_1, FUNCT_1, TARSKI, WELLORD1, FUNCT_2, GROUP_5, PRE_TOPC, XCMPLX_0, ORDINAL1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2, NUMBERS, INT_1, INT_2, CARD_1, NAT_D, GROUP_2, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_3, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, FINSEQ_1, XXREAL_0;
definitions FUNCT_1, TARSKI;
theorems FUNCT_2, GROUP_1, GROUP_2, GROUP_4, GROUP_5, FUNCT_1, GROUP_6, GR_CY_1, NAT_1, INT_1, INT_2, FINSEQ_1, XBOOLE_0, XCMPLX_1, NEWTON, XREAL_1, ORDINAL1, NAT_D, STRUCT_0, XXREAL_0, RELAT_1;
schemes FUNCT_2, FINSEQ_1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1, MEMBERED, CARD_1;
constructors HIDDEN, BINOP_1, DOMAIN_1, REAL_1, NAT_D, BINOP_2, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ALGSTR_0, GR_CY_1;
expansions GR_CY_1;