environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, ORDERS_2, STRUCT_0, CAT_1, YELLOW_0, SUBSET_1, RCOMP_1, WELLORD1, TARSKI, LATTICES, REWRITE1, WAYBEL_0, XXREAL_0, WAYBEL_3, WAYBEL_6, CARD_FIL, LATTICE3, EQREL_1, ORDINAL2, FINSET_1, ZFMISC_1, WAYBEL_4, MSSUBFAM, WAYBEL_7, INT_2, WAYBEL_1, FUNCT_1, GROUP_6, RELAT_1, BINOP_1, SEQM_3, YELLOW_1, FILTER_1, SETFAM_1, WAYBEL_8, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CARD_1, FINSET_1, RELAT_1, TOLER_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, RELAT_2, STRUCT_0, ORDERS_2, LATTICE3, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7;
definitions TARSKI, RELAT_2, ORDERS_2;
theorems TARSKI, STRUCT_0, FINSET_1, FUNCT_1, FUNCT_2, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_5, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, RELAT_1, YELLOW_7, XBOOLE_0, XBOOLE_1;
schemes SUBSET_1, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6;
constructors HIDDEN, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, RELSET_1, PRALG_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities YELLOW_2, STRUCT_0;
expansions TARSKI, RELAT_2, ORDERS_2;