environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, TARSKI, FINSUB_1, BINOP_1, LATTICES, EQREL_1, STRUCT_0, PBOOLE, SETWISEO, FUNCOP_1, FILTER_0, FINSET_1, XXREAL_2, LATTICE2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, PARTFUN1, FUNCOP_1, BINOP_1, FINSET_1, STRUCT_0, LATTICES, FINSUB_1, SETWISEO, FILTER_0;
definitions LATTICES, BINOP_1, SETWISEO, FILTER_0;
theorems LATTICES, BINOP_1, SETWISEO, FUNCOP_1, FUNCT_4, SETWOP_2, FINSET_1, FINSUB_1, FUNCT_2, FUNCT_1, FILTER_0, GRFUNC_1, RELAT_1, RLSUB_2, XBOOLE_1;
schemes FRAENKEL;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, RELSET_1, FILTER_0;
constructors HIDDEN, BINOP_1, FUNCOP_1, FUNCT_4, SETWISEO, GROUP_1, FILTER_0, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICES;
expansions LATTICES, BINOP_1, SETWISEO;