environ
vocabularies HIDDEN, PBOOLE, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ZFMISC_1, FUNCT_2, CARD_3, FINSET_1, COMPLEX1, SETFAM_1, FUNCT_4, MSSUBFAM, FUNCOP_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1, PRE_TOPC, CLOSURE2, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, PBOOLE, CARD_3, MSUALG_1, MBOOLEAN, MSSUBFAM;
definitions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, CARD_3, TARSKI;
theorems FUNCOP_1, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, PBOOLE, PZFMISC1, SETFAM_1, TARSKI, MSSUBFAM, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, RELAT_1;
schemes FRAENKEL, FUNCT_1, FUNCT_2, DOMAIN_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, PBOOLE, MSUALG_1;
constructors HIDDEN, SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_1, CARD_3, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCOP_1;
expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI;
Lm1:
for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
deffunc H1( set ) -> set = $1;