environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, GROUP_1, FINSEQ_1, GROUP_3, XXREAL_0, CARD_1, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, ARYTM_3, STRUCT_0, PRE_TOPC, GROUP_6, BINOP_1, TARSKI, XBOOLE_0, QC_LANG1, WELLORD1, NAT_1, FUNCT_2, ALGSTR_0, GRAPH_1, GRSOLV_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, STRUCT_0, ALGSTR_0, BINOP_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, GR_CY_1, FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6, XXREAL_0;
definitions TARSKI;
theorems FINSEQ_1, BINOP_1, GROUP_2, GROUP_3, TARSKI, GROUP_6, FINSEQ_2, FUNCT_1, FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, STRUCT_0;
schemes FINSEQ_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ORDINAL1;
constructors HIDDEN, BINOP_1, FINSUB_1, REALSET1, GROUP_6, GR_CY_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities GROUP_2, RELAT_1, ALGSTR_0;
expansions TARSKI;