@MISC{TOPGEN_5.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Niemytzki Plane -- an Example of {T}ychonoff Space
           Which Is Not $T_4$},
  SECTION1 = {Preliminaries},
  SECTION2 = {Niemytzki Plane},
  SECTION3 = {Tychonoff Spaces},
  SECTION4 = {Niemytzki Plane is Tychonoff Space},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  DAY = {7},
  MONTH = {November},
  YEAR = {2005},
  SUMMARY = {We continue Mizar formalization of General Topology
    according to the book \cite{ENGEL:1} by Engelking.
    Niemytzki plane is defined as halfplane $y \geq 0$
    with topology introduced by a neighborhood system.
    Niemytzki plane is not $T_4$. Next, the definition of Tychonoff
    space is given. The characterization of Tychonoff space by prebasis
    and the fact that Tychonoff spaces are between $T_3$ and $T_4$ is proved.
    The final result is that Niemytzki plane is also a Tychonoff space.}}
