environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, CAT_1, STRUCT_0, YELLOW_0, SUBSET_1, TARSKI, XXREAL_0, RELAT_1, ARYTM_0, WELLORD1, FUNCOP_1, WAYBEL_3, RELAT_2, SEQM_3, FUNCT_1, WAYBEL_1, BINOP_1, WAYBEL_0, ORDINAL2, GROUP_6, YELLOW_1, FUNCT_2, NEWTON, CARD_3, RLVECT_2, REWRITE1, UNIALG_2, ZFMISC_1, LATTICE3, LATTICES, EQREL_1, WAYBEL10;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_3, FUNCOP_1, STRUCT_0, TMAP_1, QUANTAL1, PRALG_1, WELLORD1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_7;
definitions TARSKI, XBOOLE_0, RELAT_1, QUANTAL1, ORDERS_2, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_3;
theorems FUNCT_1, FUNCT_2, YELLOW_0, YELLOW_1, WAYBEL_1, FUNCOP_1, RELSET_1, SYSREL, ORDERS_2, YELLOW_2, WAYBEL_0, ZFMISC_1, TARSKI, YELLOW_7, RELAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1, TMAP_1;
schemes YELLOW_0, FUNCT_2, XBOOLE_0;
registrations FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, RELSET_1;
constructors HIDDEN, TOLER_1, BORSUK_1, PRALG_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, TMAP_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, LATTICE3, YELLOW_2, STRUCT_0;
expansions TARSKI, XBOOLE_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0;