theorem Th30: :: TOPGEN_5:30

for p being Point of Niemytzki-plane
for r being positive Real ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )