environ
vocabularies HIDDEN, WAYBEL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, ORDERS_2, ORDERS_1, STRUCT_0, XXREAL_0, TARSKI, ARYTM_3, LATTICE3, ARYTM_0, RELAT_1, RELAT_2, CARD_FIL, REWRITE1, FUNCT_1, FUNCOP_1, YELLOW_0, SEQM_3, FINSET_1, ORDINAL2, YELLOW_1, SETFAM_1, WELLORD2, ZFMISC_1, WAYBEL_1, WAYBEL_6, YELLOW_8, WAYBEL_2, INT_2, WAYBEL_3, WAYBEL_8, RCOMP_1, WAYBEL16;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELSET_1, FUNCT_2, FUNCOP_1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, SUBSET_1, SETFAM_1, RELAT_1, ZFMISC_1, FUNCOP_1, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, WAYBEL_8, WAYBEL13, WAYBEL14, WAYBEL15, XBOOLE_0, XBOOLE_1;
schemes DOMAIN_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_6, WAYBEL_8;
constructors HIDDEN, DOMAIN_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities ;
expansions TARSKI, XBOOLE_0;