environ
vocabularies HIDDEN, GROUP_1, GROUP_2, STRUCT_0, XBOOLE_0, GROUP_3, SUBSET_1, GROUP_4, EQREL_1, TARSKI, GROUP_6, RELAT_1, FUNCT_1, ZFMISC_1, SETFAM_1, RLSUB_2, LATTICES, PBOOLE, REWRITE1, LATTICE3, VECTSP_8;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, SETFAM_1, RELAT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, LATTICES, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4, VECTSP_8;
definitions TARSKI, LATTICE3, VECTSP_8, XBOOLE_0;
theorems TARSKI, FUNCT_1, SUBSET_1, SETFAM_1, FUNCT_2, LATTICES, GROUP_2, GROUP_3, GROUP_4, GROUP_6, VECTSP_8, RELAT_1, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FUNCT_2;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, GROUP_3, GROUP_4, RELSET_1;
constructors HIDDEN, BINOP_1, REALSET1, GROUP_4, GROUP_6, LATTICE3, LATTICE4, VECTSP_8, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, RELAT_1, GROUP_4;
expansions TARSKI, LATTICE3, XBOOLE_0;