for p being Point of (TOP-REAL 2)
for G being Subset of (TOP-REAL 2) st G is open & p in G holds
ex r being Real st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G )