environ
vocabularies HIDDEN, XBOOLE_0, MARGREL1, XBOOLEAN, BVFUNC_1, PARTIT1, FUNCT_1, SUBSET_1, RELAT_1, TARSKI;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, RELAT_1, FUNCT_1, FUNCT_2, BVFUNC_1, MARGREL1;
definitions TARSKI, FUNCT_2, MARGREL1;
theorems BVFUNC_1, BVFUNC_4, BVFUNC_5, BVFUNC_6, FUNCT_1, FUNCT_2, MARGREL1, XBOOLEAN, PARTFUN1;
schemes FUNCT_1;
registrations XBOOLE_0, FUNCT_2, XBOOLEAN, MARGREL1, RELSET_1;
constructors HIDDEN, BVFUNC_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions ;