environ
vocabularies HIDDEN, VECTSP_1, STRUCT_0, GROUP_4, XXREAL_2, LATTICES, RLSUB_2, RLSUB_1, XBOOLE_0, SUBSET_1, GROUP_2, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, SETFAM_1, ARYTM_3, PBOOLE, TARSKI, EQREL_1, REWRITE1, LATTICE3, RLVECT_3, GROUP_6, VECTSP_8, MSSUBFAM, UNIALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, VECTSP_1, LATTICES, VECTSP_5, LATTICE3, VECTSP_4, VECTSP_7, GRCAT_1, MOD_2;
definitions LATTICE3, TARSKI;
theorems TARSKI, VECTSP_5, LATTICES, LATTICE4, VECTSP_4, SETFAM_1, VECTSP_7, MOD_2, SUBSET_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, STRUCT_0, VECTSP_1;
schemes FUNCT_2, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, VECTSP_2, VECTSP_4, VECTSP_5, RELSET_1;
constructors HIDDEN, SETFAM_1, BINOP_1, REALSET1, VECTSP_5, VECTSP_7, MOD_2, LATTICE3, LATTICE4, RELSET_1, GRCAT_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities ;
expansions LATTICE3;