let T be non empty TopSpace; :: thesis: for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let p be Point of T; :: thesis: for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
let A be Element of (OpenNeighborhoods p); :: thesis: A is a_neighborhood of p
ex W being Subset of T st
( W = A & p in W & W is open ) by YELLOW_6:29;
hence A is a_neighborhood of p by CONNSP_2:3; :: thesis: verum