Niemytzki Plane - an Example of Tychonoff Space Which Is Not T 4

Summary. We continue Mizar formalization of General Topology according to the book [20] by Engelking. Niemytzki plane is defined as halfplane y ≥ 0 with topology introduced by a neighborhood system. Niemytzki plane is not T4. Next, the definition of Tychonoff space is given. The characterization of Tychonoff space by prebasis and the fact that Tychonoff spaces are between T3 and T4 is proved. The final result is that Niemytzki plane is also a Tychonoff space.