@MISC{METRIZTS.MIZ,
  AUTHOR = {P\c{a}k, Karol},
  TITLE = {Basic Properties of Metrizable Topological Spaces},
  SECTION1 = {Preliminaries},
  SECTION2 = {Main Properties},
  SECTION2 = {Properties of Lindel\"of spaces},
  DAY = {31},
  MONTH = {March},
  YEAR = {2009},
  ADDRESS1 = {University of Bialystok, ul. Akademicka 2, 15-267 Bialystok},
  SUMMARY = {We continue Mizar formalization of general topology according to
             the book \cite{ENGEL:1} by Engelking. In the article we present
             the final theorem of Section 4.1. Namely, the paper includes the
             formalization of theorems on the correspondence beetwen the
             cardinalities of the basis and of some open subcover, and a
             discreet (closed) subspaces, and the weight of that metrizable
             topological space. We also define Lindel\"of spaces and state the
             above theorem in this special case. We also introduce the concept
             of separation among two subsets (see \cite{ENGEL:BM51}).}}

@BOOK{ENGEL:BM51,
 AUTHOR={Engelking, Ryszard},
 TITLE={Teoria wymiaru},
 PUBLISHER={PWN},
 YEAR=1981}

