@ARTICLE(HIDDEN.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Mizar Built-in Notions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {Axiomatics},
    NOTE    = {\url{http://mizar.org/JFM/Axiomatics/hidden.html}})

@ARTICLE(TARSKI.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Tarski {G}rothendieck Set Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {Axiomatics},
    NOTE    = {\url{http://mizar.org/JFM/Axiomatics/tarski.html}})

@ARTICLE(AXIOMS.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Strong Arithmetic of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {Addenda},
    NOTE    = {\url{http://mizar.org/JFM/Addenda/axioms.html}})

@ARTICLE(STRUCT_0.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Preliminaries to Structures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {Addenda},
    NOTE    = {\url{http://mizar.org/JFM/Addenda/struct_0.html}})

@ARTICLE(ARYTM_3.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Arithmetic of Non Negative Rational Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1998},
    VOLUME  = {Addenda},
    NOTE    = {\url{http://mizar.org/JFM/Addenda/arytm_3.html}})

@ARTICLE(ARYTM_2.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Non Negative Real Numbers. {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1998},
    VOLUME  = {Addenda},
    NOTE    = {\url{http://mizar.org/JFM/Addenda/arytm_2.html}})

@ARTICLE(ARYTM_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Non Negative Real Numbers. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1998},
    VOLUME  = {Addenda},
    NOTE    = {http://mizar.\-org/\-Addenda/\-arytm\_1\-.html})

@ARTICLE(ARYTM.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Preliminaries to Arithmetic},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {Addenda},
    NOTE    = {\url{http://mizar.org/JFM/Addenda/arytm.html}})

@ARTICLE(XBOOLE_0.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Boolean Properties of Sets --- Definitions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {2002},
    VOLUME  = {EMM},
    NOTE    = {\url{http://mizar.org/JFM/EMM/xboole_0.html}})

@ARTICLE(XBOOLE_1.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Boolean Properties of Sets --- Theorems},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {2002},
    VOLUME  = {EMM},
    NOTE    = {\url{http://mizar.org/JFM/EMM/xboole_1.html}})

@ARTICLE(BOOLE.ABS,
    AUTHOR  = {Committee, Library},
    TITLE   = {Boolean Properties of Sets --- Requirements},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {2002},
    VOLUME  = {EMM},
    NOTE    = {\url{http://mizar.org/JFM/EMM/boole.html}})

@ARTICLE(ENUMSET1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Enumerated Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/enumset1.html}})

@ARTICLE(ZFMISC_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Some Basic Properties of Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/zfmisc_1.html}})

@ARTICLE(SUBSET_1.ABS,
    AUTHOR  = {Trybulec, Zinaida},
    TITLE   = {Properties of Subsets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/subset_1.html}})

@ARTICLE(RELAT_1.ABS,
    AUTHOR  = {Woronowicz, Edmund},
    TITLE   = {Relations and Their Basic Properties},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/relat_1.html}})

@ARTICLE(FUNCT_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Functions and Their Basic Properties},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/funct_1.html}})

@ARTICLE(GRFUNC_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Graphs of Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/grfunc_1.html}})

@ARTICLE(RELAT_2.ABS,
    AUTHOR  = {Woronowicz, Edmund and Zalewska, Anna},
    TITLE   = {Properties of Binary Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/relat_2.html}})

@ARTICLE(ORDINAL1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {The Ordinal Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/ordinal1.html}})

@ARTICLE(WELLORD1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {The Well Ordering Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/wellord1.html}})

@ARTICLE(SETFAM_1.ABS,
    AUTHOR  = {Padlewska, Beata},
    TITLE   = {Families of Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/setfam_1.html}})

@ARTICLE(ORDINAL2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Sequences of Ordinal Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/ordinal2.html}})

@ARTICLE(ORDINAL3.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Ordinal Arithmetics},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/ordinal3.html}})

@ARTICLE(REAL_1.ABS,
    AUTHOR  = {Hryniewiecki, Krzysztof},
    TITLE   = {Basic Properties of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/real_1.html}})

@ARTICLE(ABSVALUE.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Some Properties of Functions
Modul and Signum},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/absvalue.html}})

@ARTICLE(SQUARE_1.ABS,
    AUTHOR  = {Trybulec, Andrzej and Byli\'nski, Czes{\l}aw},
    TITLE   = {Some Properties of Real Numbers
Operations: min, max, square, and square root},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/square_1.html}})

@ARTICLE(NAT_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {The Fundamental Properties of Natural Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/nat_1.html}})

@ARTICLE(MCART_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Tuples, Projections and {C}artesian Products},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/mcart_1.html}})

@ARTICLE(RELSET_1.ABS,
    AUTHOR  = {Woronowicz, Edmund},
    TITLE   = {Relations Defined on Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/relset_1.html}})

@ARTICLE(PARTFUN1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Partial Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/partfun1.html}})

@ARTICLE(FINSET_1.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {Finite Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/finset_1.html}})

@ARTICLE(WELLORD2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Zermelo Theorem and Axiom of Choice},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/wellord2.html}})

@ARTICLE(CARD_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Cardinal Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/card_1.html}})

@ARTICLE(FUNCT_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Functions from a Set to a Set},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/funct_2.html}})

@ARTICLE(FINSEQ_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Hryniewiecki, Krzysztof},
    TITLE   = {Segments of Natural Numbers and Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/finseq_1.html}})

@ARTICLE(DOMAIN_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Domains and Their {C}artesian Products},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/domain_1.html}})

@ARTICLE(ZF_LANG.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {A Model of {ZF} Set Theory Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/zf_lang.html}})

@ARTICLE(BINOP_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Binary Operations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/binop_1.html}})

@ARTICLE(FINSUB_1.ABS,
    AUTHOR  = {Trybulec, Andrzej and Darmochwa{\l}, Agata},
    TITLE   = {Boolean Domains},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/finsub_1.html}})

@ARTICLE(ZF_MODEL.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Models and Satisfiability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/zf_model.html}})

@ARTICLE(ZF_COLLA.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {The Contraction Lemma},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/zf_colla.html}})

@ARTICLE(INCSP_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Axioms of Incidency},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/incsp_1.html}})

@ARTICLE(LATTICES.ABS,
    AUTHOR  = {\.Zukowski, Stanis{\l}aw},
    TITLE   = {Introduction to Lattice Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/lattices.html}})

@ARTICLE(PRE_TOPC.ABS,
    AUTHOR  = {Padlewska, Beata and Darmochwa{\l}, Agata},
    TITLE   = {Topological Spaces and Continuous Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/pre_topc.html}})

@ARTICLE(TOPS_1.ABS,
    AUTHOR  = {Wysocki, Miros{\l}aw and Darmochwa{\l}, Agata},
    TITLE   = {Subsets of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/tops_1.html}})

@ARTICLE(CONNSP_1.ABS,
    AUTHOR  = {Padlewska, Beata},
    TITLE   = {Connected Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/connsp_1.html}})

@ARTICLE(FUNCT_3.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Basic Functions and Operations on Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/funct_3.html}})

@ARTICLE(TOPS_2.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {Families of Subsets, Subspaces and Mappings in Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/tops_2.html}})

@ARTICLE(SEQ_1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Real Sequences and
Basic Operations on Them},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/seq_1.html}})

@ARTICLE(SEQ_2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Convergent Sequences and the Limit of Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/seq_2.html}})

@ARTICLE(ZFMODEL1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Properties of {ZF} Models},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/zfmodel1.html}})

@ARTICLE(RLVECT_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Vectors in Real Linear Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/rlvect_1.html}})

@ARTICLE(RLSUB_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Subspaces and Cosets of Subspaces in Real Linear Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/rlsub_1.html}})

@ARTICLE(QC_LANG1.ABS,
    AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
    TITLE   = {A First Order Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/qc_lang1.html}})

@ARTICLE(ORDERS_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Partially Ordered Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/orders_1.html}})

@ARTICLE(RECDEF_1.ABS,
    AUTHOR  = {Hryniewiecki, Krzysztof},
    TITLE   = {Recursive Definitions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/recdef_1.html}})

@ARTICLE(FUNCOP_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Binary Operations Applied to Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/funcop_1.html}})

@ARTICLE(VECTSP_1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech and Muzalewski, Micha{\l}},
    TITLE   = {Abelian Groups, Fields and Vector Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/vectsp_1.html}})

@ARTICLE(PARSP_1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech and Muzalewski, Micha{\l}},
    TITLE   = {Parallelity Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/parsp_1.html}})

@ARTICLE(SYMSP_1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech and Muzalewski, Micha{\l}},
    TITLE   = {Construction of a bilinear antisymmetric form
in symplectic vector space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/symsp_1.html}})

@ARTICLE(ORTSP_1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech and Muzalewski, Micha{\l}},
    TITLE   = {Construction of a bilinear symmetric form
in orthogonal vector space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/ortsp_1.html}})

@ARTICLE(SETWISEO.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Semilattice Operations on Finite Subsets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/setwiseo.html}})

@ARTICLE(COMPTS_1.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {Compact Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/compts_1.html}})

@ARTICLE(ORDERS_2.ABS,
    AUTHOR  = {Trybulec, Wojciech A. and Bancerek, Grzegorz},
    TITLE   = {Kuratowski - {Z}orn Lemma},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/orders_2.html}})

@ARTICLE(RLSUB_2.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Operations on Subspaces in Real Linear Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/rlsub_2.html}})

@ARTICLE(PROB_1.ABS,
    AUTHOR  = {N\c{e}dzusiak, Andrzej},
    TITLE   = { $\sigma$-Fields and Probability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/prob_1.html}})

@ARTICLE(CAT_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Introduction to Categories and Functors},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/cat_1.html}})

@ARTICLE(FUNCT_4.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {The Modification of a Function by a Function
and the Iteration of the Composition of a Function},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/funct_4.html}})

@ARTICLE(FUNCT_5.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Curried and Uncurried Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/funct_5.html}})

@ARTICLE(CARD_2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Cardinal Arithmetics},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/card_2.html}})

@ARTICLE(TREES_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Introduction to Trees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/trees_1.html}})

@ARTICLE(WELLSET1.ABS,
    AUTHOR  = {Nowak, Bogdan and Bia{\l}ecki, S{\l}awomir},
    TITLE   = {Zermelo's Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/wellset1.html}})

@ARTICLE(REALSET1.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Group and Field Definitions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/realset1.html}})

@ARTICLE(EQREL_1.ABS,
    AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
    TITLE   = {Equivalence Relations and Classes of Abstraction},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/eqrel_1.html}})

@ARTICLE(QC_LANG2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Connectives and Subformulae of the First Order Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/qc_lang2.html}})

@ARTICLE(QC_LANG3.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw and Bancerek, Grzegorz},
    TITLE   = {Variables in Formulae of the First Order Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/qc_lang3.html}})

@ARTICLE(SEQM_3.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Monotone Real Sequences. {S}ubsequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/seqm_3.html}})

@ARTICLE(SEQ_4.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Convergent Real Sequences.
{U}pper and Lower Bound of Sets of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/seq_4.html}})

@ARTICLE(MIDSP_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Midpoint algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/midsp_1.html}})

@ARTICLE(QMAX_1.ABS,
    AUTHOR  = {Sadowski, Pawe{\l} and Trybulec, Andrzej and Raczkowski, Konrad},
    TITLE   = {The Fundamental Logic Structure in Quantum Mechanics},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1989},
    VOLUME  = {1},
    NOTE    = {\url{http://mizar.org/JFM/Vol1/qmax_1.html}})

@ARTICLE(FRAENKEL.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Function Domains and {F}r{\ae}nkel Operator},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/fraenkel.html}})

@ARTICLE(INT_1.ABS,
    AUTHOR  = {Trybulec, Micha{\l} J.},
    TITLE   = {Integers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/int_1.html}})

@ARTICLE(REAL_2.ABS,
    AUTHOR  = {Kondracki, Andrzej},
    TITLE   = {Equalities and Inequalities in Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/real_2.html}})

@ARTICLE(COMPLEX1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {The Complex Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/complex1.html}})

@ARTICLE(FINSEQ_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Finite Sequences and
Tuples of Elements of a Non-empty Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/finseq_2.html}})

@ARTICLE(PARSP_2.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech},
    TITLE   = {Fano-{D}esargues Parallelity Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/parsp_2.html}})

@ARTICLE(FUNCSDOM.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Real Functions Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/funcsdom.html}})

@ARTICLE(CLASSES1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Tarski's Classes and Ranks},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/classes1.html}})

@ARTICLE(FINSEQ_3.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Non-contiguous Substrings and
One-to-one Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/finseq_3.html}})

@ARTICLE(FINSEQ_4.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Pigeon Hole Principle},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/finseq_4.html}})

@ARTICLE(RLVECT_2.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Linear Combinations in Real Linear Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rlvect_2.html}})

@ARTICLE(CARD_3.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {K\"onig's Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/card_3.html}})

@ARTICLE(CLASSES2.ABS,
    AUTHOR  = {Nowak, Bogdan and Bancerek, Grzegorz},
    TITLE   = {Universal Classes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/classes2.html}})

@ARTICLE(ANALOAF.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Analytical Ordered Affine Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/analoaf.html}})

@ARTICLE(METRIC_1.ABS,
    AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam and Startek, Mariusz},
    TITLE   = {Metric Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/metric_1.html}})

@ARTICLE(DIRAF.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Ordered Affine Spaces Defined in Terms of Directed Parallelity --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/diraf.html}})

@ARTICLE(AFF_1.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Parallelity and Lines in Affine Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/aff_1.html}})

@ARTICLE(AFF_2.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Classical Configurations in Affine Planes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/aff_2.html}})

@ARTICLE(AFF_3.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Affine Localizations of {D}esargues {A}xiom},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/aff_3.html}})

@ARTICLE(FINSEQOP.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Binary Operations Applied to Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/finseqop.html}})

@ARTICLE(FINSOP_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Binary Operations on Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/finsop_1.html}})

@ARTICLE(SETWOP_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Semigroup Operations on Finite Subsets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/setwop_2.html}})

@ARTICLE(COLLSP.ABS,
    AUTHOR  = {Skaba, Wojciech},
    TITLE   = {The Collinearity Structure},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/collsp.html}})

@ARTICLE(RVSUM_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {The Sum and Product of Finite Sequences of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rvsum_1.html}})

@ARTICLE(CQC_LANG.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {A Classical First Order Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/cqc_lang.html}})

@ARTICLE(PASCH.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof and Pra\.zmowska, Ma{\l}gorzata},
    TITLE   = {Classical and Non-classical {P}asch Configurations
in Ordered Affine Planes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/pasch.html}})

@ARTICLE(REAL_LAT.ABS,
    AUTHOR  = {Chmur, Marek},
    TITLE   = {The Lattice of Real Numbers.
{T}he Lattice of Real Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/real_lat.html}})

@ARTICLE(TDGROUP.ABS,
    AUTHOR  = {Lewandowski, Grzegorz and Pra\.zmowski, Krzysztof},
    TITLE   = {A Construction of an Abstract Space of Congruence of Vectors},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/tdgroup.html}})

@ARTICLE(CQC_THE1.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {A First-Order Predicate Calculus},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/cqc_the1.html}})

@ARTICLE(PARTFUN2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Partial Functions from a Domain to a Domain},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/partfun2.html}})

@ARTICLE(RFUNCT_1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Partial Functions from a Domain to the Set of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rfunct_1.html}})

@ARTICLE(ORDINAL4.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Increasing and Continuous Ordinal Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/ordinal4.html}})

@ARTICLE(TRANSGEO.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Transformations in Affine Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/transgeo.html}})

@ARTICLE(CAT_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Subcategories and Products of Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/cat_2.html}})

@ARTICLE(MARGREL1.ABS,
    AUTHOR  = {Woronowicz, Edmund},
    TITLE   = {Many-Argument Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/margrel1.html}})

@ARTICLE(VALUAT_1.ABS,
    AUTHOR  = {Woronowicz, Edmund},
    TITLE   = {Interpretation and Satisfiability in the First Order Logic},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/valuat_1.html}})

@ARTICLE(PROB_2.ABS,
    AUTHOR  = {N\c{e}dzusiak, Andrzej},
    TITLE   = {Probability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/prob_2.html}})

@ARTICLE(TRANSLAC.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Translations in Affine Planes },
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/translac.html}})

@ARTICLE(RPR_1.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Introduction to Probability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rpr_1.html}})

@ARTICLE(ANPROJ_1.ABS,
    AUTHOR  = {Leo\'nczuk, Wojciech and Pra\.zmowski, Krzysztof},
    TITLE   = {A Construction of Analytical Projective Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/anproj_1.html}})

@ARTICLE(ANPROJ_2.ABS,
    AUTHOR  = {Leo\'nczuk, Wojciech and Pra\.zmowski, Krzysztof},
    TITLE   = {Projective Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/anproj_2.html}})

@ARTICLE(RCOMP_1.ABS,
    AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
    TITLE   = {Topological Properties of Subsets in Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rcomp_1.html}})

@ARTICLE(RFUNCT_2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Properties of Real Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rfunct_2.html}})

@ARTICLE(FCONT_1.ABS,
    AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
    TITLE   = {Real Function Continuity},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/fcont_1.html}})

@ARTICLE(FCONT_2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
    TITLE   = {Real Function Uniform Continuity},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/fcont_2.html}})

@ARTICLE(FDIFF_1.ABS,
    AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
    TITLE   = {Real Function Differentiability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/fdiff_1.html}})

@ARTICLE(ROLLE.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad and Sadowski, Pawe{\l}},
    TITLE   = {Average Value Theorems for Real Functions of One Variable},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rolle.html}})

@ARTICLE(VECTSP_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Construction of Rings and Left-, Right-, and Bi-Modules over a Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_2.html}})

@ARTICLE(REALSET2.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Properties of Fields},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/realset2.html}})

@ARTICLE(FILTER_0.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Filters --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/filter_0.html}})

@ARTICLE(GROUP_1.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Groups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/group_1.html}})

@ARTICLE(INT_2.ABS,
    AUTHOR  = {Kwiatek, Rafa{\l} and Zwara, Grzegorz},
    TITLE   = {The Divisibility of Integers and Integer Relatively Primes   },
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/int_2.html}})

@ARTICLE(ALGSTR_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {From Loops to Abelian Multiplicative Groups with Zero},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/algstr_1.html}})

@ARTICLE(RAT_1.ABS,
    AUTHOR  = {Kondracki, Andrzej},
    TITLE   = {Basic Properties of Rational Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rat_1.html}})

@ARTICLE(RLVECT_3.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Basis of Real Linear Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rlvect_3.html}})

@ARTICLE(VECTSP_3.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Finite Sums of Vectors in Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_3.html}})

@ARTICLE(GROUP_2.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Subgroup and Cosets of Subgroups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/group_2.html}})

@ARTICLE(VECTSP_4.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Subspaces and Cosets of Subspaces in Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_4.html}})

@ARTICLE(VECTSP_5.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Operations on Subspaces in Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_5.html}})

@ARTICLE(VECTSP_6.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Linear Combinations in Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_6.html}})

@ARTICLE(VECTSP_7.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Basis of Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/vectsp_7.html}})

@ARTICLE(NEWTON.ABS,
    AUTHOR  = {Kwiatek, Rafa{\l}},
    TITLE   = {Factorial and {N}ewton Coefficients},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/newton.html}})

@ARTICLE(ANALMETR.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Analytical Metric Affine Spaces
and Planes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/analmetr.html}})

@ARTICLE(NET_1.ABS,
    AUTHOR  = {Korczy\'nski, Waldemar},
    TITLE   = {Some Elementary Notions of the Theory of {P}etri Nets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/net_1.html}})

@ARTICLE(GROUP_3.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Classes of Conjugation. {N}ormal Subgroups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/group_3.html}})

@ARTICLE(ZF_LANG1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Replacing of Variables in Formulas of {ZF} Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/zf_lang1.html}})

@ARTICLE(ZF_REFLE.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {The Reflection Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/zf_refle.html}})

@ARTICLE(LATTICE2.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Finite Join and Finite Meet, and Dual Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/lattice2.html}})

@ARTICLE(ZFREFLE1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Consequences of the Reflection Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/zfrefle1.html}})

@ARTICLE(PROJDES1.ABS,
    AUTHOR  = {Kusak, Eugeniusz},
    TITLE   = {Desargues Theorem In Projective 3-Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/projdes1.html}})

@ARTICLE(LIMFUNC1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {The Limit of a Real Function at Infinity},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/limfunc1.html}})

@ARTICLE(LIMFUNC2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {The One-Side Limits of a Real Function at a Point},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/limfunc2.html}})

@ARTICLE(GROUP_4.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Lattice of Subgroups of a Group. {F}rattini Subgroup},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/group_4.html}})

@ARTICLE(CARD_4.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Countable Sets and {H}essenberg's Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/card_4.html}})

@ARTICLE(LIMFUNC3.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {The Limit of a Real Function at a Point},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/limfunc3.html}})

@ARTICLE(LIMFUNC4.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {The Limit of a Composition of Real Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/limfunc4.html}})

@ARTICLE(CONNSP_2.ABS,
    AUTHOR  = {Padlewska, Beata},
    TITLE   = {Locally Connected Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/connsp_2.html}})

@ARTICLE(NORMSP_1.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Real Normed Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/normsp_1.html}})

@ARTICLE(ALGSEQ_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
    TITLE   = {Construction of Finite Sequence over Ring and Left-, Right-, and Bi-Modules
over a Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/algseq_1.html}})

@ARTICLE(TOLER_1.ABS,
    AUTHOR  = {Hryniewiecki, Krzysztof},
    TITLE   = {Relations of Tolerance},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/toler_1.html}})

@ARTICLE(SCHEME1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Schemes of Existence of Some Types of Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/scheme1.html}})

@ARTICLE(PREPOWER.ABS,
    AUTHOR  = {Raczkowski, Konrad},
    TITLE   = {Integer and Rational Exponents},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/prepower.html}})

@ARTICLE(HOMOTHET.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Homotheties and Shears in Affine Planes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/homothet.html}})

@ARTICLE(AFVECT0.ABS,
    AUTHOR  = {Lewandowski, Grzegorz and Pra\.zmowski, Krzysztof and Lewandowska, Bo\.zena},
    TITLE   = {Directed Geometrical Bundles and Their Analytical Representation},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/afvect0.html}})

@ARTICLE(ZFMODEL2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Definable Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/zfmodel2.html}})

@ARTICLE(LUKASI_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Darmochwa{\l}, Agata and Trybulec, Andrzej},
    TITLE   = {Propositional Calculus},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/lukasi_1.html}})

@ARTICLE(COMPLSP1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw and Trybulec, Andrzej},
    TITLE   = {Complex Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/complsp1.html}})

@ARTICLE(REALSET3.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Several Properties of Fields. {F}ield Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/realset3.html}})

@ARTICLE(SUPINF_1.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Infimum and Supremum of the Set of Real Numbers.
{M}easure Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/supinf_1.html}})

@ARTICLE(SUPINF_2.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Series of Positive Real Numbers.
{M}easure Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/supinf_2.html}})

@ARTICLE(ALGSTR_2.ABS,
    AUTHOR  = {Skaba, Wojciech and Muzalewski, Micha{\l}},
    TITLE   = {From Double Loops to Fields},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/algstr_2.html}})

@ARTICLE(METRIC_3.ABS,
    AUTHOR  = {Kanas, Stanis{\l}awa and Stankiewicz, Jan},
    TITLE   = {Metrics in {C}artesian Product},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/metric_3.html}})

@ARTICLE(SUB_METR.ABS,
    AUTHOR  = {Lecko, Adam and Startek, Mariusz},
    TITLE   = {Submetric Spaces --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/sub_metr.html}})

@ARTICLE(METRIC_2.ABS,
    AUTHOR  = {Lecko, Adam and Startek, Mariusz},
    TITLE   = {On Pseudometric Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/metric_2.html}})

@ARTICLE(POWER.ABS,
    AUTHOR  = {Raczkowski, Konrad and N\c{e}dzusiak, Andrzej},
    TITLE   = {Real Exponents and Logarithms},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/power.html}})

@ARTICLE(HESSENBE.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech},
    TITLE   = {Hessenberg Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/hessenbe.html}})

@ARTICLE(MULTOP_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Three-Argument Operations and Four-Argument Operations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/multop_1.html}})

@ARTICLE(INCPROJ.ABS,
    AUTHOR  = {Leo\'nczuk, Wojciech and Pra\.zmowski, Krzysztof},
    TITLE   = {Incidence Projective Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/incproj.html}})

@ARTICLE(AFVECT01.ABS,
    AUTHOR  = {Konstanta, Barbara and Kowieska, Urszula and Lewandowski, Grzegorz and Pra\.zmowski, Krzysztof},
    TITLE   = {One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/afvect01.html}})

@ARTICLE(NORMFORM.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Algebra of Normal Forms},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/normform.html}})

@ARTICLE(O_RING_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
    TITLE   = {Ordered Rings - Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/o_ring_1.html}})

@ARTICLE(O_RING_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
    TITLE   = {Ordered Rings - Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/o_ring_2.html}})

@ARTICLE(O_RING_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
    TITLE   = {Ordered Rings - Part {III}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/o_ring_3.html}})

@ARTICLE(MCART_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = { $N$-Tuples and {C}artesian Products for $n=5$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mcart_2.html}})

@ARTICLE(MCART_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = { $N$-Tuples and {C}artesian Products for $n=6$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mcart_3.html}})

@ARTICLE(MCART_4.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = { $N$-Tuples and {C}artesian Products for $n=7$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mcart_4.html}})

@ARTICLE(MCART_5.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = { $N$-Tuples and {C}artesian Products for $n=8$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mcart_5.html}})

@ARTICLE(MCART_6.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = { $N$-Tuples and {C}artesian Products for $n=9$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mcart_6.html}})

@ARTICLE(ALGSTR_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Ternary Fields},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/algstr_3.html}})

@ARTICLE(MEASURE1.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {The $\sigma$-additive Measure Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/measure1.html}})

@ARTICLE(PROJRED1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech},
    TITLE   = {Incidence Projective Space (a reduction theorem in a plane)},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/projred1.html}})

@ARTICLE(MOD_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Groups, Rings, Left- and Right-Modules},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/mod_1.html}})

@ARTICLE(LMOD_4.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Linear Combinations in Left Module over Associative Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/lmod_4.html}})

@ARTICLE(LMOD_5.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Linear Independence in Left Module over Domain},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/lmod_5.html}})

@ARTICLE(RMOD_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Finite Sums of Vectors in Right Module over Associative Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rmod_1.html}})

@ARTICLE(RMOD_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Submodules and Cosets of Submodules in Right Module over Associative Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rmod_2.html}})

@ARTICLE(RMOD_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Operations on Submodules in Right Module over Associative Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rmod_3.html}})

@ARTICLE(RMOD_4.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Linear Combinations in Right Module over Associative Ring},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rmod_4.html}})

@ARTICLE(RMOD_5.ABS,
    AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
    TITLE   = {Linear Independence in Right Module over Domain},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/rmod_5.html}})

@ARTICLE(PROCAL_1.ABS,
    AUTHOR  = {Popio{\l}ek, Jan and Trybulec, Andrzej},
    TITLE   = {Calculus of Propositions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/procal_1.html}})

@ARTICLE(CQC_THE2.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {Calculus of Quantifiers. {D}eduction Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/cqc_the2.html}})

@ARTICLE(GEOMTRAP.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {A Construction of Analytical Ordered Trapezium Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/geomtrap.html}})

@ARTICLE(PROJRED2.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Leo\'nczuk, Wojciech and Pra\.zmowski, Krzysztof},
    TITLE   = {On Projections in Projective Planes --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/projred2.html}})

@ARTICLE(CONAFFM.ABS,
    AUTHOR  = {\'Swierzy\'nska, Jolanta and \'Swierzy\'nski, Bogdan},
    TITLE   = {Metric-Affine Configurations in Metric Affine Planes --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/conaffm.html}})

@ARTICLE(CONMETR.ABS,
    AUTHOR  = {\'Swierzy\'nska, Jolanta and \'Swierzy\'nski, Bogdan},
    TITLE   = {Metric-Affine Configurations in Metric Affine Planes --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/conmetr.html}})

@ARTICLE(PAPDESAF.ABS,
    AUTHOR  = {Pra\.zmowski, Krzysztof},
    TITLE   = {Fanoian, {P}appian and {D}esarguesian Affine Spaces },
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/papdesaf.html}})

@ARTICLE(PARDEPAP.ABS,
    AUTHOR  = {Pra\.zmowski, Krzysztof and Radziszewski, Krzysztof},
    TITLE   = {Elementary Variants of Affine Configurational Theorems},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/pardepap.html}})

@ARTICLE(SEMI_AF1.ABS,
    AUTHOR  = {Kusak, Eugeniusz and Radziszewski, Krzysztof},
    TITLE   = {Semi-Affine Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/semi_af1.html}})

@ARTICLE(AFF_4.ABS,
    AUTHOR  = {Leo\'nczuk, Wojciech and Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Planes in Affine Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/aff_4.html}})

@ARTICLE(GRAPH_1.ABS,
    AUTHOR  = {Hryniewiecki, Krzysztof},
    TITLE   = {Graphs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/graph_1.html}})

@ARTICLE(ZF_FUND1.ABS,
    AUTHOR  = {Kondracki, Andrzej},
    TITLE   = {Mostowski's Fundamental Operations --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/zf_fund1.html}})

@ARTICLE(AFPROJ.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {A Projective Closure and Projective Horizon of an Affine Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/afproj.html}})

@ARTICLE(SCHEMS_1.ABS,
    AUTHOR  = {Czuba, Stanis{\l}aw T.},
    TITLE   = {Schemes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1990},
    VOLUME  = {2},
    NOTE    = {\url{http://mizar.org/JFM/Vol2/schems_1.html}})

@ARTICLE(HEYTING1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Algebra of Normal Forms Is a {H}eyting Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/heyting1.html}})

@ARTICLE(TREES_2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {K\"onig's {L}emma},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/trees_2.html}})

@ARTICLE(FCONT_3.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Monotonic and Continuous Real Function},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/fcont_3.html}})

@ARTICLE(FDIFF_2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
    TITLE   = {Real Function Differentiability --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/fdiff_2.html}})

@ARTICLE(PRELAMB.ABS,
    AUTHOR  = {Zielonka, Wojciech},
    TITLE   = {Preliminaries to the {L}ambek Calculus},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/prelamb.html}})

@ARTICLE(OPPCAT_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Opposite Categories and Contravariant Functors},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/oppcat_1.html}})

@ARTICLE(ZF_FUND2.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Kondracki, Andrzej},
    TITLE   = {Mostowski's Fundamental Operations --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/zf_fund2.html}})

@ARTICLE(EUCLMETR.ABS,
    AUTHOR  = {Oryszczyszyn, Henryk and Pra\.zmowski, Krzysztof},
    TITLE   = {Fundamental Types of Metric Affine Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/euclmetr.html}})

@ARTICLE(FILTER_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Filters - Part {II}.
{Q}uotient Lattices Modulo Filters and
Direct Product of Two Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/filter_1.html}})

@ARTICLE(CONMETR1.ABS,
    AUTHOR  = {\'Swierzy\'nska, Jolanta and \'Swierzy\'nski, Bogdan},
    TITLE   = {Shear Theorems and Their Role in Affine Geometry},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/conmetr1.html}})

@ARTICLE(SERIES_1.ABS,
    AUTHOR  = {Raczkowski, Konrad and N\c{e}dzusiak, Andrzej},
    TITLE   = {Serieses},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/series_1.html}})

@ARTICLE(NAT_LAT.ABS,
    AUTHOR  = {Chmur, Marek},
    TITLE   = {The Lattice of Natural Numbers and The Sublattice of it.
{T}he Set of Prime Numbers.},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/nat_lat.html}})

@ARTICLE(GROUP_5.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Commutator and Center of a Group},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/group_5.html}})

@ARTICLE(NATTRA_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Natural transformations.
{D}iscrete categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/nattra_1.html}})

@ARTICLE(MATRIX_1.ABS,
    AUTHOR  = {Jankowska, Katarzyna},
    TITLE   = {Matrices. {A}belian Group of Matrices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/matrix_1.html}})

@ARTICLE(PCOMPS_1.ABS,
    AUTHOR  = {Borys, Leszek},
    TITLE   = {Paracompact and Metrizable Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/pcomps_1.html}})

@ARTICLE(MIDSP_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Atlas of Midpoint Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/midsp_2.html}})

@ARTICLE(MEASURE2.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Several Properties of the $\sigma$-additive Measure},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/measure2.html}})

@ARTICLE(METRIC_4.ABS,
    AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam},
    TITLE   = {Metrics in the {C}artesian Product --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/metric_4.html}})

@ARTICLE(ALI2.ABS,
    AUTHOR  = {de~la~Cruz, Alicia},
    TITLE   = {Fix Point Theorem for Compact Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/ali2.html}})

@ARTICLE(QUIN_1.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Quadratic Inequalities},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/quin_1.html}})

@ARTICLE(BHSP_1.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Introduction to {B}anach and {H}ilbert Spaces --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/bhsp_1.html}})

@ARTICLE(BHSP_2.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Introduction to {B}anach and {H}ilbert Spaces --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/bhsp_2.html}})

@ARTICLE(BHSP_3.ABS,
    AUTHOR  = {Popio{\l}ek, Jan},
    TITLE   = {Introduction to {B}anach and {H}ilbert Spaces --- Part {III}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/bhsp_3.html}})

@ARTICLE(ENS_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Category {E}ns},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/ens_1.html}})

@ARTICLE(BORSUK_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {A {B}orsuk Theorem on Homotopy Types},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/borsuk_1.html}})

@ARTICLE(FUNCT_6.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Cartesian Product of Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/funct_6.html}})

@ARTICLE(MODAL_1.ABS,
    AUTHOR  = {de~la~Cruz, Alicia},
    TITLE   = {Introduction to Modal Propositional Logic},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/modal_1.html}})

@ARTICLE(TBSP_1.ABS,
    AUTHOR  = {de~la~Cruz, Alicia},
    TITLE   = {Totally Bounded Metric Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/tbsp_1.html}})

@ARTICLE(GRCAT_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Categories of Groups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/grcat_1.html}})

@ARTICLE(GROUP_6.ABS,
    AUTHOR  = {Trybulec, Wojciech A. and Trybulec, Micha{\l} J.},
    TITLE   = {Homomorphisms and Isomorphisms of Groups. {Q}uotient Group},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/group_6.html}})

@ARTICLE(MOD_2.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Rings and Modules --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/mod_2.html}})

@ARTICLE(MOD_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Free Modules},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/mod_3.html}})

@ARTICLE(ANALORT.ABS,
    AUTHOR  = {Zajkowski, Jaros{\l}aw},
    TITLE   = {Oriented Metric-Affine Plane --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/analort.html}})

@ARTICLE(EUCLID.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata},
    TITLE   = {The {E}uclidean Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/euclid.html}})

@ARTICLE(TOPMETR.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
    TITLE   = {Metric Spaces as Topological Spaces --- Fundamental Concepts},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/topmetr.html}})

@ARTICLE(HEINE.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
    TITLE   = {Heine--{B}orel's Covering Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/heine.html}})

@ARTICLE(TOPMETR2.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Darmochwa{\l}, Agata},
    TITLE   = {Some Facts about Union of Two Functions and Continuity of Union
    of Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/topmetr2.html}})

@ARTICLE(TOPREAL1.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
    TITLE   = {The Topological Space ${\calE}^2_{\rmT}$.
{A}rcs, Line Segments and Special Polygonal Arcs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/topreal1.html}})

@ARTICLE(GR_CY_1.ABS,
    AUTHOR  = {Surowik, Dariusz},
    TITLE   = {Cyclic Groups and Some of Their Properties --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/gr_cy_1.html}})

@ARTICLE(ISOCAT_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Isomorphisms of Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/isocat_1.html}})

@ARTICLE(CQC_SIM1.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata and Trybulec, Andrzej},
    TITLE   = {Similarity of Formulae},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/cqc_sim1.html}})

@ARTICLE(RINGCAT1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Category of Rings},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/ringcat1.html}})

@ARTICLE(MODCAT_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Category of Left Modules},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/modcat_1.html}})

@ARTICLE(FDIFF_3.ABS,
    AUTHOR  = {Burakowska, Ewa and Madras, Beata},
    TITLE   = {Real Function One-Side Differentiability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/fdiff_3.html}})

@ARTICLE(METRIC_6.ABS,
    AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam},
    TITLE   = {Sequences in Metric Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/metric_6.html}})

@ARTICLE(TOPREAL2.ABS,
    AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
    TITLE   = {The Topological Space ${\calE}^2_{\rmT}$.
{S}imple Closed Curves},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1991},
    VOLUME  = {3},
    NOTE    = {\url{http://mizar.org/JFM/Vol3/topreal2.html}})

@ARTICLE(TSEP_1.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Separated and Weakly Separated Subspaces of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tsep_1.html}})

@ARTICLE(SYSREL.ABS,
    AUTHOR  = {Korczy\'nski, Waldemar},
    TITLE   = {Some Properties of Binary Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/sysrel.html}})

@ARTICLE(FF_SIEC.ABS,
    AUTHOR  = {Korczy\'nski, Waldemar},
    TITLE   = {Definitions of {P}etri Net. {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/ff_siec.html}})

@ARTICLE(E_SIEC.ABS,
    AUTHOR  = {Korczy\'nski, Waldemar},
    TITLE   = {Definitions of {P}etri Net. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/e_siec.html}})

@ARTICLE(S_SIEC.ABS,
    AUTHOR  = {Korczy\'nski, Waldemar},
    TITLE   = {Definitions of {P}etri Net. {P}art {III}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/s_siec.html}})

@ARTICLE(L_HOSPIT.ABS,
    AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
    TITLE   = {The de l'{H}ospital Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/l_hospit.html}})

@ARTICLE(COMMACAT.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Darmochwa{\l}, Agata},
    TITLE   = {Comma Category},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/commacat.html}})

@ARTICLE(LANG1.ABS,
    AUTHOR  = {Carlson, Patricia L. and Bancerek, Grzegorz},
    TITLE   = {Context-Free Grammar --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/lang1.html}})

@ARTICLE(MEASURE3.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Completeness of the $\sigma$-Additive Measure.
{M}easure Theory},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/measure3.html}})

@ARTICLE(BHSP_4.ABS,
    AUTHOR  = {Kraszewska, El\.zbieta and Popio{\l}ek, Jan},
    TITLE   = {Series in {B}anach and {H}ilbert Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/bhsp_4.html}})

@ARTICLE(CAT_3.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Products and Coproducts in Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/cat_3.html}})

@ARTICLE(MATRIX_2.ABS,
    AUTHOR  = {Jankowska, Katarzyna},
    TITLE   = {Transpose Matrices and Groups of Permutations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/matrix_2.html}})

@ARTICLE(LATTICE3.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Complete Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/lattice3.html}})

@ARTICLE(TMAP_1.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Continuity of Mappings over the Union of Subspaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tmap_1.html}})

@ARTICLE(SEQFUNC.ABS,
    AUTHOR  = {Perkowska, Beata},
    TITLE   = {Functional Sequence from a Domain to a Domain},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/seqfunc.html}})

@ARTICLE(MIDSP_3.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Reper Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/midsp_3.html}})

@ARTICLE(GR_CY_2.ABS,
    AUTHOR  = {Surowik, Dariusz},
    TITLE   = {Isomorphisms of Cyclic Groups.
{S}ome Properties of Cyclic Groups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/gr_cy_2.html}})

@ARTICLE(ISOCAT_2.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Some Isomorphisms Between Functor Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/isocat_2.html}})

@ARTICLE(TDLAT_1.ABS,
    AUTHOR  = {Watanabe, Toshihiko},
    TITLE   = {The Lattice of Domains of a Topological Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tdlat_1.html}})

@ARTICLE(LMOD_6.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Submodules},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/lmod_6.html}})

@ARTICLE(DIRORT.ABS,
    AUTHOR  = {Zajkowski, Jaros{\l}aw},
    TITLE   = {Oriented Metric-Affine Plane --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/dirort.html}})

@ARTICLE(MOD_4.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Opposite Rings, Modules and Their Morphisms},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/mod_4.html}})

@ARTICLE(MEASURE4.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Properties of {C}aratheodor's Measure},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/measure4.html}})

@ARTICLE(TDLAT_2.ABS,
    AUTHOR  = {Karno, Zbigniew and Watanabe, Toshihiko},
    TITLE   = {Completeness of the Lattices of Domains 
of a Topological Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tdlat_2.html}})

@ARTICLE(PCOMPS_2.ABS,
    AUTHOR  = {Borys, Leszek},
    TITLE   = {On Paracompactness of Metrizable Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/pcomps_2.html}})

@ARTICLE(TREAL_1.ABS,
    AUTHOR  = {Watanabe, Toshihiko},
    TITLE   = {The {B}rouwer Fixed Point Theorem
for Intervals},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/treal_1.html}})

@ARTICLE(CARD_5.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {On Powers of Cardinals},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/card_5.html}})

@ARTICLE(TOPREAL3.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Kotowicz, Jaros{\l}aw},
    TITLE   = {Basic Properties of Connecting Points with Line Segments in ${\calE}^2_{\rmT}$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/topreal3.html}})

@ARTICLE(TOPREAL4.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Kotowicz, Jaros{\l}aw},
    TITLE   = {Connectedness Conditions Using Polygonal Arcs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/topreal4.html}})

@ARTICLE(GOBOARD1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
    TITLE   = {Introduction to {G}o-{B}oard --- Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/goboard1.html}})

@ARTICLE(GOBOARD2.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
    TITLE   = {Introduction to {G}o-{B}oard --- Part {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/goboard2.html}})

@ARTICLE(GOBOARD3.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
    TITLE   = {Properties of {G}o-{B}oard --- Part {III}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/goboard3.html}})

@ARTICLE(GOBOARD4.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
    TITLE   = {Go-{B}oard Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/goboard4.html}})

@ARTICLE(JORDAN1.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Kotowicz, Jaros{\l}aw},
    TITLE   = {The {J}ordan's Property for Certain Subsets of the Plane},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/jordan1.html}})

@ARTICLE(TDLAT_3.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {The Lattice of Domains of an Extremally Disconnected Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tdlat_3.html}})

@ARTICLE(AMI_1.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {A Mathematical Model of {CPU}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/ami_1.html}})

@ARTICLE(CAT_4.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Cartesian Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/cat_4.html}})

@ARTICLE(VFUNCT_1.ABS,
    AUTHOR  = {Yamazaki, Hiroshi and Shidama, Yasunari},
    TITLE   = {Algebra of Vector Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/vfunct_1.html}})

@ARTICLE(TSEP_2.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {On a Duality Between Weakly Separated 
Subspaces of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/tsep_2.html}})

@ARTICLE(PETRI.ABS,
    AUTHOR  = {Kawamoto, Pauline N. and Fuwa, Yasushi and Nakamura, Yatsuka},
    TITLE   = {Basic {P}etri Net Concepts},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/petri.html}})

@ARTICLE(FIN_TOPO.ABS,
    AUTHOR  = {Imura, Hiroshi and Eguchi, Masayoshi},
    TITLE   = {Finite Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/fin_topo.html}})

@ARTICLE(TREES_3.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Sets and Functions of Trees and Joining Operations of Trees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/trees_3.html}})

@ARTICLE(FVSUM_1.ABS,
    AUTHOR  = {Zawadzka, Katarzyna},
    TITLE   = {Sum and Product of Finite Sequences of Elements of a Field},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/fvsum_1.html}})

@ARTICLE(AMI_2.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {On a Mathematical Model of Programs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/ami_2.html}})

@ARTICLE(UNIALG_1.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Madras, Beata and Korolkiewicz, Ma{\l}gorzata},
    TITLE   = {Basic Notation of Universal Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/unialg_1.html}})

@ARTICLE(COH_SP.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
    TITLE   = {Coherent Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/coh_sp.html}})

@ARTICLE(MONOID_0.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Monoids},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/monoid_0.html}})

@ARTICLE(MONOID_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Monoid of Multisets and Subsets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/monoid_1.html}})

@ARTICLE(PRVECT_1.ABS,
    AUTHOR  = {Lango, Anna and Bancerek, Grzegorz},
    TITLE   = {Product of Families of Groups and Vector Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1992},
    VOLUME  = {4},
    NOTE    = {\url{http://mizar.org/JFM/Vol4/prvect_1.html}})

@ARTICLE(MEASURE5.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Properties of the Intervals of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/measure5.html}})

@ARTICLE(RLVECT_4.ABS,
    AUTHOR  = {Trybulec, Wojciech A.},
    TITLE   = {Subspaces of Real Linear Space Generated by One, Two, or Three Vectors 
and Their Cosets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/rlvect_4.html}})

@ARTICLE(LMOD_7.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Domains of Submodules, Join and Meet 
of Finite Sequences of Submodules 
and Quotient Modules},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/lmod_7.html}})

@ARTICLE(RFINSEQ.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw},
    TITLE   = {Functions and Finite Sequences of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/rfinseq.html}})

@ARTICLE(RFUNCT_3.ABS,
    AUTHOR  = {Kotowicz, Jaros{\l}aw and Sakai, Yuji},
    TITLE   = {Properties of Partial Functions from a Domain to the Set of Real Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/rfunct_3.html}})

@ARTICLE(TOPS_3.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Remarks on Special Subsets of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/tops_3.html}})

@ARTICLE(TEX_1.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {On Discrete and Almost Discrete Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/tex_1.html}})

@ARTICLE(MATRIX_3.ABS,
    AUTHOR  = {Zawadzka, Katarzyna},
    TITLE   = {The Product and the Determinant of Matrices with Entries in a Field},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/matrix_3.html}})

@ARTICLE(REARRAN1.ABS,
    AUTHOR  = {Sakai, Yuji and Kotowicz, Jaros{\l}aw},
    TITLE   = {Introduction to Theory of Rearrangement},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/rearran1.html}})

@ARTICLE(PBOOLE.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Many-sorted Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/pboole.html}})

@ARTICLE(UNIALG_2.ABS,
    AUTHOR  = {Burakowska, Ewa},
    TITLE   = {Subalgebras of the Universal Algebra. {L}attices of Subalgebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/unialg_2.html}})

@ARTICLE(HAHNBAN.ABS,
    AUTHOR  = {Nowak, Bogdan and Trybulec, Andrzej},
    TITLE   = {Hahn-{B}anach Theorem},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/hahnban.html}})

@ARTICLE(LATTICE4.ABS,
    AUTHOR  = {Kamie\'nska, Jolanta and Walijewski, Jaros{\l}aw Stanis{\l}aw},
    TITLE   = {Homomorphisms of Lattices,
Finite Join and Finite Meet},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/lattice4.html}})

@ARTICLE(OPENLATT.ABS,
    AUTHOR  = {Kamie\'nska, Jolanta},
    TITLE   = {Representation Theorem for {H}eyting Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/openlatt.html}})

@ARTICLE(LOPCLSET.ABS,
    AUTHOR  = {Walijewski, Jaros{\l}aw Stanis{\l}aw},
    TITLE   = {Representation Theorem for Boolean Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/lopclset.html}})

@ARTICLE(AMI_3.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
    TITLE   = {Some Remarks on the Simple Concrete Model of Computer},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/ami_3.html}})

@ARTICLE(AMI_4.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
    TITLE   = {Euclid's Algorithm},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/ami_4.html}})

@ARTICLE(SCM_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {Development of Terminology for {\bf SCM}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/scm_1.html}})

@ARTICLE(PRE_FF.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {Two Programs for {\bf {SCM}}. {P}art {I} - Preliminaries},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/pre_ff.html}})

@ARTICLE(FIB_FUSC.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {Two Programs for {\bf {SCM}}. {P}art {II} - Programs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/fib_fusc.html}})

@ARTICLE(TREES_4.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Joining of Decorated Trees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/trees_4.html}})

@ARTICLE(BINARITH.ABS,
    AUTHOR  = {Nishiyama, Takaya and Mizuhara, Yasuho},
    TITLE   = {Binary Arithmetics},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/binarith.html}})

@ARTICLE(BOOLMARK.ABS,
    AUTHOR  = {Kawamoto, Pauline N. and Fuwa, Yasushi and Nakamura, Yatsuka},
    TITLE   = {Basic Concepts for {P}etri Nets with Boolean Markings},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/boolmark.html}})

@ARTICLE(DTCONSTR.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {On Defining Functions on Trees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/dtconstr.html}})

@ARTICLE(PRALG_1.ABS,
    AUTHOR  = {Madras, Beata},
    TITLE   = {Product of Family of Universal Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/pralg_1.html}})

@ARTICLE(ALG_1.ABS,
    AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
    TITLE   = {Homomorphisms of Algebras. {Q}uotient Universal Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/alg_1.html}})

@ARTICLE(FREEALG.ABS,
    AUTHOR  = {Perkowska, Beata},
    TITLE   = {Free Universal Algebra Construction},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/freealg.html}})

@ARTICLE(COMSEQ_1.ABS,
    AUTHOR  = {Banachowicz, Agnieszka and Winnicka, Anna},
    TITLE   = {Complex Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/comseq_1.html}})

@ARTICLE(TEX_2.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Maximal Discrete Subspaces of Almost Discrete Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/tex_2.html}})

@ARTICLE(TEX_3.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {On Nowhere and Everywhere Dense Subspaces of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/tex_3.html}})

@ARTICLE(AMI_5.ABS,
    AUTHOR  = {Tanaka, Yasushi},
    TITLE   = {On the Decomposition of the States of {SCM}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/ami_5.html}})

@ARTICLE(BINTREE1.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {On Defining Functions on Binary Trees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/bintree1.html}})

@ARTICLE(SCM_COMP.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
    TITLE   = {A Compiler of Arithmetic Expressions for {SCM}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1993},
    VOLUME  = {5},
    NOTE    = {\url{http://mizar.org/JFM/Vol5/scm_comp.html}})

@ARTICLE(MEASURE6.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {Some Properties of the Intervals},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/measure6.html}})

@ARTICLE(BINARI_2.ABS,
    AUTHOR  = {Mizuhara, Yasuho and Nishiyama, Takaya},
    TITLE   = {Binary Arithmetics,
Addition and Subtraction of Integers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/binari_2.html}})

@ARTICLE(BOOLEALG.ABS,
    AUTHOR  = {Marasik, Agnieszka Julia},
    TITLE   = {Boolean Properties of Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/boolealg.html}})

@ARTICLE(MSUALG_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msualg_1.html}})

@ARTICLE(AUTGROUP.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {On the Group of Inner Automorphisms},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/autgroup.html}})

@ARTICLE(MSUALG_2.ABS,
    AUTHOR  = {Burakowska, Ewa},
    TITLE   = {Subalgebras of Many Sorted Algebra.
{L}attice of Subalgebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msualg_2.html}})

@ARTICLE(PRALG_2.ABS,
    AUTHOR  = {Madras, Beata},
    TITLE   = {Products of Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/pralg_2.html}})

@ARTICLE(MSUALG_3.ABS,
    AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
    TITLE   = {Homomorphisms of Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msualg_3.html}})

@ARTICLE(MSAFREE.ABS,
    AUTHOR  = {Perkowska, Beata},
    TITLE   = {Free Many Sorted Universal Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msafree.html}})

@ARTICLE(T_0TOPSP.ABS,
    AUTHOR  = {\.Zynel, Mariusz and Guzowski, Adam},
    TITLE   = {{\Tzero}\ Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/t_0topsp.html}})

@ARTICLE(MSUALG_4.ABS,
    AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
    TITLE   = {Many Sorted Quotient Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msualg_4.html}})

@ARTICLE(QUANTAL1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Quantales},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/quantal1.html}})

@ARTICLE(TOPRNS_1.ABS,
    AUTHOR  = {Sakowicz, Agnieszka and Gryko, Jaros{\l}aw and Grabowski, Adam},
    TITLE   = {Sequences in ${\calE}^{N}_{\rmT}$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/toprns_1.html}})

@ARTICLE(SPPOL_1.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Byli\'nski, Czes{\l}aw},
    TITLE   = {Extremal Properties of Vertices on Special Polygons, Part {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/sppol_1.html}})

@ARTICLE(RELOC.ABS,
    AUTHOR  = {Tanaka, Yasushi},
    TITLE   = {Relocatability},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/reloc.html}})

@ARTICLE(TEX_4.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Maximal Anti-Discrete Subspaces of Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/tex_4.html}})

@ARTICLE(TSP_1.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {On {K}olmogorov Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/tsp_1.html}})

@ARTICLE(TSP_2.ABS,
    AUTHOR  = {Karno, Zbigniew},
    TITLE   = {Maximal {K}olmogorov Subspaces of a Topological Space as {S}tone Retracts of the Ambient Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/tsp_2.html}})

@ARTICLE(PROJPL_1.ABS,
    AUTHOR  = {Muzalewski, Micha{\l}},
    TITLE   = {Projective Planes},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/projpl_1.html}})

@ARTICLE(SGRAPH1.ABS,
    AUTHOR  = {Toda, Yozo},
    TITLE   = {The Formalization of Simple Graphs},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/sgraph1.html}})

@ARTICLE(GRSOLV_1.ABS,
    AUTHOR  = {Zawadzka, Katarzyna},
    TITLE   = {Solvable Groups},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/grsolv_1.html}})

@ARTICLE(FILTER_2.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Ideals},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/filter_2.html}})

@ARTICLE(CAT_5.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Categorial Categories and Slice Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/cat_5.html}})

@ARTICLE(PRE_CIRC.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
    TITLE   = {Preliminaries to Circuits, {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/pre_circ.html}})

@ARTICLE(FSM_1.ABS,
    AUTHOR  = {Kaloper, Miroslava and Rudnicki, Piotr},
    TITLE   = {Minimization of Finite State Machines},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/fsm_1.html}})

@ARTICLE(TREES_9.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Subtrees},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/trees_9.html}})

@ARTICLE(MSATERM.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Terms Over Many Sorted Universal Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msaterm.html}})

@ARTICLE(DECOMP_1.ABS,
    AUTHOR  = {Przemski, Marian},
    TITLE   = {On the Decomposition of the Continuity},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/decomp_1.html}})

@ARTICLE(MSAFREE1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {A Scheme for Extensions of Homomorphisms of Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msafree1.html}})

@ARTICLE(MSUHOM_1.ABS,
    AUTHOR  = {Grabowski, Adam},
    TITLE   = {The Correspondence Between Homomorphisms of Universal Algebra 
 \& Many Sorted Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msuhom_1.html}})

@ARTICLE(MSAFREE2.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
    TITLE   = {Preliminaries to Circuits, {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/msafree2.html}})

@ARTICLE(AUTALG_1.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {On the Group of Automorphisms of Universal Algebra and
Many Sorted Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/autalg_1.html}})

@ARTICLE(CIRCUIT1.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
    TITLE   = {Introduction to Circuits, {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1994},
    VOLUME  = {6},
    NOTE    = {\url{http://mizar.org/JFM/Vol6/circuit1.html}})

@ARTICLE(CANTOR_1.ABS,
    AUTHOR  = {Shibakov, Alexander Yu. and Trybulec, Andrzej},
    TITLE   = {The {C}antor Set},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/cantor_1.html}})

@ARTICLE(CQC_THE3.ABS,
    AUTHOR  = {Okhotnikov, Oleg},
    TITLE   = {Logical Equivalence of Formulae},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/cqc_the3.html}})

@ARTICLE(FINSEQ_5.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Some Properties of Restrictions of Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/finseq_5.html}})

@ARTICLE(SPPOL_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw and Nakamura, Yatsuka},
    TITLE   = {Special Polygons},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/sppol_2.html}})

@ARTICLE(MEASURE7.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef},
    TITLE   = {The One-Dimensional {L}ebesgue Measure },
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/measure7.html}})

@ARTICLE(ALTCAT_1.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Categories without Uniqueness of {\rm cod} and {\rm dom}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/altcat_1.html}})

@ARTICLE(EXTENS_1.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {Extensions of Mappings on Generator Set},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/extens_1.html}})

@ARTICLE(CIRCUIT2.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
    TITLE   = {Introduction to Circuits, {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/circuit2.html}})

@ARTICLE(MBOOLEAN.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {Definitions and Basic Properties of Boolean and
Union of Many Sorted Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/mboolean.html}})

@ARTICLE(CIRCCOMB.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Bancerek, Grzegorz},
    TITLE   = {Combining of Circuits},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/circcomb.html}})

@ARTICLE(GRAPH_2.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr},
    TITLE   = {Vertex Sequences Induced by Chains},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/graph_2.html}})

@ARTICLE(VECTSP_8.ABS,
    AUTHOR  = {Iwaniuk, Andrzej},
    TITLE   = {On the Lattice of Subspaces of a Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/vectsp_8.html}})

@ARTICLE(LATSUBGR.ABS,
    AUTHOR  = {Ganczarski, Janusz},
    TITLE   = {On the Lattice of Subgroups of a Group},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/latsubgr.html}})

@ARTICLE(UNIALG_3.ABS,
    AUTHOR  = {Paszek, Miros{\l}aw Jan},
    TITLE   = {On the Lattice of Subalgebras of a Universal Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/unialg_3.html}})

@ARTICLE(FINSEQ_6.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {On the Decomposition of Finite Sequences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/finseq_6.html}})

@ARTICLE(GOBOARD5.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {Decomposing a {G}o-{B}oard into Cells},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/goboard5.html}})

@ARTICLE(INDEX_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Indexed Category},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/index_1.html}})

@ARTICLE(MATRLIN.ABS,
    AUTHOR  = {Milewski, Robert},
    TITLE   = {Associated Matrix of Linear Map},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/matrlin.html}})

@ARTICLE(GOBOARD6.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {On the Geometry of a {G}o-{B}oard},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/goboard6.html}})

@ARTICLE(WEIERSTR.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef and Nakamura, Yatsuka},
    TITLE   = {The Theorem of {W}eierstrass},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/weierstr.html}})

@ARTICLE(URYSOHN1.ABS,
    AUTHOR  = {Bia{\l}as, J\'ozef and Nakamura, Yatsuka},
    TITLE   = {Dyadic Numbers and {T}${}_4$ Topological Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/urysohn1.html}})

@ARTICLE(FACIRC_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Nakamura, Yatsuka},
    TITLE   = {Full Adder Circuit.  {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/facirc_1.html}})

@ARTICLE(COHSP_1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Continuous, Stable, and Linear Maps of Coherence Spaces},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/cohsp_1.html}})

@ARTICLE(PZFMISC1.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {Some Basic Properties of Many Sorted Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/pzfmisc1.html}})

@ARTICLE(TREES_A.ABS,
    AUTHOR  = {Okhotnikov, Oleg},
    TITLE   = {Replacement of Subtrees in a Tree},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/trees_a.html}})

@ARTICLE(PUA2MSS1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Minimal Signature for Partial Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/pua2mss1.html}})

@ARTICLE(QC_LANG4.ABS,
    AUTHOR  = {Okhotnikov, Oleg},
    TITLE   = {The Subformula Tree of a Formula of the First Order Language},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/qc_lang4.html}})

@ARTICLE(VECTSP_9.ABS,
    AUTHOR  = {\.Zynel, Mariusz},
    TITLE   = {The {S}teinitz Theorem and the Dimension of a Vector Space},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/vectsp_9.html}})

@ARTICLE(GOBOARD7.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {On the {G}o-{B}oard of a Standard Special Circular Sequence},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/goboard7.html}})

@ARTICLE(ENDALG.ABS,
    AUTHOR  = {Gryko, Jaros{\l}aw},
    TITLE   = {On the Monoid of Endomorphisms of Universal Algebra and Many
       Sorted Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/endalg.html}})

@ARTICLE(GOBOARD8.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {More on Segments on a {G}o-{B}oard},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/goboard8.html}})

@ARTICLE(MSSUBFAM.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {Certain Facts about Families of Subsets of Many Sorted Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/mssubfam.html}})

@ARTICLE(TRIANG_1.ABS,
    AUTHOR  = {Madras, Beata},
    TITLE   = {On the Concept of the Triangulation},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/triang_1.html}})

@ARTICLE(GOBOARD9.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Left and Right Component of the Complement of a Special Closed Curve},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/goboard9.html}})

@ARTICLE(REWRITE1.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Reduction Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1995},
    VOLUME  = {7},
    NOTE    = {\url{http://mizar.org/JFM/Vol7/rewrite1.html}})

@ARTICLE(MSUALG_5.ABS,
    AUTHOR  = {Milewski, Robert},
    TITLE   = {Lattice of Congruences in Many Sorted Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msualg_5.html}})

@ARTICLE(FUNCT_7.ABS,
    AUTHOR  = {Bancerek, Grzegorz and Trybulec, Andrzej},
    TITLE   = {Miscellaneous Facts about Functions},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/funct_7.html}})

@ARTICLE(ALTCAT_2.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Examples of Category Structures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/altcat_2.html}})

@ARTICLE(ORDERS_3.ABS,
    AUTHOR  = {Grabowski, Adam},
    TITLE   = {On the Category of Posets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/orders_3.html}})

@ARTICLE(SCMFSA_1.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Rudnicki, Piotr},
    TITLE   = {An Extension of {\bf {SCM}}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_1.html}})

@ARTICLE(CONNSP_3.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {Components and Unions of Components},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/connsp_3.html}})

@ARTICLE(SCMFSA_2.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Rudnicki, Piotr},
    TITLE   = {The {\SCMFSA} Computer},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_2.html}})

@ARTICLE(CLOSURE1.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {On the Many Sorted Closure Operator
and the Many Sorted Closure System},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/closure1.html}})

@ARTICLE(SCMFSA_3.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
    TITLE   = {Computation in {\SCMFSA}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_3.html}})

@ARTICLE(CLOSURE2.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {On the Closure Operator and the Closure System of Many Sorted Sets},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/closure2.html}})

@ARTICLE(MSUALG_6.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Translations, Endomorphisms, and Stable Equational Theories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msualg_6.html}})

@ARTICLE(MSUALG_7.ABS,
    AUTHOR  = {Milewski, Robert},
    TITLE   = {More on the Lattice of Many Sorted Equivalence Relations},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msualg_7.html}})

@ARTICLE(SCMFSA_4.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
    TITLE   = {Modifying Addresses of Instructions of {\SCMFSA}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_4.html}})

@ARTICLE(MSSCYC_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw and Rudnicki, Piotr},
    TITLE   = {The Correspondence Between Monotonic Many Sorted Signatures
       and Well-Founded Graphs. {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msscyc_1.html}})

@ARTICLE(SCMFSA_5.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
    TITLE   = {Relocability for {\SCMFSA}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_5.html}})

@ARTICLE(MSUALG_8.ABS,
    AUTHOR  = {Milewski, Robert},
    TITLE   = {More on the Lattice of Congruences in Many Sorted Algebra},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msualg_8.html}})

@ARTICLE(MSSCYC_2.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw and Rudnicki, Piotr},
    TITLE   = {The Correspondence Between Monotonic Many Sorted Signatures
and Well-Founded Graphs. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msscyc_2.html}})

@ARTICLE(FUNCTOR0.ABS,
    AUTHOR  = {Trybulec, Andrzej},
    TITLE   = {Functors for Alternative Categories},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/functor0.html}})

@ARTICLE(FUNCTOR1.ABS,
    AUTHOR  = {Zinn, Claus and Jaksch, Wolfgang},
    TITLE   = {Basic Properties of Functor Structures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/functor1.html}})

@ARTICLE(SCMFSA_7.ABS,
    AUTHOR  = {Asamoto, Noriko},
    TITLE   = {Some Multi Instructions Defined by Sequence of Instructions of {\SCMFSA}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa_7.html}})

@ARTICLE(PRALG_3.ABS,
    AUTHOR  = {Giero, Mariusz},
    TITLE   = {More on Products of Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/pralg_3.html}})

@ARTICLE(GOBRD10.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {Adjacency Concept for Pairs of Natural Numbers},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/gobrd10.html}})

@ARTICLE(MSALIMIT.ABS,
    AUTHOR  = {Grabowski, Adam},
    TITLE   = {Inverse Limits of Many Sorted Algebras},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msalimit.html}})

@ARTICLE(MSUALG_9.ABS,
    AUTHOR  = {Korni{\l}owicz, Artur},
    TITLE   = {On the Trivial Many Sorted Algebras and Many Sorted Congruences},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msualg_9.html}})

@ARTICLE(MSINST_1.ABS,
    AUTHOR  = {Grabowski, Adam},
    TITLE   = {Examples of Category Structures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/msinst_1.html}})

@ARTICLE(SCMFSA6A.ABS,
    AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Asamoto, Noriko},
    TITLE   = {On the Compositions of Macro Instructions. {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa6a.html}})

@ARTICLE(SF_MASTR.ABS,
    AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
    TITLE   = {Memory Handling for {\SCMFSA}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/sf_mastr.html}})

@ARTICLE(GOBRD11.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {Some Topological Properties of Cells in $R^2$},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/gobrd11.html}})

@ARTICLE(SCMFSA6B.ABS,
    AUTHOR  = {Asamoto, Noriko and Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej},
    TITLE   = {On the Composition of Macro Instructions. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa6b.html}})

@ARTICLE(GOBRD12.ABS,
    AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
    TITLE   = {The First Part of {J}ordan's Theorem for Special Polygons},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/gobrd12.html}})

@ARTICLE(SCMFSA6C.ABS,
    AUTHOR  = {Asamoto, Noriko and Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej},
    TITLE   = {On the Composition of Macro Instructions. {P}art {III}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa6c.html}})

@ARTICLE(SCMFSA7B.ABS,
    AUTHOR  = {Asamoto, Noriko},
    TITLE   = {Constant Assignment Macro Instructions of {\SCMFSA}. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa7b.html}})

@ARTICLE(SCMFSA8A.ABS,
    AUTHOR  = {Asamoto, Noriko},
    TITLE   = {Conditional Branch Macro Instructions of {\SCMFSA}. {P}art {I}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa8a.html}})

@ARTICLE(SCMFSA8B.ABS,
    AUTHOR  = {Asamoto, Noriko},
    TITLE   = {Conditional Branch Macro Instructions of {\SCMFSA}. {P}art {II}},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/scmfsa8b.html}})

@ARTICLE(YELLOW_0.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Bounds in Posets and Relational Substructures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/yellow_0.html}})

@ARTICLE(WAYBEL_0.ABS,
    AUTHOR  = {Bancerek, Grzegorz},
    TITLE   = {Directed Sets, Nets, Ideals, Filters, and Maps},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/waybel_0.html}})

@ARTICLE(KNASTER.ABS,
    AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
    TITLE   = {Fixpoints in Complete Lattices},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/knaster.html}})

@ARTICLE(YELLOW_1.ABS,
    AUTHOR  = {Grabowski, Adam and Milewski, Robert},
    TITLE   = {Boolean Posets, Posets under Inclusion and
   Products of Relational Structures},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/yellow_1.html}})

@ARTICLE(YELLOW_2.ABS,
    AUTHOR  = {\.Zynel, Mariusz and Byli\'nski, Czes{\l}aw},
    TITLE   = {Properties of Relational Structures, Posets, Lattices and Maps},
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/yellow_2.html}})

@ARTICLE(WAYBEL_1.ABS,
    AUTHOR  = {Byli\'nski, Czes{\l}aw},
    TITLE   = {Galois Connections },
    JOURNAL = {Journal of Formalized Mathematics},
    YEAR    = {1996},
    VOLUME  = {8},
    NOTE    = {\url{http://mizar.org/JFM/Vol8/waybel_1.html}})

@