@Preamble{"\newcommand{\calE}{\cal E} \newcommand{\rmT}{\rm T} \newcommand{\BbbR}{\mathbb R} \newcommand{\SCM}{\bf SCM} \newcommand{\SCMFSA}{${\bf SCM}_{\rm FSA}$}"}
@MISC(FF_SIEC.ABS,
      AUTHOR = {Korczy\'nski, Waldemar},
      TITLE  = {Definitons of {P}etri Net -- Part {I} -- {\tt FF\_SIEC}},
      HOWPUBLISHED = {Mizar Mathematical Library},
      YEAR = 1992)

@MISC(E_SIEC.ABS,
      AUTHOR = {Korczy\'nski, Waldemar},
      TITLE  = {Definitons of {P}etri Net -- Part {II} -- {\tt E\_SIEC}},
      HOWPUBLISHED = {Mizar Mathematical Library},
      YEAR = 1992)

@MISC(S_SIEC.ABS,
      AUTHOR = {Korczy\'nski, Waldemar},
      TITLE  = {Definitions of {P}etri Net -- Part {III} -- {\tt S\_SIEC}},
      HOWPUBLISHED = {Mizar Mathematical Library},
      YEAR = 1992)

@ARTICLE(ARYTM_0.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Introduction to Arithmetics},
      JOURNAL = {To appear in Formalized Mathematics})

@ARTICLE(ARYTM_3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Arithmetic of Non-Negative Rational Numbers},
      JOURNAL = {To appear in Formalized Mathematics})

@ARTICLE(BINOP_2.ABS,
      AUTHOR  = {Library Committee of the Association of Mizar Users},
      TITLE   = {Binary Operations on Numbers},
      JOURNAL = {To appear in Formalized Mathematics})

@ARTICLE(NUMBERS.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Subsets of Complex Numbers},
      JOURNAL = {To appear in Formalized Mathematics})

@ARTICLE(TARSKI.ABS,
      AUTHOR  = {Andrzej Trybulec},
      TITLE   = {Tarski {G}rothendieck Set Theory},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {9--11})

@ARTICLE(AXIOMS.ABS,
      AUTHOR  = {Andrzej Trybulec},
      TITLE   = {Built-in Concepts },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {13--15})

@ARTICLE(BOOLE.ABS,
      AUTHOR  = {Zinaida Trybulec and Halina {\'{S}}wi{\Ple}czkowska},
      TITLE   = {Boolean Properties of Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {17--23})

@ARTICLE(ENUMSET1.ABS,
      AUTHOR  = {Andrzej Trybulec},
      TITLE   = {Enumerated Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {25--34})

@ARTICLE(REAL_1.ABS,
      AUTHOR  = {Krzysztof Hryniewiecki},
      TITLE   = {Basic Properties  of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {35--40})

@ARTICLE(NAT_1.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {The Fundamental Properties of Natural Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {41--46})

@ARTICLE(ZFMISC_1.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Some Basic Properties of Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {47--53})

@ARTICLE(FUNCT_1.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Functions and Their Basic Properties },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {55--65})

@ARTICLE(SUBSET_1.ABS,
      AUTHOR  = {Zinaida Trybulec},
      TITLE   = {Properties of Subsets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {67--71})

@ARTICLE(RELAT_1.ABS,
      AUTHOR  = {Edmund Woronowicz},
      TITLE   = {Relations and Their Basic Properties },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {73--83})

@ARTICLE(RELAT_2.ABS,
      AUTHOR  = {Edmund Woronowicz and Anna Zalewska},
      TITLE   = {Properties of Binary Relations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {85--89})

@ARTICLE(ORDINAL1.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {The Ordinal Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {91--96})

@ARTICLE(MCART_1.ABS,
      AUTHOR  = {Andrzej Trybulec},
      TITLE   = {Tuples, Projections and {C}artesian Products },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {97--105})

@ARTICLE(FINSEQ_1.ABS,
      AUTHOR  = {Grzegorz Bancerek and Krzysztof Hryniewiecki},
      TITLE   = {Segments of Natural Numbers and Finite Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {107--114})

@ARTICLE(DOMAIN_1.ABS,
      AUTHOR  = {Andrzej Trybulec},
      TITLE   = {Domains and Their {C}artesian Products },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {115--122})

@ARTICLE(WELLORD1.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {The Well Ordering Relations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {123--129})

@ARTICLE(ZF_LANG.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {A Model of {ZF} Set Theory Language },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {131--145})

@ARTICLE(SETFAM_1.ABS,
      AUTHOR  = {Beata Padlewska},
      TITLE   = {Families of Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {147--152})

@ARTICLE(FUNCT_2.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Functions from a Set to a Set },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {153--164})

@ARTICLE(FINSET_1.ABS,
      AUTHOR  = {Agata Darmochwa{\l}},
      TITLE   = {Finite Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {165--167})

@ARTICLE(GRFUNC_1.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Graphs of Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {169--173})

@ARTICLE(BINOP_1.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Binary Operations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {175--180})

@ARTICLE(RELSET_1.ABS,
      AUTHOR  = {Edmund Woronowicz},
      TITLE   = {Relations Defined on Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {181--186})

@ARTICLE(FINSUB_1.ABS,
      AUTHOR  = {Andrzej Trybulec and Agata Darmochwa{\l}},
      TITLE   = {Boolean Domains },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {187--190})

@ARTICLE(ZF_MODEL.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {Models and Satisfiability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {191--199})

@ARTICLE(ZF_COLLA.ABS,
      AUTHOR  = {Grzegorz Bancerek},
      TITLE   = {The Contraction Lemma },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {201--203})

@ARTICLE(INCSP_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Axioms of Incidence },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {205--213})

@ARTICLE(LATTICES.ABS,
      AUTHOR  = {Stanis{\l}aw {\.{Z}}ukowski},
      TITLE   = {Introduction to Lattice Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {215--222})

@ARTICLE(PRE_TOPC.ABS,
      AUTHOR  = {Beata Padlewska and Agata Darmochwa{\l}},
      TITLE   = {Topological Spaces and Continuous Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {223--230})

@ARTICLE(TOPS_1.ABS,
      AUTHOR  = {Miros{\l}aw Wysocki and Agata Darmochwa{\l}},
      TITLE   = {Subsets of Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {231--237})

@ARTICLE(CONNSP_1.ABS,
      AUTHOR  = {Beata Padlewska},
      TITLE   = {Connected Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {239--244})

@ARTICLE(FUNCT_3.ABS,
      AUTHOR  = {Czes{\l}aw Byli{\'n}ski},
      TITLE   = {Basic Functions and Operations on Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      NUMBER  = {{\bf 1}},
      VOLUME  = 1,
      PAGES   = {245--254})

@ARTICLE(TOPS_2.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata},
      TITLE   = {Families of Subsets, Subspaces and Mappings in Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {257--261},
      NUMBER  = {{\bf 2}})

@ARTICLE(ANAL_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Some Properties of Functions Modul and Signum },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {263--264},
      NUMBER  = {{\bf 2}})

@ARTICLE(ABSVALUE.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Some Properties of Functions Modul and Signum },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {263--264},
      NUMBER  = {{\bf 2}})

@ARTICLE(WELLORD2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Zermelo Theorem and Axiom of Choice },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {265--267},
      NUMBER  = {{\bf 2}})

@ARTICLE(SEQ_1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Real Sequences and Basic Operations on Them },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {269--272},
      NUMBER  = {{\bf 2}})

@ARTICLE(SEQ_2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Convergent Sequences and the Limit of Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {273--275},
      NUMBER  = {{\bf 2}})

@ARTICLE(ZFMODEL1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Properties of {ZF} Models },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {277--280},
      NUMBER  = {{\bf 2}})

@ARTICLE(ORDINAL2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Sequences of Ordinal Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {281--290},
      NUMBER  = {{\bf 2}})

@ARTICLE(RLVECT_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Vectors in Real Linear Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {291--296},
      NUMBER  = {{\bf 2}})

@ARTICLE(RLSUB_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Subspaces and Cosets of Subspaces in Real Linear Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {297--301},
      NUMBER  = {{\bf 2}})

@ARTICLE(QC_LANG1.ABS,
      AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
      TITLE   = {A First Order Language },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {303--311},
      NUMBER  = {{\bf 2}})

@ARTICLE(ORDERS_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Partially Ordered Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {313--319},
      NUMBER  = {{\bf 2}})

@ARTICLE(RECDEF_1.ABS,
      AUTHOR  = {Hryniewiecki, Krzysztof},
      TITLE   = {Recursive Definitions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {321--328},
      NUMBER  = {{\bf 2}})

@ARTICLE(FUNCOP_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Binary Operations Applied to Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {329--334},
      NUMBER  = {{\bf 2}})

@ARTICLE(VECTSP_1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech and Muzalewski, Micha{\l}},
      TITLE   = {Abelian Groups, Fields and Vector Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {335--342},
      NUMBER  = {{\bf 2}})

@ARTICLE(PARSP_1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech and Muzalewski, Micha{\l}},
      TITLE   = {Parallelity Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {343--348},
      NUMBER  = {{\bf 2}})

@ARTICLE(SYMSP_1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech and Muzalewski, Micha{\l}},
      TITLE   = {Construction of a bilinear antisymmetric form in simplectic vector space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {349--352},
      NUMBER  = {{\bf 2}})

@ARTICLE(ORTSP_1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech and Muzalewski, Micha{\l}},
      TITLE   = {Construction of a bilinear symmetric form in orthogonal vector space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {353--356},
      NUMBER  = {{\bf 2}})

@ARTICLE(PARTFUN1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Partial Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {357--367},
      NUMBER  = {{\bf 2}})

@ARTICLE(SETWISEO.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Semilattice Operations on Finite Subsets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {369--376},
      NUMBER  = {{\bf 2}})

@ARTICLE(CARD_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Cardinal Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {377--382},
      NUMBER  = {{\bf 2}})

@ARTICLE(COMPTS_1.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata},
      TITLE   = {Compact Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {383--386},
      NUMBER  = {{\bf 2}})

@ARTICLE(ORDERS_2.ABS,
      AUTHOR  = {Trybulec, Wojciech A. and Bancerek, Grzegorz},
      TITLE   = {Kuratowski -- {Z}orn Lemma },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {387--393},
      NUMBER  = {{\bf 2}})

@ARTICLE(RLSUB_2.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Operations on Subspaces in Real Linear Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {395--399},
      NUMBER  = {{\bf 2}})

@ARTICLE(PROB_1.ABS,
      AUTHOR  = {N{\Ple}dzusiak, Andrzej},
      TITLE   = { $\sigma$-Fields and Probability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {401--407},
      NUMBER  = {{\bf 2}})

@ARTICLE(CAT_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Introduction to Categories and Functors },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {409--420},
      NUMBER  = {{\bf 2}})

@ARTICLE(TREES_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Introduction to Trees },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {421--427},
      NUMBER  = {{\bf 2}})

@ARTICLE(WELLSET1.ABS,
      AUTHOR  = {Nowak, Bogdan and Bia{\l}ecki, S{\l}awomir},
      TITLE   = {Zermelo's Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {431--432},
      NUMBER  = {{\bf 3}})

@ARTICLE(REALSET1.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Group and Field Definitions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {433--439},
      NUMBER  = {{\bf 3}})

@ARTICLE(EQREL_1.ABS,
      AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
      TITLE   = {Equivalence Relations and Classes of Abstraction },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {441--444},
      NUMBER  = {{\bf 3}})

@ARTICLE(SQUARE_1.ABS,
      AUTHOR  = {Trybulec, Andrzej and Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Some Properties of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {445--449},
      NUMBER  = {{\bf 3}})

@ARTICLE(QC_LANG2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Connectives and Subformulae of the First Order Language },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {451--458},
      NUMBER  = {{\bf 3}})

@ARTICLE(QC_LANG3.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw and Bancerek, Grzegorz},
      TITLE   = {Variables in Formulae of the First Order Language },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {459--469},
      NUMBER  = {{\bf 3}})

@ARTICLE(SEQM_3.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Monotone Real Sequences. {S}ubsequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {471--475},
      NUMBER  = {{\bf 3}})

@ARTICLE(SEQ_4.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Convergent Real Sequences. {U}pper and Lower Bound of Sets of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {477--481},
      NUMBER  = {{\bf 3}})

@ARTICLE(MIDSP_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Midpoint algebras },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {483--488},
      NUMBER  = {{\bf 3}})

@ARTICLE(QMAX_1.ABS,
      AUTHOR  = {Sadowski, Pawe{\l} and Trybulec, Andrzej and Raczkowski, Konrad},
      TITLE   = {The Fundamental Logic Structure in Quantum Mechanics },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {489--494},
      NUMBER  = {{\bf 3}})

@ARTICLE(FRAENKEL.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Function Domains and {F}r{\ae}nkel Operator },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {495--500},
      NUMBER  = {{\bf 3}})

@ARTICLE(INT_1.ABS,
      AUTHOR  = {Trybulec, Micha{\l} J.},
      TITLE   = {Integers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {501--505},
      NUMBER  = {{\bf 3}})

@ARTICLE(COMPLEX1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {The Complex Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {507--513},
      NUMBER  = {{\bf 3}})

@ARTICLE(ORDINAL3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Ordinal Arithmetics },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {515--519},
      NUMBER  = {{\bf 3}})

@ARTICLE(FUNCT_4.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {The Modification of a Function by a Function and the Iteration of the Composition of a Function },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {521--527},
      NUMBER  = {{\bf 3}})

@ARTICLE(FINSEQ_2.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Finite Sequences and Tuples of Elements of a Non-empty Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {529--536},
      NUMBER  = {{\bf 3}})

@ARTICLE(FUNCT_5.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Curried and Uncurried Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {537--541},
      NUMBER  = {{\bf 3}})

@ARTICLE(CARD_2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Cardinal Arithmetics },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {543--547},
      NUMBER  = {{\bf 3}})

@ARTICLE(PARSP_2.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech},
      TITLE   = {Fano-{D}esargues Parallelity Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {549--553},
      NUMBER  = {{\bf 3}})

@ARTICLE(FUNCSDOM.ABS,
      AUTHOR  = {Oryszczyszyn , Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Real Functions Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {555--561},
      NUMBER  = {{\bf 3}})

@ARTICLE(CLASSES1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Tarski's Classes and Ranks },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {563--567},
      NUMBER  = {{\bf 3}})

@ARTICLE(FINSEQ_3.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Non-contiguous Substrings and One-to-one Finite Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {569--573},
      NUMBER  = {{\bf 3}})

@ARTICLE(FINSEQ_4.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Pigeon Hole Principle },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {575--579},
      NUMBER  = {{\bf 3}})

@ARTICLE(RLVECT_2.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Linear Combinations in Real Linear Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {581--588},
      NUMBER  = {{\bf 3}})

@ARTICLE(CARD_3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {K{\"o}nig's Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {589--593},
      NUMBER  = {{\bf 3}})

@ARTICLE(CLASSES2.ABS,
      AUTHOR  = {Nowak, Bogdan and Bancerek, Grzegorz},
      TITLE   = {Universal Classes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {595--600},
      NUMBER  = {{\bf 3}})

@ARTICLE(ANALOAF.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Analytical Ordered Affine Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {601--605},
      NUMBER  = {{\bf 3}})

@ARTICLE(METRIC_1.ABS,
      AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam and Startek, Mariusz},
      TITLE   = {Metric Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {607--610},
      NUMBER  = {{\bf 3}})

@ARTICLE(DIRAF.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Ordered Affine Spaces Defined in Terms of Directed Parallelity -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {611--615},
      NUMBER  = {{\bf 3}})

@ARTICLE(AFF_1.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Parallelity and Lines in Affine Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {617--621},
      NUMBER  = {{\bf 3}})

@ARTICLE(AFF_2.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Classical Configurations in Affine Planes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {625--633},
      NUMBER  = {{\bf 4}})

@ARTICLE(AFF_3.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Affine Localizations of {D}esargues Axiom },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {635--642},
      NUMBER  = {{\bf 4}})

@ARTICLE(FINSEQOP.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Binary Operations Applied to Finite Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {643--649},
      NUMBER  = {{\bf 4}})

@ARTICLE(SETWOP_2.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Semigroup operations on finite subsets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {651--656},
      NUMBER  = {{\bf 4}})

@ARTICLE(COLLSP.ABS,
      AUTHOR  = {Skaba, Wojciech},
      TITLE   = {The Collinearity Structure    },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {657--659},
      NUMBER  = {{\bf 4}})

@ARTICLE(RVSUM_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {The Sum and Product of Finite Sequences of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {661--668},
      NUMBER  = {{\bf 4}})

@ARTICLE(CQC_LANG.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {A Classical First Order Language },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {669--676},
      NUMBER  = {{\bf 4}})

@ARTICLE(PASCH.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof and Pra{\.z}mowska, Ma{\l}gorzata},
      TITLE   = {Classical and Non--classical {P}asch Configurations in Ordered Affine Planes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {677--680},
      NUMBER  = {{\bf 4}})
      
@ARTICLE(REAL_LAT.ABS,
      AUTHOR  = {Chmur, Marek},
      TITLE   = {The Lattice of Real Numbers. {T}he Lattice of Real Functions  },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {681--684},
      NUMBER  = {{\bf 4}})

@ARTICLE(TDGROUP.ABS,
      AUTHOR  = {Lewandowski, Grzegorz and Pra{\.z}mowski, Krzysztof},
      TITLE   = {A Construction of an Abstract Space of Congruence of Vectors },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {685--688},
      NUMBER  = {{\bf 4}})

@ARTICLE(CQC_THE1.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata},
      TITLE   = {A First--Order Predicate Calculus },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {689--695},
      NUMBER  = {{\bf 4}})

@ARTICLE(PARTFUN2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Partial Functions from a Domain to a Domain  },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {697--702},
      NUMBER  = {{\bf 4}})

@ARTICLE(RFUNCT_1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Partial Functions from a Domain to the Set of Real Numbers  },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {703--709},
      NUMBER  = {{\bf 4}})

@ARTICLE(ORDINAL4.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Increasing and Continuous Ordinal Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {711--714},
      NUMBER  = {{\bf 4}})

@ARTICLE(TRANSGEO.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Transformations in Affine Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {715--723},
      NUMBER  = {{\bf 4}})

@ARTICLE(CAT_2.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Subcategories and Products of Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {725--732},
      NUMBER  = {{\bf 4}})

@ARTICLE(MARGREL1.ABS,
      AUTHOR  = {Woronowicz, Edmund},
      TITLE   = {Many--Argument Relations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {733--737},
      NUMBER  = {{\bf 4}})

@ARTICLE(VALUAT_1.ABS,
      AUTHOR  = {Woronowicz, Edmund},
      TITLE   = {Interpretation and Satisfiability in the First Order Logic },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {739--743},
      NUMBER  = {{\bf 4}})

@ARTICLE(PROB_2.ABS,
      AUTHOR  = {N{\Ple}dzusiak, Andrzej},
      TITLE   = {Probability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {745--749},
      NUMBER  = {{\bf 4}})

@ARTICLE(TRANSLAC.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Translations in Affine Planes  },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {751--753},
      NUMBER  = {{\bf 4}})

@ARTICLE(RPR_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Introduction to Probability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {755--760},
      NUMBER  = {{\bf 4}})

@ARTICLE(ANPROJ_1.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {A Construction of Analytical Projective Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {761--766},
      NUMBER  = {{\bf 4}})

@ARTICLE(ANPROJ_2.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {767--776},
      NUMBER  = {{\bf 4}})

@ARTICLE(RCOMP_1.ABS,
      AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
      TITLE   = {Topological Properties of Subsets in Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {777--780},
      NUMBER  = {{\bf 4}})

@ARTICLE(RFUNCT_2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Properties of Real Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {781--786},
      NUMBER  = {{\bf 4}})

@ARTICLE(FCONT_1.ABS,
      AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
      TITLE   = {Real Function Continuity },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {787--791},
      NUMBER  = {{\bf 4}})

@ARTICLE(FCONT_2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
      TITLE   = {Real Function Uniform Continuity },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {793--795},
      NUMBER  = {{\bf 4}})

@ARTICLE(FDIFF_1.ABS,
      AUTHOR  = {Raczkowski, Konrad and Sadowski, Pawe{\l}},
      TITLE   = {Real Function Differentiability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {797--801},
      NUMBER  = {{\bf 4}})

@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 = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {803--805},
      NUMBER  = {{\bf 4}})

@ARTICLE(REALSET2.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Properties of Fields },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {807--812},
      NUMBER  = {{\bf 5}})

@ARTICLE(FILTER_0.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Filters -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {813--819},
      NUMBER  = {{\bf 5}})

@ARTICLE(GROUP_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Groups },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {821--827},
      NUMBER  = {{\bf 5}})

@ARTICLE(INT_2.ABS,
      AUTHOR  = {Kwiatek, Rafa{\l} and Zwara, Grzegorz},
      TITLE   = {The Divisibility of Integers and Integer Relative Primes    },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {829--832},
      NUMBER  = {{\bf 5}})

@ARTICLE(ALGSTR_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {From Loops to Abelian Multiplicative Groups with Zero },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {833--840},
      NUMBER  = {{\bf 5}})

@ARTICLE(RAT_1.ABS,
      AUTHOR  = {Kondracki, Andrzej},
      TITLE   = {Basic Properties of Rational Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {841--845},
      NUMBER  = {{\bf 5}})

@ARTICLE(RLVECT_3.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Basis of Real Linear Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {847--850},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_3.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Finite Sums of Vectors in Vector Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {851--854},
      NUMBER  = {{\bf 5}})

@ARTICLE(GROUP_2.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Subgroup and Cosets of Subgroups },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {855--864},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_4.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Subspaces and Cosets of Subspaces in Vector Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {865--870},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_5.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Operations on Subspaces in Vector Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {871--876},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_6.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Linear Combinations in Vector Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {877--882},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_7.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Basis of Vector Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {883--885},
      NUMBER  = {{\bf 5}})

@ARTICLE(NEWTON.ABS,
      AUTHOR  = {Kwiatek, Rafa{\l}},
      TITLE   = {Factorial and {N}ewton coefficients },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {887--890},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANALMETR.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Analytical Metric Affine Spaces and Planes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {891--899},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANPROJ_3.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {901--907},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANPROJ_4.ABS,
      AUTHOR  = {Leo{\.n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- part {III} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {909--918},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANPROJ_5.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- part {IV} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {919--927},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANPROJ_6.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- part {V} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {929--938},
      NUMBER  = {{\bf 5}})

@ARTICLE(ANPROJ_7.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Projective Spaces -- part {VI} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {939--947},
      NUMBER  = {{\bf 5}})

@ARTICLE(NET_1.ABS,
      AUTHOR  = {Korczy{\'n}ski, Waldemar},
      TITLE   = {Some Elementary Notions of the Theory of {P}etri Nets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {949--953},
      NUMBER  = {{\bf 5}})

@ARTICLE(GROUP_3.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Classes of Conjugation. {N}ormal Subgroups },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {955--962},
      NUMBER  = {{\bf 5}})

@ARTICLE(ZF_LANG1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Replacing of Variables in Formulas of {ZF} Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {963--972},
      NUMBER  = {{\bf 5}})

@ARTICLE(ZF_REFLE.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {The Reflection Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {973--977},
      NUMBER  = {{\bf 5}})

@ARTICLE(FINSOP_1.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Binary Operations on Finite Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {979--981},
      NUMBER  = {{\bf 5}})

@ARTICLE(LATTICE2.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Finite Join and Finite Meet and Dual Lattices },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {983--988},
      NUMBER  = {{\bf 5}})

@ARTICLE(ZFREFLE1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Consequences of the Reflection Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1990,
      VOLUME  = 1,
      PAGES   = {989--993},
      NUMBER  = {{\bf 5}})

@ARTICLE(VECTSP_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Construction of Rings and Left-, Right-, and Bi-Modules over a Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {3--11},
      NUMBER  = {{\bf 1}})

@ARTICLE(PROJDES1.ABS,
      AUTHOR  = {Kusak, Eugeniusz},
      TITLE   = {Desargues Theorem In Projective 3-Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {13--16},
      NUMBER  = {{\bf 1}})

@ARTICLE(LIMFUNC1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {The Limit of a Real Function at Infinity },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {17--28},
      NUMBER  = {{\bf 1}})

@ARTICLE(LIMFUNC2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {One-Side Limits of a Real Function at a Point },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {29--40},
      NUMBER  = {{\bf 1}})

@ARTICLE(GROUP_4.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Lattice of Subgroups of a Group. {F}rattini Subgroup },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {41--47},
      NUMBER  = {{\bf 1}})

@ARTICLE(REAL_2.ABS,
      AUTHOR  = {Kondracki, Andrzej},
      TITLE   = {Equalities and Inequalities in Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {49--63},
      NUMBER  = {{\bf 1}})

@ARTICLE(CARD_4.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Countable Sets and {H}essenberg's Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {65--69},
      NUMBER  = {{\bf 1}})

@ARTICLE(LIMFUNC3.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {The Limit of a Real Function at a Point },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {71--80},
      NUMBER  = {{\bf 1}})

@ARTICLE(LIMFUNC4.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {The Limit of a Composition of Real Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {81--92},
      NUMBER  = {{\bf 1}})

@ARTICLE(CONNSP_2.ABS,
      AUTHOR  = {Padlewska, Beata},
      TITLE   = {Locally Connected Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {93--96},
      NUMBER  = {{\bf 1}})

@ARTICLE(ALGSEQ_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
      TITLE   = {Construction of Finite Sequences over Ring and Left-, Right-,  and Bi-Modules over a Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {97--104},
      NUMBER  = {{\bf 1}})

@ARTICLE(TOLER_1.ABS,
      AUTHOR  = {Hryniewiecki, Krzysztof},
      TITLE   = {Relations of Tolerance },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {105--109},
      NUMBER  = {{\bf 1}})

@ARTICLE(NORMSP_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Real Normed Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {111--115},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCHEME1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Schemes of Existence of some Types of Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {117--123},
      NUMBER  = {{\bf 1}})

@ARTICLE(PREPOWER.ABS,
      AUTHOR  = {Raczkowski, Konrad},
      TITLE   = {Integer and Rational Exponents },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {125--130},
      NUMBER  = {{\bf 1}})

@ARTICLE(HOMOTHET.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Homotheties and Shears in Affine Planes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {131--133},
      NUMBER  = {{\bf 1}})

@ARTICLE(AFVECT0.ABS,
      AUTHOR  = {Lewandowski, Grzegorz and Pra{\.z}mowski, Krzysztof and Lewandowska, Bo{\.z}ena},
      TITLE   = {Directed Geometrical Bundles and Their Analytical Representation },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {135--141},
      NUMBER  = {{\bf 1}})

@ARTICLE(ZFMODEL2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Definable Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {143--145},
      NUMBER  = {{\bf 1}})

@ARTICLE(LUKASI_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz  and Darmochwa{\l}, Agata and Trybulec, Andrzej},
      TITLE   = {Propositional Calculus },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {147--150},
      NUMBER  = {{\bf 1}})

@ARTICLE(COMPLSP1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw and Trybulec, Andrzej},
      TITLE   = {Complex Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {151--158},
      NUMBER  = {{\bf 1}})

@ARTICLE(REALSET3.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Several Properties of Fields. {F}ield Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {159--162},
      NUMBER  = {{\bf 1}})

@ARTICLE(SUPINF_1.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Infimum and Supremum of the Set of Real Numbers. {M}easure Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {163--171},
      NUMBER  = {{\bf 1}})

@ARTICLE(SUPINF_2.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Series of  Positive Real Numbers. {M}easure Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {173--183},
      NUMBER  = {{\bf 1}})

@ARTICLE(ALGSTR_2.ABS,
      AUTHOR  = {Skaba, Wojciech and Muzalewski, Micha{\l}},
      TITLE   = {From Double Loops to Fields    },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {185--191},
      NUMBER  = {{\bf 1}})

@ARTICLE(METRIC_3.ABS,
      AUTHOR  = {Kanas, Stanis{\l}awa and Stankiewicz, Jan},
      TITLE   = {Metrics in {C}artesian Product },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {193--197},
      NUMBER  = {{\bf 2}})

@ARTICLE(SUB_METR.ABS,
      AUTHOR  = {Lecko, Adam and Startek, Mariusz},
      TITLE   = {Submetric Spaces -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {199--203},
      NUMBER  = {{\bf 2}})

@ARTICLE(METRIC_2.ABS,
      AUTHOR  = {Lecko, Adam and Startek, Mariusz},
      TITLE   = {On Pseudometric Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {205--211},
      NUMBER  = {{\bf 2}})

@ARTICLE(POWER.ABS,
      AUTHOR  = {Raczkowski, Konrad and N{\Ple}dzusiak, Andrzej},
      TITLE   = {Real Exponents and Logarithms },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {213--216},
      NUMBER  = {{\bf 2}})

@ARTICLE(HESSENBE.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech},
      TITLE   = {Hessenberg Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {217--219},
      NUMBER  = {{\bf 2}})

@ARTICLE(MULTOP_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Three-Argument Operations and Four-Argument Operations    },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {221--224},
      NUMBER  = {{\bf 2}})

@ARTICLE(INCPROJ.ABS,
      AUTHOR  = {Leo{\'n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Incidence Projective Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {225--232},
      NUMBER  = {{\bf 2}})

@ARTICLE(AFVECT01.ABS,
      AUTHOR  = {Konstanta, Barbara and Kowieska, Urszula and Lewandowski, Grzegorz and Pra{\.z}mowski, Krzysztof},
      TITLE   = {One-Dimensional Congruence of Segments, Basic Facts and Midpoint  Relation },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {233--235},
      NUMBER  = {{\bf 2}})

@ARTICLE(NORMFORM.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Algebra of Normal Forms },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {237--242},
      NUMBER  = {{\bf 2}})

@ARTICLE(O_RING_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
      TITLE   = {Ordered Rings -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {243--245},
      NUMBER  = {{\bf 2}})

@ARTICLE(O_RING_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
      TITLE   = {Ordered Rings -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {247--249},
      NUMBER  = {{\bf 2}})

@ARTICLE(O_RING_3.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Szczerba, Les{\l}aw W.},
      TITLE   = {Ordered Rings -- Part {III} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {251--253},
      NUMBER  = {{\bf 2}})

@ARTICLE(MCART_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {{N}-Tuples and {C}artesian Products for n$=$5 },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {255--258},
      NUMBER  = {{\bf 2}})

@ARTICLE(ALGSTR_3.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Ternary Fields },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {259--261},
      NUMBER  = {{\bf 2}})

@ARTICLE(MEASURE1.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {The $\sigma$-additive Measure Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {263--270},
      NUMBER  = {{\bf 2}})

@ARTICLE(PROJRED1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\'n}czuk, Wojciech},
      TITLE   = {Incidence Projective Space (a reduction theorem in a plane) },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {271--274},
      NUMBER  = {{\bf 2}})

@ARTICLE(MOD_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Groups, Rings, Left- and Right-Modules },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {275--278},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Finite Sums of Vectors in Left Module over Associative Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {279--282},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Submodules and Cosets of Submodules in Left Module over Associative Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {283--287},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_3.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Operations on Submodules in Left Module over Associative Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {289--293},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_4.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Linear Combinations in Left Module over Associative Ring },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {295--300},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_5.ABS,
      AUTHOR  = {Muzalewski, Micha{\l} and Skaba, Wojciech},
      TITLE   = {Linear Independence in Left Module over Domain },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {301--303},
      NUMBER  = {{\bf 2}})

@ARTICLE(PROCAL_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan and Trybulec, Andrzej},
      TITLE   = {Calculus of Propositions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {305--307},
      NUMBER  = {{\bf 2}})

@ARTICLE(CQC_THE2.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata},
      TITLE   = {Calculus of Quantifiers. {D}eduction Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {309--312},
      NUMBER  = {{\bf 2}})

@ARTICLE(ANALTRAP.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {A construction of analytical Ordered Trapezium Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {315--322},
      NUMBER  = {{\bf 3}})

@ARTICLE(GEOMTRAP.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {A construction of analytical Ordered Trapezium Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {315--322},
      NUMBER  = {{\bf 3}})

@ARTICLE(PROJRED2.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Leo{\.n}czuk, Wojciech and Pra{\.z}mowski, Krzysztof},
      TITLE   = {On Projections in Projective Planes ({P}art {II} ) },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {323--329},
      NUMBER  = {{\bf 3}})

@ARTICLE(CONAFFM.ABS,
      AUTHOR  = {{\'{S}}wierzy{\'n}ska, Jolanta and {\'{S}}wierzy{\'n}ski, Bogdan},
      TITLE   = {Metric-Affine Configurations in Metric Affine Planes -- {P}art {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {331--334},
      NUMBER  = {{\bf 3}})

@ARTICLE(CONMETR.ABS,
      AUTHOR  = {{\'{S}}wierzy{\'n}ska, Jolanta and {\'{S}}wierzy{\'n}ski, Bogdan},
      TITLE   = {Metric-Affine Configurations in Metric Affine Planes -- {P}art {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {335--340},
      NUMBER  = {{\bf 3}})

@ARTICLE(PAPDESAF.ABS,
      AUTHOR  = {Pra{\.z}mowski, Krzysztof},
      TITLE   = {{F}anoian, {P}appian and {D}esarguesian Affine Spaces  },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {341--346},
      NUMBER  = {{\bf 3}})

@ARTICLE(PARDEPAP.ABS,
      AUTHOR  = {Pra{\.z}mowski, Krzysztof and Radziszewski, Krzysztof},
      TITLE   = {Elementary Variants of Affine Configurational Theorems },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {347--348},
      NUMBER  = {{\bf 3}})

@ARTICLE(SEMI_AF1.ABS,
      AUTHOR  = {Kusak, Eugeniusz and Radziszewski, Krzysztof},
      TITLE   = {Semi\_Affine Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {349--356},
      NUMBER  = {{\bf 3}})

@ARTICLE(AFF_4.ABS,
      AUTHOR  = {Leo{\.n}czuk, Wojciech and Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Planes in Affine Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {357--363},
      NUMBER  = {{\bf 3}})

@ARTICLE(GRAPH_1.ABS,
      AUTHOR  = {Hryniewiecki, Krzysztof},
      TITLE   = {Graphs },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {365--370},
      NUMBER  = {{\bf 3}})

@ARTICLE(ZF_FUND1.ABS,
      AUTHOR  = {Kondracki, Andrzej},
      TITLE   = {{M}ostowski's Fundamental Operations -- {P}art {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {371--375},
      NUMBER  = {{\bf 3}})

@ARTICLE(AFPROJ.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {A Projective Closure and Projective Horizon of an Affine Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {377--384},
      NUMBER  = {{\bf 3}})

@ARTICLE(SCHEMS_1.ABS,
      AUTHOR  = {Czuba, Stanis{\l}aw T.},
      TITLE   = {Schemes },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {385--391},
      NUMBER  = {{\bf 3}})

@ARTICLE(HEYTING1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Algebra of Normal Forms Is a {H}eyting Algebra },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {393--396},
      NUMBER  = {{\bf 3}})

@ARTICLE(TREES_2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {K{\"o}nig's Lemma },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {397--402},
      NUMBER  = {{\bf 3}})

@ARTICLE(FCONT_3.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Monotonic and Continuous Real Function },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {403--405},
      NUMBER  = {{\bf 3}})

@ARTICLE(FDIFF_2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
      TITLE   = {Real Function Differentiability -- {P}art {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {407--411},
      NUMBER  = {{\bf 3}})

@ARTICLE(PRELAMB.ABS,
      AUTHOR  = {Zielonka, Wojciech},
      TITLE   = {Preliminaries to the {L}ambek calculus },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {413--418},
      NUMBER  = {{\bf 3}})

@ARTICLE(OPPCAT_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Opposite Categories and Contravariant Functors },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {419--424},
      NUMBER  = {{\bf 3}})

@ARTICLE(ZF_FUND2.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Kondracki, Andrzej},
      TITLE   = {{M}ostowski's Fundamental Operations -- {P}art {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {425--427},
      NUMBER  = {{\bf 3}})

@ARTICLE(EUCLMETR.ABS,
      AUTHOR  = {Oryszczyszyn, Henryk and Pra{\.z}mowski, Krzysztof},
      TITLE   = {Fundamental Types of Metric Affine Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {429--432},
      NUMBER  = {{\bf 3}})

@ARTICLE(FILTER_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Filters -- Part {II}. {Q}uotient Lattices Modulo Filters and Direct Product of Two Lattices },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {433--438},
      NUMBER  = {{\bf 3}})

@ARTICLE(CONMETR1.ABS,
      AUTHOR  = {{\'{S}}wierzy{\'n}ska, Jolanta and {\'{S}}wierzy{\'n}ski, Bogdan},
      TITLE   = {Shear Theorems and their role in Affine Geometry },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {439--444},
      NUMBER  = {{\bf 3}})

@ARTICLE(SERIES_1.ABS,
      AUTHOR  = {Raczkowski, Konrad and N{\Ple}dzusiak, Andrzej},
      TITLE   = {Series },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {449--452},
      NUMBER  = {{\bf 4}})

@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 = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {453--459},
      NUMBER  = {{\bf 4}})

@ARTICLE(GROUP_5.ABS,
      AUTHOR  = {Trybulec, Wojciech A.},
      TITLE   = {Commutator and Center of a Group },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {461--466},
      NUMBER  = {{\bf 4}})

@ARTICLE(NATTRA_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Natural Transformations. {D}iscrete Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {467--474},
      NUMBER  = {{\bf 4}})

@ARTICLE(MATRIX_1.ABS,
      AUTHOR  = {Jankowska, Katarzyna},
      TITLE   = {Matrices. {A}belian Group of Matrices },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {475--480},
      NUMBER  = {{\bf 4}})

@ARTICLE(PCOMPS_1.ABS,
      AUTHOR  = {Borys, Leszek},
      TITLE   = {Paracompact and Metrizable Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {481--485},
      NUMBER  = {{\bf 4}})

@ARTICLE(MIDSP_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Atlas of {M}idpoint {A}lgebra },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {487--491},
      NUMBER  = {{\bf 4}})

@ARTICLE(MEASURE2.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Several Properties of the $\sigma$-additive Measure },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {493--497},
      NUMBER  = {{\bf 4}})

@ARTICLE(METRIC_4.ABS,
      AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam},
      TITLE   = {Metrics in the {C}artesian Product -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {499--504},
      NUMBER  = {{\bf 4}})

@ARTICLE(ALI2.ABS,
      AUTHOR  = {de la Cruz, Alicia},
      TITLE   = {Fix Point Theorem for Compact Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {505--506},
      NUMBER  = {{\bf 4}})

@ARTICLE(QUIN_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Quadratic Inequalities },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {507--509},
      NUMBER  = {{\bf 4}})

@ARTICLE(BHSP_1.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Introduction to {B}anach and {H}ilbert Spaces -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {511--516},
      NUMBER  = {{\bf 4}})

@ARTICLE(BHSP_2.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Introduction to {B}anach and {H}ilbert Spaces -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {517--521},
      NUMBER  = {{\bf 4}})

@ARTICLE(BHSP_3.ABS,
      AUTHOR  = {Popio{\l}ek, Jan},
      TITLE   = {Introduction to {B}anach and {H}ilbert Spaces -- Part {III} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {523--526},
      NUMBER  = {{\bf 4}})

@ARTICLE(ENS_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Category {E}ns },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {527--533},
      NUMBER  = {{\bf 4}})

@ARTICLE(BORSUK_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {A {B}orsuk Theorem on Homotopy Types },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {535--545},
      NUMBER  = {{\bf 4}})

@ARTICLE(FUNCT_6.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {{C}artesian Product of Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {547--552},
      NUMBER  = {{\bf 4}})

@ARTICLE(MODAL_1.ABS,
      AUTHOR  = {de la Cruz, Alicia},
      TITLE   = {Introduction to Modal Propositional Logic },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {553--558},
      NUMBER  = {{\bf 4}})

@ARTICLE(TBSP_1.ABS,
      AUTHOR  = {de la Cruz, Alicia},
      TITLE   = {Totally Bounded Metric Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {559--562},
      NUMBER  = {{\bf 4}})

@ARTICLE(GRCAT_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Categories of Groups },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {563--571},
      NUMBER  = {{\bf 4}})

@ARTICLE(GROUP_6.ABS,
      AUTHOR  = {Trybulec, Wojciech A. and Trybulec, Micha{\l} J.},
      TITLE   = {Homomorphisms and Isomorphisms of Groups. {Q}uotient Group },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {573--578},
      NUMBER  = {{\bf 4}})

@ARTICLE(MOD_2.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Rings and Modules -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {579--585},
      NUMBER  = {{\bf 4}})

@ARTICLE(MOD_3.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Free Modules },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {587--589},
      NUMBER  = {{\bf 4}})

@ARTICLE(ANALORT.ABS,
      AUTHOR  = {Zajkowski, Jaros{\l}aw},
      TITLE   = {Oriented Metric-Affine Plane -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {591--597},
      NUMBER  = {{\bf 4}})

@ARTICLE(EUCLID.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata},
      TITLE   = {The {E}uclidean Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {599--603},
      NUMBER  = {{\bf 4}})

@ARTICLE(TOPMETR.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
      TITLE   = {Metric Spaces as Topological Spaces -- Fundamental Concepts },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {605--608},
      NUMBER  = {{\bf 4}})

@ARTICLE(HEINE.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
      TITLE   = {{H}eine--{B}orel's Covering Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {609--610},
      NUMBER  = {{\bf 4}})

@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 = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {611--613},
      NUMBER  = {{\bf 4}})

@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 = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {617--621},
      NUMBER  = {{\bf 5}})

@ARTICLE(GR_CY_1.ABS,
      AUTHOR  = {Surowik, Dariusz},
      TITLE   = {Cyclic Groups and Some of Their Properties -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {623--627},
      NUMBER  = {{\bf 5}})

@ARTICLE(ISOCAT_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Isomorphisms of Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {629--634},
      NUMBER  = {{\bf 5}})

@ARTICLE(CQC_SIM1.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata and Trybulec, Andrzej},
      TITLE   = {Similarity of Formulae },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {635--642},
      NUMBER  = {{\bf 5}})

@ARTICLE(RINGCAT1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Category of Rings },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {643--648},
      NUMBER  = {{\bf 5}})

@ARTICLE(MODCAT_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Category of Left Modules },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {649--652},
      NUMBER  = {{\bf 5}})

@ARTICLE(FDIFF_3.ABS,
      AUTHOR  = {Burakowska, Ewa and Madras, Beata},
      TITLE   = {Real Function One-Side Differentiability },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {653--656},
      NUMBER  = {{\bf 5}})

@ARTICLE(METRIC_6.ABS,
      AUTHOR  = {Kanas, Stanis{\l}awa and Lecko, Adam},
      TITLE   = {Sequences in Metric Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {657--661},
      NUMBER  = {{\bf 5}})

@ARTICLE(TOPREAL2.ABS,
      AUTHOR  = {Darmochwa{\l}, Agata and Nakamura, Yatsuka},
      TITLE   = {The Topological Space ${\calE}^2_{\rmT}$. {S}imple Closed Curves },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {663--664},
      NUMBER  = {{\bf 5}})

@ARTICLE(TSEP_1.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {Separated and Weakly Separated Subspaces of Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {665--674},
      NUMBER  = {{\bf 5}})

@ARTICLE(L'HOSPIT.ABS,
      AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
      TITLE   = {The de l'{H}ospital Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {675--678},
      NUMBER  = {{\bf 5}})

@ARTICLE(COMMACAT.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Darmochwa\l, Agata},
      TITLE   = {Comma Category },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {679--681},
      NUMBER  = {{\bf 5}})

@ARTICLE(LANG1.ABS,
      AUTHOR  = {Carlson, Patricia L. and Bancerek, Grzegorz},
      TITLE   = {Context-Free Grammar -- Part 1 },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {683--687},
      NUMBER  = {{\bf 5}})

@ARTICLE(MEASURE3.ABS,
      AUTHOR  = {Bia{\l}as, J\'ozef},
      TITLE   = {Completeness of the $\sigma$-Additive Measure. {M}easure Theory },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {689--693},
      NUMBER  = {{\bf 5}})

@ARTICLE(BHSP_4.ABS,
      AUTHOR  = {Kraszewska, El\.zbieta and Popio{\l}ek, Jan},
      TITLE   = {Series in {B}anach and {H}ilbert {S}paces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {695--699},
      NUMBER  = {{\bf 5}})

@ARTICLE(CAT_3.ABS,
      AUTHOR  = {Byli\'{n}ski, Czes{\l}aw},
      TITLE   = {Products and Coproducts in Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {701--709},
      NUMBER  = {{\bf 5}})

@ARTICLE(MATRIX_2.ABS,
      AUTHOR  = {Jankowska, Katarzyna},
      TITLE   = {Transpose Matrices and Groups of Permutations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {711--717},
      NUMBER  = {{\bf 5}})

@ARTICLE(LATTICE3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Complete Lattices },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1991,
      VOLUME  = 2,
      PAGES   = {719--725},
      NUMBER  = {{\bf 5}})

@ARTICLE(TMAP_1.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {Continuity of Mappings over the Union  of Subspaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {1--16},
      NUMBER  = {{\bf 1}})

@ARTICLE(SEQFUNC.ABS,
      AUTHOR  = {Perkowska, Beata},
      TITLE   = {Functional Sequence from a Domain to a Domain },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {17--21},
      NUMBER  = {{\bf 1}})

@ARTICLE(MIDSP_3.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Reper Algebras },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {23--28},
      NUMBER  = {{\bf 1}})

@ARTICLE(GR_CY_2.ABS,
      AUTHOR  = {Surowik, Dariusz},
      TITLE   = {Isomorphisms of Cyclic Groups. {S}ome Properties of Cyclic Groups },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {29--32},
      NUMBER  = {{\bf 1}})

@ARTICLE(ISOCAT_2.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Some Isomorphisms Between Functor Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {33--40},
      NUMBER  = {{\bf 1}})

@ARTICLE(TDLAT_1.ABS,
      AUTHOR  = {Watanabe, Toshihiko},
      TITLE   = {The Lattice of Domains of a Topological Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {41--46},
      NUMBER  = {{\bf 1}})

@ARTICLE(LMOD_6.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Submodules },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {47--51},
      NUMBER  = {{\bf 1}})

@ARTICLE(DIRORT.ABS,
      AUTHOR  = {Zajkowski, Jaros{\l}aw},
      TITLE   = {Oriented Metric-Affine Plane -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {53--56},
      NUMBER  = {{\bf 1}})

@ARTICLE(MOD_4.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Opposite Rings, Modules and their Morphisms },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {57--65},
      NUMBER  = {{\bf 1}})

@ARTICLE(MEASURE4.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Properties of {C}aratheodor's Measure },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {67--70},
      NUMBER  = {{\bf 1}})

@ARTICLE(TDLAT_2.ABS,
      AUTHOR  = {Karno, Zbigniew and Watanabe, Toshihiko},
      TITLE   = {Completeness of the Lattices of Domains  of a Topological Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {71--79},
      NUMBER  = {{\bf 1}})

@ARTICLE(PCOMPS_2.ABS,
      AUTHOR  = {Borys, Leszek},
      TITLE   = {On Paracompactness of Metrizable Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {81--84},
      NUMBER  = {{\bf 1}})

@ARTICLE(TREAL_1.ABS,
      AUTHOR  = {Watanabe, Toshihiko},
      TITLE   = {The {B}rouwer Fixed Point Theorem for Intervals },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {85--88},
      NUMBER  = {{\bf 1}})

@ARTICLE(CARD_5.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {On Powers of Cardinals },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {89--93},
      NUMBER  = {{\bf 1}})

@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 = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {95--99},
      NUMBER  = {{\bf 1}})

@ARTICLE(TOPREAL4.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Kotowicz, Jaros{\l}aw},
      TITLE   = {Connectedness Conditions Using Polygonal Arcs },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {101--106},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBOARD1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
      TITLE   = {Introduction to {G}o-Board -- Part {I} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {107--115},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBOARD2.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
      TITLE   = {Introduction to {G}o-Board -- Part {II} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {117--121},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBOARD3.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
      TITLE   = {Properties of {G}o-Board -- Part {III} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {123--124},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBOARD4.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Nakamura, Yatsuka},
      TITLE   = {Go-Board Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {125--129},
      NUMBER  = {{\bf 1}})

@ARTICLE(SYSREL.ABS,
      AUTHOR  = {Korczy\'nski, Waldemar},
      TITLE   = {Some Properties of Binary Relations },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {131--134},
      NUMBER  = {{\bf 1}})

@ARTICLE(JORDAN1.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Kotowicz, Jaros{\l}aw},
      TITLE   = {The {J}ordan's Property for Certain Subsets of the Plane },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {137--142},
      NUMBER  = {{\bf 2}})

@ARTICLE(TDLAT_3.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {The Lattice of Domains of an Extremally Disconnected Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {143--149},
      NUMBER  = {{\bf 2}})

@ARTICLE(AMI_1.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {A Mathematical Model of {CPU} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {151--160},
      NUMBER  = {{\bf 2}})

@ARTICLE(CAT_4.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {{C}artesian Categories },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {161--169},
      NUMBER  = {{\bf 2}})

@ARTICLE(VFUNCT_1.ABS,
      AUTHOR  = {Yamazaki, Hiroshi and Shidama, Yasunari},
      TITLE   = {Algebra of Vector Functions },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {171--175},
      NUMBER  = {{\bf 2}})

@ARTICLE(TSEP_2.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {On a Duality between Weakly Separated  Subspaces of Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {177--182},
      NUMBER  = {{\bf 2}})

@ARTICLE(PETRI.ABS,
      AUTHOR  = {Kawamoto, Pauline N. and Fuwa, Yasushi and Nakamura, Yatsuka},
      TITLE   = {Basic {P}etri Net Concepts },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {183--187},
      NUMBER  = {{\bf 2}})

@ARTICLE(FIN_TOPO.ABS,
      AUTHOR  = {Imura, Hiroshi and Eguchi, Masayoshi},
      TITLE   = {Finite Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {189--193},
      NUMBER  = {{\bf 2}})

@ARTICLE(TREES_3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Sets and Functions of Trees and Joining Operations of Trees },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {195--204},
      NUMBER  = {{\bf 2}})

@ARTICLE(FVSUM_1.ABS,
      AUTHOR  = {Zawadzka, Katarzyna},
      TITLE   = {The Sum and Product of Finite Sequences of Elements of a Field },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {205--211},
      NUMBER  = {{\bf 2}})

@ARTICLE(MONOID_0.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Monoids },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {213--225},
      NUMBER  = {{\bf 2}})

@ARTICLE(MONOID_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Monoid of Multisets and Subsets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {227--233},
      NUMBER  = {{\bf 2}})

@ARTICLE(PRVECT_1.ABS,
      AUTHOR  = {Lango, Anna and Bancerek, Grzegorz},
      TITLE   = {Product of Families of Groups and Vector Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {235--240},
      NUMBER  = {{\bf 2}})

@ARTICLE(AMI_2.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {On a Mathematical Model of Programs },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {241--250},
      NUMBER  = {{\bf 2}})

@ARTICLE(UNIALG_1.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Madras, Beata and Korolkiewicz, Ma{\l}gorzata},
      TITLE   = {Basic Notation of Universal Algebra },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {251--253},
      NUMBER  = {{\bf 2}})

@ARTICLE(COH_SP.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw and Raczkowski, Konrad},
      TITLE   = {Coherent Space },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {255--261},
      NUMBER  = {{\bf 2}})

@ARTICLE(MEASURE5.ABS,
      AUTHOR  = {Bia{\l}as, J\'{o}zef},
      TITLE   = {Properties of the Intervals of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {263--269},
      NUMBER  = {{\bf 2}})

@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 = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {271--274},
      NUMBER  = {{\bf 2}})

@ARTICLE(RFINSEQ.ABS,
      AUTHOR  = {Kotowicz, Jaros{\l}aw},
      TITLE   = {Functions and Finite Sequences of Real Numbers },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {275--278},
      NUMBER  = {{\bf 2}})

@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 = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {279--288},
      NUMBER  = {{\bf 2}})

@ARTICLE(LMOD_7.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {289--296},
      NUMBER  = {{\bf 2}})

@ARTICLE(TOPS_3.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {Remarks on Special Subsets of Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {297--303},
      NUMBER  = {{\bf 2}})

@ARTICLE(TEX_1.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {On Discrete and Almost Discrete Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1992,
      VOLUME  = 3,
      PAGES   = {305--310},
      NUMBER  = {{\bf 2}})

@ARTICLE(MATRIX_3.ABS,
      AUTHOR  = {Zawadzka, Katarzyna},
      TITLE   = {The Product and the Determinant of Matrices with Entries in a Field },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {1--8},
      NUMBER  = {{\bf 1}})

@ARTICLE(REARRAN1.ABS,
      AUTHOR  = {Sakai, Yuji and Kotowicz, Jaros{\l}aw},
      TITLE   = {Introduction to Theory of Rearrangement },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {9--13},
      NUMBER  = {{\bf 1}})

@ARTICLE(PBOOLE.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Many-sorted Sets },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {15--22},
      NUMBER  = {{\bf 1}})

@ARTICLE(UNIALG_2.ABS,
      AUTHOR  = {Burakowska, Ewa},
      TITLE   = {Subalgebras of the Universal Algebra. {L}attices of Subalgebras },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {23--27},
      NUMBER  = {{\bf 1}})

@ARTICLE(HAHNBAN.ABS,
      AUTHOR  = {Nowak, Bogdan and Trybulec, Andrzej},
      TITLE   = {Hahn-{B}anach Theorem },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {29--34},
      NUMBER  = {{\bf 1}})

@ARTICLE(LATTICE4.ABS,
      AUTHOR  = {Kamie{\'n}ska, Jolanta and Walijewski, Jaros{\l}aw Stanis{\l}aw},
      TITLE   = {Homomorphisms of Lattices, Finite Join and Finite Meet },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {35--40},
      NUMBER  = {{\bf 1}})

@ARTICLE(OPENLATT.ABS,
      AUTHOR  = {Kamie\'nska, Jolanta},
      TITLE   = {Representation Theorem for {H}eyting Lattices },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {41--45},
      NUMBER  = {{\bf 1}})

@ARTICLE(LOPCLSET.ABS,
      AUTHOR  = {Walijewski, Jaros{\l}aw Stanis{\l}aw},
      TITLE   = {Representation Theorem for Boolean Algebras },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {45--50},
      NUMBER  = {{\bf 1}})

@ARTICLE(AMI_3.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
      TITLE   = {Some Remarks on the Simple Concrete Model of Computer },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {51--56},
      NUMBER  = {{\bf 1}})

@ARTICLE(AMI_4.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
      TITLE   = {{E}uclid's Algorithm },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {57--60},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCM_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {Development of Terminology for {\bf SCM} },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {61--67},
      NUMBER  = {{\bf 1}})

@ARTICLE(PRE_FF.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {Two Programs for {\bf SCM}. {P}art {I} -- Preliminaries },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {69--72},
      NUMBER  = {{\bf 1}})

@ARTICLE(FIB_FUSC.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {Two Programs for {\bf SCM}. {P}art {II} -- Programs },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {73--75},
      NUMBER  = {{\bf 1}})

@ARTICLE(TREES_4.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Joining of Decorated Trees },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {77--82},
      NUMBER  = {{\bf 1}})

@ARTICLE(BINARITH.ABS,
      AUTHOR  = {Nishiyama, Takaya and Mizuhara, Yasuho},
      TITLE   = {Binary Arithmetics },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {83--86},
      NUMBER  = {{\bf 1}})

@ARTICLE(BOOLMARK.ABS,
      AUTHOR  = {Kawamoto, Pauline N. and Fuwa, Yasushi and Nakamura, Yatsuka},
      TITLE   = {Basic Concepts for {P}etri Nets with Boolean Markings },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {87--90},
      NUMBER  = {{\bf 1}})

@ARTICLE(DTCONSTR.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {On Defining Functions on Trees },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {91--101},
      NUMBER  = {{\bf 1}})

@ARTICLE(PRALG_1.ABS,
      AUTHOR  = {Madras, Beata},
      TITLE   = {Product of Family of Universal Algebras },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {103--108},
      NUMBER  = {{\bf 1}})

@ARTICLE(ALG_1.ABS,
      AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
      TITLE   = {Homomorphisms of Algebras. {Q}uotient Universal Algebra },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {109--113},
      NUMBER  = {{\bf 1}})

@ARTICLE(FREEALG.ABS,
      AUTHOR  = {Perkowska, Beata},
      TITLE   = {Free Universal Algebra Construction },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {115--120},
      NUMBER  = {{\bf 1}})

@ARTICLE(COMSEQ_1.ABS,
      AUTHOR  = {Banachowicz, Agnieszka and Winnicka, Anna},
      TITLE   = {Complex Sequences },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {121--124},
      NUMBER  = {{\bf 1}})

@ARTICLE(TEX_2.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {Maximal Discrete Subspaces of Almost Discrete Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {125--135},
      NUMBER  = {{\bf 1}})

@ARTICLE(TEX_3.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {On Nowhere and Everywhere Dense Subspaces of Topological Spaces },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1993,
      VOLUME  = 4,
      PAGES   = {137--146},
      NUMBER  = {{\bf 1}})

@ARTICLE(AMI_5.ABS,
      AUTHOR  = {Tanaka, Yasushi},
      TITLE   = {On the Decomposition of the States of {SCM}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {1--8},
      NUMBER  = {{\bf 1}})

@ARTICLE(BINTREE1.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {On Defining Functions on Binary Trees},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {9--13},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCM_COMP.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Rudnicki, Piotr},
      TITLE   = {A Compiler of Arithmetic Expressions for {SCM}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {15--20},
      NUMBER  = {{\bf 1}})

@ARTICLE(MEASURE6.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {Some Properties of the Intervals},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {21--26},
      NUMBER  = {{\bf 1}})

@ARTICLE(BINARI_2.ABS,
      AUTHOR  = {Mizuhara, Yasuho and Nishiyama, Takaya},
      TITLE   = {Binary Arithmetics, Addition and Subtraction of Integers},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {27--29},
      NUMBER  = {{\bf 1}})

@ARTICLE(BOOLEALG.ABS,
      AUTHOR  = {Marasik, Agnieszka Julia},
      TITLE   = {Boolean Properties of Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {31--35},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSUALG_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {37--42},
      NUMBER  = {{\bf 1}})

@ARTICLE(AUTGROUP.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Group of Inner Automorphisms},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {43--45},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSUALG_2.ABS,
      AUTHOR  = {Burakowska, Ewa},
      TITLE   = {Subalgebras of Many Sorted Algebra. {L}attice of Subalgebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {47--54},
      NUMBER  = {{\bf 1}})

@ARTICLE(PRALG_2.ABS,
      AUTHOR  = {Madras, Beata},
      TITLE   = {Products of Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {55--60},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSUALG_3.ABS,
      AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
      TITLE   = {Homomorphisms of Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {61--65},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSAFREE.ABS,
      AUTHOR  = {Perkowska, Beata},
      TITLE   = {Free Many Sorted Universal Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {67--74},
      NUMBER  = {{\bf 1}})

@ARTICLE(T_0TOPSP.ABS,
      AUTHOR  = {\.Zynel, Mariusz and Guzowski, Adam},
      TITLE   = { \Tzero\ Topological Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {75--77},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSUALG_4.ABS,
      AUTHOR  = {Korolkiewicz, Ma{\l}gorzata},
      TITLE   = {Many Sorted Quotient Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {79--84},
      NUMBER  = {{\bf 1}})

@ARTICLE(QUANTAL1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Quantales},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {85--91},
      NUMBER  = {{\bf 1}})

@ARTICLE(TOPRNS_1.ABS,
      AUTHOR  = {Sakowicz, Agnieszka and Gryko, Jaros{\l}aw and Grabowski, Adam},
      TITLE   = {Sequences in ${\calE}^{N}_{\rmT}$},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {93--96},
      NUMBER  = {{\bf 1}})

@ARTICLE(SPPOL_1.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Byli\'nski, Czes\l{}aw},
      TITLE   = {Extremal Properties of Vertices on Special Polygons. {P}art {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {97--102},
      NUMBER  = {{\bf 1}})

@ARTICLE(RELOC.ABS,
      AUTHOR  = {Tanaka, Yasushi},
      TITLE   = {Relocatability},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {103--108},
      NUMBER  = {{\bf 1}})

@ARTICLE(TEX_4.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {Maximal Anti-Discrete Subspaces of Topological Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {109--118},
      NUMBER  = {{\bf 1}})

@ARTICLE(TSP_1.ABS,
      AUTHOR  = {Karno, Zbigniew},
      TITLE   = {On {K}olmogorov Topological Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {119--124},
      NUMBER  = {{\bf 1}})

@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 = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {125--130},
      NUMBER  = {{\bf 1}})

@ARTICLE(PROJPL_1.ABS,
      AUTHOR  = {Muzalewski, Micha{\l}},
      TITLE   = {Projective Planes},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {131--136},
      NUMBER  = {{\bf 1}})

@ARTICLE(SGRAPH1.ABS,
      AUTHOR  = {Toda, Yozo},
      TITLE   = {The Formalization of Simple Graphs},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {137--144},
      NUMBER  = {{\bf 1}})

@ARTICLE(GRSOLV_1.ABS,
      AUTHOR  = {Zawadzka, Katarzyna},
      TITLE   = {Solvable Groups},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {145--147},
      NUMBER  = {{\bf 1}})

@ARTICLE(FILTER_2.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Ideals},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {149--156},
      NUMBER  = {{\bf 2}})

@ARTICLE(CAT_5.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Categorial Categories and Slice Categories},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {157--165},
      NUMBER  = {{\bf 2}})

@ARTICLE(PRE_CIRC.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
      TITLE   = {Preliminaries to Circuits, {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {167--172},
      NUMBER  = {{\bf 2}})

@ARTICLE(FSM_1.ABS,
      AUTHOR  = {Kaloper , Miroslava and Rudnicki, Piotr},
      TITLE   = {Minimization of finite state machines},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {173--184},
      NUMBER  = {{\bf 2}})

@ARTICLE(TREES_9.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Subtrees},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {185--190},
      NUMBER  = {{\bf 2}})

@ARTICLE(MSATERM.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Terms Over Many Sorted Universal Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {191--198},
      NUMBER  = {{\bf 2}})

@ARTICLE(DECOMP_1.ABS,
      AUTHOR  = {Przemski, Marian},
      TITLE   = {On the Decomposition of the Continuity},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {199--204},
      NUMBER  = {{\bf 2}})

@ARTICLE(MSAFREE1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {A Scheme for Extensions of Homomorphisms of Manysorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {205--209},
      NUMBER  = {{\bf 2}})

@ARTICLE(MSUHOM_1.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {The Correspondence Between Homomorphisms of Universal Algebra   \& Many Sorted Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {211--214},
      NUMBER  = {{\bf 2}})

@ARTICLE(MSAFREE2.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
      TITLE   = {Preliminaries to Circuits, {II}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {215--220},
      NUMBER  = {{\bf 2}})

@ARTICLE(AUTALG_1.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Group of Automorphisms of Universal Algebra \&         Many Sorted Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {221--226},
      NUMBER  = {{\bf 2}})

@ARTICLE(CIRCUIT1.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
      TITLE   = {Introduction to Circuits, {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {227--232},
      NUMBER  = {{\bf 2}})

@ARTICLE(CANTOR_1.ABS,
      AUTHOR  = {Shibakov, Alexander Yu. and Trybulec, Andrzej},
      TITLE   = {The {C}antor Set},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {233--236},
      NUMBER  = {{\bf 2}})

@ARTICLE(CQC_THE3.ABS,
      AUTHOR  = {Okhotnikov, Oleg},
      TITLE   = {Logical Equivalence of Formulae},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {237--240},
      NUMBER  = {{\bf 2}})

@ARTICLE(FINSEQ_5.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Some Properties of Restrictions of Finite Sequences},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {241--245},
      NUMBER  = {{\bf 2}})

@ARTICLE(SPPOL_2.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw and Nakamura, Yatsuka},
      TITLE   = {Special Polygons},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {247--252},
      NUMBER  = {{\bf 2}})

@ARTICLE(MEASURE7.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef},
      TITLE   = {The One-Dimensional {L}ebesgue Measure },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {253--258},
      NUMBER  = {{\bf 2}})

@ARTICLE(ALTCAT_1.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Categories without Uniqueness of {\bf cod} and {\bf dom}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {259--267},
      NUMBER  = {{\bf 2}})

@ARTICLE(EXTENS_1.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Extensions of Mappings on Generator Set},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {269--272},
      NUMBER  = {{\bf 2}})

@ARTICLE(CIRCUIT2.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr and Trybulec, Andrzej and Kawamoto, Pauline N.},
      TITLE   = {Introduction to Circuits, {II}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {273--278},
      NUMBER  = {{\bf 2}})

@ARTICLE(MBOOLEAN.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Definitions and Basic Properties of Boolean \&          Union of Many Sorted Sets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {279--281},
      NUMBER  = {{\bf 2}})

@ARTICLE(CIRCCOMB.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Bancerek, Grzegorz},
      TITLE   = {Combining of Circuits},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {283--295},
      NUMBER  = {{\bf 2}})

@ARTICLE(GRAPH_2.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr},
      TITLE   = {Vertex Sequences Induced by Chains},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {297--304},
      NUMBER  = {{\bf 3}})

@ARTICLE(VECTSP_8.ABS,
      AUTHOR  = {Iwaniuk, Andrzej},
      TITLE   = {On the Lattice of Subspaces of a Vector Space},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {305--308},
      NUMBER  = {{\bf 3}})

@ARTICLE(LATSUBGR.ABS,
      AUTHOR  = {Ganczarski, Janusz},
      TITLE   = {On the Lattice of Subgroups of a Group},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {309--312},
      NUMBER  = {{\bf 3}})

@ARTICLE(UNIALG_3.ABS,
      AUTHOR  = {Paszek, Miros{\l}aw Jan},
      TITLE   = {On the Lattice of Subalgebras of a Universal Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {313--316},
      NUMBER  = {{\bf 3}})

@ARTICLE(FINSEQ_6.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {On the Decomposition of Finite Sequences},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {317--322},
      NUMBER  = {{\bf 3}})

@ARTICLE(GOBOARD5.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {Decomposing a {G}o-Board into Cells},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {323--328},
      NUMBER  = {{\bf 3}})

@ARTICLE(INDEX_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Indexed Category},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {329--337},
      NUMBER  = {{\bf 3}})

@ARTICLE(MATRLIN.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {Associated Matrix of Linear Map},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {339--345},
      NUMBER  = {{\bf 3}})

@ARTICLE(GOBOARD6.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {On the Geometry of a {G}o-{B}oard},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {347--352},
      NUMBER  = {{\bf 3}})

@ARTICLE(WEIERSTR.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef and Nakamura, Yatsuka},
      TITLE   = {The Theorem of {W}eierstrass},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {353--359},
      NUMBER  = {{\bf 3}})

@ARTICLE(URYSOHN1.ABS,
      AUTHOR  = {Bia{\l}as, J{\'o}zef and Nakamura, Yatsuka},
      TITLE   = {Dyadic Numbers and {T}${}_4$ Topological Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {361--366},
      NUMBER  = {{\bf 3}})

@ARTICLE(FACIRC_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Nakamura, Yatsuka},
      TITLE   = {Full Adder Circuit.  {P}art {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {367--380},
      NUMBER  = {{\bf 3}})

@ARTICLE(COHSP_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Continuous, Stable, and Linear Maps of Coherence Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {381--393},
      NUMBER  = {{\bf 3}})

@ARTICLE(PZFMISC1.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Some Basic Properties of Many Sorted Sets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {395--399},
      NUMBER  = {{\bf 3}})

@ARTICLE(TREES_A.ABS,
      AUTHOR  = {Okhotnikov, Oleg},
      TITLE   = {Replacement of Subtrees in a Tree},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {401--403},
      NUMBER  = {{\bf 3}})

@ARTICLE(PUA2MSS1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Minimal Signature for Partial Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {405--414},
      NUMBER  = {{\bf 3}})

@ARTICLE(QC_LANG4.ABS,
      AUTHOR  = {Okhotnikov, Oleg},
      TITLE   = {The Subformula Tree of a Formula of the First Order Language},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {415--422},
      NUMBER  = {{\bf 3}})

@ARTICLE(VECTSP_9.ABS,
      AUTHOR  = {{\.Z}ynel, Mariusz},
      TITLE   = {The {S}teinitz Theorem and the Dimension of a Vector Space},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {423--428},
      NUMBER  = {{\bf 3}})

@ARTICLE(GOBOARD7.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {On the {G}o-{B}oard of a Standard Special Circular Sequence},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {429--438},
      NUMBER  = {{\bf 3}})

@ARTICLE(ENDALG.ABS,
      AUTHOR  = {Gryko, Jaros{\l}aw},
      TITLE   = {On the Monoid of Endomorphisms of Universal Algebra and Many        Sorted Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {439--442},
      NUMBER  = {{\bf 3}})

@ARTICLE(GOBOARD8.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {More on Segments on a {G}o-{B}oard},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {443--450},
      NUMBER  = {{\bf 3}})

@ARTICLE(MSSUBFAM.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Certain Facts about Families of Subsets of Many Sorted Sets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {451--456},
      NUMBER  = {{\bf 3}})

@ARTICLE(TRIANG_1.ABS,
      AUTHOR  = {Madras, Beata},
      TITLE   = {On the Concept of the Triangulation},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {457--462},
      NUMBER  = {{\bf 3}})

@ARTICLE(GOBOARD9.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Left and Right Component of the Complement of a Special Closed Curve},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {465--468},
      NUMBER  = {{\bf 4}})

@ARTICLE(REWRITE1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Reduction Relations},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {469--478},
      NUMBER  = {{\bf 4}})

@ARTICLE(MSUALG_5.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {Lattice of Congruences in Many Sorted Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {479--483},
      NUMBER  = {{\bf 4}})

@ARTICLE(FUNCT_7.ABS,
      AUTHOR  = {Bancerek, Grzegorz and Trybulec, Andrzej},
      TITLE   = {Miscellaneous Facts about Functions},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {485--492},
      NUMBER  = {{\bf 4}})

@ARTICLE(ALTCAT_2.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Examples of Category Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {493--500},
      NUMBER  = {{\bf 4}})

@ARTICLE(ORDERS_3.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {On the Category of Posets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {501--505},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_1.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Rudnicki, Piotr},
      TITLE   = {An Extension of {\bf SCM}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {507--512},
      NUMBER  = {{\bf 4}})

@ARTICLE(CONNSP_3.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {Components and Unions of Components},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {513--517},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_2.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Rudnicki, Piotr},
      TITLE   = {The {\SCMFSA} Computer},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {519--528},
      NUMBER  = {{\bf 4}})

@ARTICLE(CLOSURE1.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Many Sorted Closure Operator and the Many Sorted Closure System},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {529--536},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_3.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
      TITLE   = {Computation in {\SCMFSA}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {537--542},
      NUMBER  = {{\bf 4}})

@ARTICLE(CLOSURE2.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Closure Operator and the Closure System of Many Sorted Sets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {543--551},
      NUMBER  = {{\bf 4}})

@ARTICLE(MSUALG_6.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Translations, Endomorphisms, and Stable Equational Theories},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {553--564},
      NUMBER  = {{\bf 4}})

@ARTICLE(MSUALG_7.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {More on the Lattice of Many Sorted Equivalence Relations},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {565--569},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_4.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
      TITLE   = {Modifying Addresses of Instructions of {\SCMFSA}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {571--576},
      NUMBER  = {{\bf 4}})

@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 = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {577--582},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_5.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka},
      TITLE   = {Relocability for {\SCMFSA}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {583--586},
      NUMBER  = {{\bf 4}})

@ARTICLE(MSUALG_8.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {More on the Lattice of Congruences in Many Sorted Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {587--590},
      NUMBER  = {{\bf 4}})

@ARTICLE(MSSCYC_2.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw and Rudnicki, Piotr},
      TITLE   = {The Correspondence Between Monotonic Many Sorted Signatures        and Well-Founded Graphs. {P}art {II}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {591--593},
      NUMBER  = {{\bf 4}})

@ARTICLE(FUNCTOR0.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {Functors for Alternative Categories},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {595--608},
      NUMBER  = {{\bf 4}})

@ARTICLE(FUNCTOR1.ABS,
      AUTHOR  = {Zinn, Claus and Jaksch, Wolfgang},
      TITLE   = {Basic Properties of Functor Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {609--613},
      NUMBER  = {{\bf 4}})

@ARTICLE(SCMFSA_7.ABS,
      AUTHOR  = {Asamoto, Noriko},
      TITLE   = {Some Multi Instructions Defined by Sequence of Instructions of {\SCMFSA}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {615--619},
      NUMBER  = {{\bf 4}})

@ARTICLE(PRALG_3.ABS,
      AUTHOR  = {Giero, Mariusz},
      TITLE   = {More on Products of Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1996,
      VOLUME  = 5,
      PAGES   = {621--626},
      NUMBER  = {{\bf 4}})

@ARTICLE(GOBRD10.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {Adjacency Concept for Pairs of Natural Numbers},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {1--3},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSALIMIT.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {Inverse Limits of Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {5--8},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSUALG_9.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Trivial Many Sorted Algebras and Many Sorted Congruences},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {9--15},
      NUMBER  = {{\bf 1}})

@ARTICLE(MSINST_1.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {Examples of Category Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {17--20},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCMFSA6A.ABS,
      AUTHOR  = {Trybulec, Andrzej and Nakamura, Yatsuka and Asamoto, Noriko},
      TITLE   = {On the Compositions of Macro Instructions. {P}art {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {21--27},
      NUMBER  = {{\bf 1}})

@ARTICLE(SF_MASTR.ABS,
      AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
      TITLE   = {Memory Handling for {\SCMFSA}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {29--36},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBRD11.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {Some Topological Properties of Cells in ${\calE}^2_{\rmT}$},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {37--40},
      NUMBER  = {{\bf 1}})

@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 = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {41--47},
      NUMBER  = {{\bf 1}})

@ARTICLE(GOBRD12.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Trybulec, Andrzej},
      TITLE   = {The First Part of {J}ordan's Theorem for Special Polygons},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {49--51},
      NUMBER  = {{\bf 1}})

@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 = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {53--57},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCMFSA7B.ABS,
      AUTHOR  = {Asamoto, Noriko},
      TITLE   = {Constant Assignment Macro Instructions of {\SCMFSA}. {P}art {II}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {59--63},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCMFSA8A.ABS,
      AUTHOR  = {Asamoto, Noriko},
      TITLE   = {Conditional Branch Macro Instructions of {\SCMFSA}. {P}art {I}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {65--72},
      NUMBER  = {{\bf 1}})

@ARTICLE(SCMFSA8B.ABS,
      AUTHOR  = {Asamoto, Noriko},
      TITLE   = {Conditional Branch Macro Instructions of {\SCMFSA}. {P}art {II}},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {73--80},
      NUMBER  = {{\bf 1}})

@ARTICLE(YELLOW_0.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Bounds in Posets and Relational Substructures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {81--91},
      NUMBER  = {{\bf 1}})

@ARTICLE(WAYBEL_0.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Directed Sets, Nets, Ideals, Filters, and Maps},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {93--107},
      NUMBER  = {{\bf 1}})

@ARTICLE(KNASTER.ABS,
      AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
      TITLE   = {Fixpoints in Complete Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {109--115},
      NUMBER  = {{\bf 1}})

@ARTICLE(YELLOW_1.ABS,
      AUTHOR  = {Grabowski, Adam and Milewski, Robert},
      TITLE   = {Boolean Posets, Posets under Inclusion and    Products of Relational Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {117--121},
      NUMBER  = {{\bf 1}})

@ARTICLE(YELLOW_2.ABS,
      AUTHOR  = {{\.Z}ynel, Mariusz and Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Properties of Relational Structures, Posets, Lattices and Maps},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {123--130},
      NUMBER  = {{\bf 1}})

@ARTICLE(WAYBEL_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw},
      TITLE   = {Galois Connections },
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {131--143},
      NUMBER  = {{\bf 1}})

@ARTICLE(YELLOW_3.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Cartesian Products of Relations and Relational Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {145--152},
      NUMBER  = {{\bf 1}})

@ARTICLE(YELLOW_4.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Definitions and Properties of the Join and Meet of Subsets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {153--158},
      NUMBER  = {{\bf 1}})

@ARTICLE(WAYBEL_2.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Meet--Continuous Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {159--167},
      NUMBER  = {{\bf 1}})

@ARTICLE(WAYBEL_3.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {The ``Way-Below'' Relation},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {169--176},
      NUMBER  = {{\bf 1}})

@ARTICLE(WAYBEL_4.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {Auxiliary and Approximating Relations},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {179--188},
      NUMBER  = {{\bf 2}})

@ARTICLE(TWOSCOMP.ABS,
      AUTHOR  = {Wasaki, Katsumi and Kawamoto, Pauline N.},
      TITLE   = {2's Complement Circuit},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {189--197},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL_5.ABS,
      AUTHOR  = {{\.Z}ynel, Mariusz},
      TITLE   = {The Equational Characterization of Continuous Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {199--205},
      NUMBER  = {{\bf 2}})

@ARTICLE(YELLOW_5.ABS,
      AUTHOR  = {Marasik, Agnieszka Julia},
      TITLE   = {Miscellaneous Facts about Relation Structure},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {207--211},
      NUMBER  = {{\bf 2}})

@ARTICLE(YELLOW_6.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {{M}oore-{S}mith Convergence},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {213--225},
      NUMBER  = {{\bf 2}})

@ARTICLE(YELLOW_7.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Duality in Relation Structures},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {227--232},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL_6.ABS,
      AUTHOR  = {Madras, Beata},
      TITLE   = {Irreducible and Prime Elements},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {233--239},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL_7.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Prime Ideals and Filters},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {241--247},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL_8.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {Algebraic Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {249--254},
      NUMBER  = {{\bf 2}})

@ARTICLE(JORDAN3.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Matuszewski, Roman},
      TITLE   = {Reconstructions of Special Sequences},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {255--263},
      NUMBER  = {{\bf 2}})

@ARTICLE(COMSEQ_2.ABS,
      AUTHOR  = {Naumowicz, Adam},
      TITLE   = {Conjugate Sequences, Bounded Complex Sequences and    Convergent Complex Sequences},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {265--268},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL_9.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the Topological Properties of Meet-Continuous Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {269--277},
      NUMBER  = {{\bf 2}})

@ARTICLE(INSTALG1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Institution of Many Sorted Algebras. {P}art {I}: Signature Reduct of an Algebra},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {279--287},
      NUMBER  = {{\bf 2}})

@ARTICLE(YELLOW_8.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {{B}aire Spaces, {S}ober Spaces},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {289--294},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL10.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Closure Operators and Subalgebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {295--301},
      NUMBER  = {{\bf 2}})

@ARTICLE(CATALG_1.ABS,
      AUTHOR  = {Bancerek, Grzegorz},
      TITLE   = {Algebra of Morphisms},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {303--310},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL11.ABS,
      AUTHOR  = {Trybulec, Andrzej},
      TITLE   = {{S}cott Topology},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {311--319},
      NUMBER  = {{\bf 2}})

@ARTICLE(WAYBEL12.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {On the {B}aire Category Theorem},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {321--327},
      NUMBER  = {{\bf 2}})

@ARTICLE(ALTCAT_3.ABS,
      AUTHOR  = {Madras, Beata},
      TITLE   = {Basic Properties of Objects and Morphisms},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {329--334},
      NUMBER  = {{\bf 3}})

@ARTICLE(ABIAN.ABS,
      AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
      TITLE   = {{A}bian's Fixed Point Theorem},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {335--338},
      NUMBER  = {{\bf 3}})

@ARTICLE(WELLFND1.ABS,
      AUTHOR  = {Rudnicki, Piotr and Trybulec, Andrzej},
      TITLE   = {On Same Equivalents of Well-foundedness},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {339--343},
      NUMBER  = {{\bf 3}})

@ARTICLE(WAYBEL13.ABS,
      AUTHOR  = {Milewski, Robert},
      TITLE   = {Algebraic and Arithmetic Lattices},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {345--349},
      NUMBER  = {{\bf 3}})

@ARTICLE(JORDAN4.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Matuszewski, Roman and Grabowski, Adam},
      TITLE   = {Subsequences of Standard Special Circular Sequences in ${\calE}^2_{\rmT}$},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {351--358},
      NUMBER  = {{\bf 3}})

@ARTICLE(SUBSTLAT.ABS,
      AUTHOR  = {Grabowski, Adam},
      TITLE   = {Lattice of Substitutions},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {359--361},
      NUMBER  = {{\bf 3}})

@ARTICLE(EQUATION.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {Equations in Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {363--369},
      NUMBER  = {{\bf 3}})

@ARTICLE(FUNCTOR2.ABS,
      AUTHOR  = {Nieszczerzewski, Robert},
      TITLE   = {Category of Functors Between Alternative Categories},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {371--375},
      NUMBER  = {{\bf 3}})

@ARTICLE(YONEDA_1.ABS,
      AUTHOR  = {Wojciechowski, Miros{\l}aw},
      TITLE   = {Yoneda Embedding},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {377--379},
      NUMBER  = {{\bf 3}})

@ARTICLE(GCD_1.ABS,
      AUTHOR  = {Schwarzweller, Christoph},
      TITLE   = {The Correctness of the Generic Algorithms of {B}rown and {H}enrici Concerning Addition and Multiplication in Fraction Fields},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {381--388},
      NUMBER  = {{\bf 3}})

@ARTICLE(BIRKHOFF.ABS,
      AUTHOR  = {Korni{\l}owicz, Artur},
      TITLE   = {{B}irkhoff Theorem for Many Sorted Algebras},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {389--395},
      NUMBER  = {{\bf 3}})

@ARTICLE(CLOSURE3.ABS,
      AUTHOR  = {Marasik, Agnieszka Julia},
      TITLE   = {Algebraic Operation on Subsets of Many Sorted Sets},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {397--401},
      NUMBER  = {{\bf 3}})

@ARTICLE(COMSEQ_3.ABS,
      AUTHOR  = {Shidama, Yasunari and Korni{\l}owicz, Artur},
      TITLE   = {Convergence and the Limit of Complex Sequences. {S}eries},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {403--410},
      NUMBER  = {{\bf 3}})

@ARTICLE(RLVECT_5.ABS,
      AUTHOR  = {Chen, Jing-Chao},
      TITLE   = {The {S}teinitz Theorem and the Dimension of a Real Linear Space},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {411--415},
      NUMBER  = {{\bf 3}})

@ARTICLE(GRAPH_3.ABS,
      AUTHOR  = {Nakamura, Yatsuka and Rudnicki, Piotr},
      TITLE   = {{E}uler Circuits and Paths},
      JOURNAL = {Formalized Mathematics},
      YEAR    = 1997,
      VOLUME  = 6,
      PAGES   = {417--425},
      NUMBER  = {{\bf 3}})

@ARTICLE(PSCOMP_1.ABS,
      AUTHOR  = {Byli{\'n}ski, Czes{\l}aw and Rudnicki, Piotr},
      TITLE   = {Bounding Boxes for Com