@MISC{PCOMPS_2.MIZ,
  AUTHOR = {Borys, Leszek},
  TITLE = {On Paracompactness of Metrizable Spaces},
  SECTION1 = {Selected Properties of Real Numbers},
  SECTION2 = {Certain Functions Defined on Families of Sets},
  SECTION3 = {Paracompactness of Metrizable Spaces},
  DAY = {23},
  MONTH = {July},
  YEAR = {1992},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {The aim is to prove, using Mizar System, one of the most important result
in general topology, namely the Stone Theorem on paracompactness of metrizable
spaces \cite{STONE:2}.
Our proof is based on \cite{RUDIN:1} (and also \cite{PATKOWSKA:74}). We prove first
auxiliary fact that every open cover of any metrizable space has a locally
finite open refinement.
We show next the main theorem that every metrizable space is paracompact.
The remaining material is devoted to concepts and certain properties needed
for the formulation and the proof of that theorem
(see also \cite{PCOMPS_1.ABS}).}}

