@MISC{TOPGEN_2.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {On the characteristic and weight of a topological space},
  NOTE = {This work has been partially supported by the KBN grant
  4 T11C 039 24.},
  SECTION1 = {Characteristic of Topological Spaces},
  SECTION2 = {Neighborhood Systems},
  SECTION3 = {Weights of Topological Spaces},
  SECTION4 = {Example of Almost Discrete Topological Space with Infinity},
  SECTION5 = {Exercises},
  DAY = {10},
  MONTH = {December},
  YEAR = {2004},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  SUMMARY = {We continue Mizar formalization of General Topology according to
the book \cite{ENGEL:1} by Engelking. In the article
the formalization of Section 1.1 is completed.
Namely, the paper includes the formalization of theorems
on correspondence of the basis and basis in a point,
definitions of the character of a point and a topological space,
a neighborhood system, and the weight of a topological space.
The formalization is tested with almost discrete topological spaces
with infinity.}}

