environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, PARTFUN1, RELAT_1, FUNCT_1, TARSKI, FUNCOP_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, FUNCT_1, FUNCT_2, GRFUNC_1, FUNCOP_1, PARTFUN1, RELAT_1, RELSET_1, XBOOLE_0;
schemes FUNCT_2, XBOOLE_0;
registrations FUNCT_1, RELSET_1;
constructors HIDDEN, PARTFUN1, FUNCOP_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0;
expansions XBOOLE_0, FUNCT_1;
:: PARTIAL FUNCTION CONSTANT ON SET
::