@MISC{TOPGEN_3.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {On constructing topological spaces and Sorgenfrey line},
  NOTE = {This work has been partially supported by the KBN grant
  4 T11C 039 24.},
  SECTION1 = {Introducing Topology},
  SECTION2 = {Sorgenfrey Line},
  SECTION3 = {Example: closed = finite},
  SECTION4 = {Example: one point closure},
  SECTION5 = {Example: discrete on subset},
  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.2 is
almost completed. Namely, we formalize theorems on introduction of topologies by bases,
neighborhood systems, closed sets, closure operator, and interior operator. The Sorgenfrey
line is defined by a basis. It is proved that the weight of it is continuum.
Other techniques are used to demonstrate introduction of discrete and anti-discrete topologies.}}

