:: deftheorem Def3 defines Niemytzki-plane TOPGEN_5:def 3 :
for b₁ being non empty strict TopSpace holds
( b₁ = Niemytzki-plane iff ( the carrier of b₁ = y>=0-plane & ex B being Neighborhood_System of b₁ st
( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) ) );