environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE, MSUALG_3, REALSET1, MEMBER_1, FUNCT_6, TARSKI, FUNCT_1, WELLORD1, MSUALG_2, PRALG_2, CARD_3, SUBSET_1, MSUALG_5, MSUALG_4, FUNCOP_1, RLVECT_2, PRALG_1, EQREL_1, CLOSURE2, SETFAM_1, FUNCT_4, ZFMISC_1, GROUP_6, NUMBERS, EQUATION, ZF_MODEL, ZF_LANG, MCART_1, PZFMISC1, MSAFREE2, FINSET_1, BIRKHOFF, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, XTUPLE_0, MCART_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, CARD_3, FUNCT_6, NAT_1, FUNCOP_1, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, MSAFREE, MSAFREE2, PRALG_2, MSUALG_4, PZFMISC1, MSSUBFAM, CLOSURE2, MSUALG_5, EQUATION;
definitions FUNCT_1, RELAT_1, TARSKI, PBOOLE, PRALG_2, MSUALG_4, EQUATION, FUNCOP_1, PZFMISC1;
theorems CARD_3, CLOSURE2, EXTENS_1, FUNCOP_1, FUNCT_1, FUNCT_2, MSAFREE, MSAFREE2, MSSCYC_1, MSSUBFAM, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5, MSUALG_7, MSUALG_9, PBOOLE, PRALG_2, PRALG_3, EQUATION, RELAT_1, ZFMISC_1, SETFAM_1;
schemes DOMAIN_1, PBOOLE;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSUALG_4, MSAFREE1, MSAFREE2, EXTENS_1, MSUALG_5, CLOSURE2, PRALG_3, MSUALG_9, EQUATION, MSSUBFAM, AUTALG_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, PZFMISC1, MSSUBFAM, MSUALG_3, MSAFREE2, MSUALG_5, CLOSURE2, PRALG_3, EQUATION, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities PRALG_2, EQUATION;
expansions PBOOLE, MSUALG_4, EQUATION, PZFMISC1;
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor Andrzej Trybulec
:: for his help in the preparation of the article.
::-------------------------------------------------------------------