environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, WAYBEL_0, LATTICE3, XXREAL_0, RELAT_2, YELLOW_0, EQREL_1, LATTICES, RELAT_1, WELLORD1, CAT_1, STRUCT_0, FUNCT_1, GROUP_6, SEQM_3, ORDINAL2, BINOP_1, REWRITE1, SETFAM_1, CARD_FIL, YELLOW_1, ZFMISC_1, WELLORD2, YELLOW_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0;
definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, WAYBEL_0;
theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, WELLORD1, ORDERS_2, YELLOW_0, YELLOW_1, WAYBEL_0, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_0, YELLOW_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities WAYBEL_0, STRUCT_0;
expansions TARSKI, LATTICE3, ORDERS_3, WAYBEL_0;