environ
vocabularies HIDDEN, PBOOLE, FUNCT_6, RELAT_1, PARTFUN1, FUNCT_1, SETFAM_1, SUBSET_1, FINSET_1, XBOOLE_0, TARSKI, MEMBER_1, PZFMISC1, ZFMISC_1, FUNCT_4, FUNCOP_1, FUNCT_2, ORDINAL1, MSSUBFAM, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_6, PBOOLE, MBOOLEAN, PZFMISC1;
definitions XBOOLE_0, PBOOLE, FINSET_1, ORDINAL1;
theorems FUNCOP_1, FINSET_1, ORDERS_1, FRAENKEL, FUNCT_2, FUNCT_4, FUNCT_6, MBOOLEAN, PBOOLE, PZFMISC1, SETFAM_1, TARSKI, RELSET_1, XBOOLE_0, XBOOLE_1, RELAT_1, PARTFUN1;
schemes FUNCT_2, PBOOLE;
registrations XBOOLE_0, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE, PRE_CIRC, MBOOLEAN, PZFMISC1, FUNCT_2, PARTFUN1, CARD_1, RELSET_1, RELAT_1;
constructors HIDDEN, SETFAM_1, FUNCT_4, FUNCT_6, MBOOLEAN, PZFMISC1, PARTFUN1, RELSET_1, ORDINAL1, PBOOLE, FINSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities PBOOLE, FUNCOP_1;
expansions XBOOLE_0, PBOOLE;
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 )